diff --git a/content/blog/integer-sets-lean4.md b/content/blog/integer-sets-lean4.md
new file mode 100644
index 0000000..19b91f9
--- /dev/null
+++ b/content/blog/integer-sets-lean4.md
@@ -0,0 +1,515 @@
+---
+title: "Working with integer sets in Lean 4"
+date: 2024-03-31T21:10:23-04:00
+draft: false
+tags: ["Formal Methods"]
+math: true
+medium_enabled: false
+---
+
+Recently I was convinced by [James Oswald](https://jamesoswald.dev/) to work with him on proving some lemmas about specific integer sets in Lean 4. Since we have different styles in going about Lean proofs, I present my version here.
+
+We'll go over three proofs today:
+
+- $\\{x \mid x \in \mathbb{Z} \wedge x^2 = 9\\} = \\{-3, 3\\}$
+- $\\{x \mid x \in \mathbb{Z} \wedge -4 \le n \wedge n \le 15 ∧ Even~n \\} = \\{-4, -2, 0, 2, 4, 6, 8, 10, 12, 14\\}$
+- $\\{x \mid x \in \mathbb{Z} \wedge x^2 = 6\\} = \emptyset$
+
+## Example 1
+
+First, let's define our set $A$
+
+```lean4
+def A : Set Int := {x : Int | x^2 = 9}
+```
+
+We want to prove the following lemma:
+
+```lean4
+lemma instA : A = ({3, -3} : Finset ℤ)
+```
+
+Recall that for sets, $A = S \iff A \subseteq S \wedge S \subseteq A$.
+
+Since we're given a specific Finset for $S$, it would be really nice if we can compute whether $S$ is a subset of $A$. In fact we can, as long as we prove a couple theorems first.
+
+```lean4
+instance (n: Int) : Decidable (n ∈ A) := by
+  suffices Decidable (n^2 = 9) by
+    rewrite [A, Set.mem_setOf_eq]
+    assumption
+  apply inferInstance
+```
+
+First as shown above, we need to decide whether an integer is in $A$. Given how $A$ is defined, this is equivalent to seeing if $n^2 = 9$. Luckily for us, the core of Lean already has a decision procedure for this. We can have Lean apply the appropriate one by calling `apply inferInstance`.
+
+With this, we can now use `#eval` to see if elements are in $A$ or not.
+
+```lean4
+#eval List.Forall (· ∈ A) [-3, 3]
+```
+
+To say that a finite set $S$ is a subset of $A$, is to say that all the elements of $S$ are in $A$. Using the last theorem, we can prove that checking subsets in this direction is decidable.
+
+```lean4
+instance (S : Finset Int) : Decidable (↑S ⊆ A) := by
+  rewrite [A]
+  rewrite [Set.subset_def]
+  show Decidable (∀ x ∈ S, x ∈ {x | x ^ 2 = 9})
+  apply inferInstance
+```
+
+Keep in mind that at this point it's not necessarily decidable if $A \subseteq S$. This is because we haven't established if $A$ is finite. However instead of trying to prove finiteness, let's skip to the main proof and show that $A = \\{3, -3\\}$ classically.
+
+```lean4
+lemma instA : A = ({3, -3} : Finset ℤ) := by
+  let S : Finset ℤ := {3, -3}
+  change (A = ↑S)
+```
+
+As stated before, set equality is making sure both are subsets of each other
+
+```lean4
+suffices A ⊆ ↑S ∧ ↑S ⊆ A by
+  rewrite [Set.Subset.antisymm_iff]
+  assumption
+```
+
+Lets make use of our decidability proof to show $S \subseteq A$ in one line!
+
+```lean4
+have H2 : ↑S ⊆ A := by decide
+```
+
+For the other side,
+
+```lean4
+have H1 : A ⊆ ↑S := by
+  intro (n : ℤ)
+  -- Goal is now (n ∈ A → n ∈ {3, -3})
+  intro (H1_1: n ∈ A)
+```
+
+Let's change `H1_1` to be in a form easier to work with
+
+```lean4
+have H1_1 : n^2 = 9 := by
+  rewrite [A, Set.mem_setOf_eq] at H1_1
+  assumption
+```
+
+To show that $n \in \\{3, -3\\}$, then it's the same as saying that $n = 3$ or $n = -3$.
+
+```lean4
+suffices n = 3 ∨ n = -3 by
+  show n ∈ S
+  rewrite [Finset.mem_insert, Finset.mem_singleton]
+  assumption
+```
+
+We can show this using a theorem from mathlib!
+
+```lean4
+exact eq_or_eq_neg_of_sq_eq_sq n 3 H1_1
+```
+
+[(Quite the long name...)](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GroupPower/Ring.html#eq_or_eq_neg_of_sq_eq_sq)
+
+Lastly, we combine the two subset proofs to show equality
+
+```lean4
+exact And.intro H1 H2
+```
+
+All together the proof looks like:
+
+```lean4
+lemma instA : A = ({3, -3} : Finset ℤ) := by
+  let S : Finset ℤ := {3, -3}
+  change (A = ↑S)
+
+  suffices A ⊆ ↑S ∧ ↑S ⊆ A by
+    rewrite [Set.Subset.antisymm_iff]
+    assumption
+
+  have H1 : A ⊆ ↑S := by
+    intro (n : ℤ)
+    -- Goal is now (n ∈ A → n ∈ {3, -3})
+    intro (H1_1: n ∈ A)
+    have H1_1 : n^2 = 9 := by
+      rewrite [A, Set.mem_setOf_eq] at H1_1
+      assumption
+
+    suffices n = 3 ∨ n = -3 by
+      show n ∈ S
+      rewrite [Finset.mem_insert, Finset.mem_singleton]
+      assumption
+
+    exact eq_or_eq_neg_of_sq_eq_sq n 3 H1_1
+
+  have H2 : ↑S ⊆ A := by decide
+
+  exact And.intro H1 H2
+```
+
+## Example 2
+
+We got to cheat a little by applying a `mathlib` theorem in the last example. This one will require a little more technique. First, let's start by defining our set $B$.
+
+```lean4
+def B : Set Int := {n | -4 ≤ n ∧ n ≤ 15 ∧ n % 2 = 0}
+```
+
+As before, we can show that set membership in $B$ is decidable. We can make use of the fact that each condition within it is decidable through `And.decidable`.
+
+```lean4
+instance (n : Int) : Decidable (n ∈ B) := by
+  suffices Decidable (-4 ≤ n ∧ n ≤ 15 ∧ n % 2 = 0) by
+    rewrite [B, Set.mem_setOf_eq]
+    assumption
+
+  exact And.decidable
+```
+
+Sanity check to see that everything works as expected.
+
+```lean4
+#eval List.Forall (· ∈ B) [-4, -2, 0, 2, 4, 6, 8, 10, 12, 14]
+```
+
+We can also show that checking if a finset is a subset of $B$ is decidable.
+
+```lean4
+instance (S : Finset Int) : Decidable (↑S ⊆ B) := by
+  suffices Decidable (∀ x ∈ S, -4 ≤ x ∧ x ≤ 15 ∧ x % 2 = 0) by
+    rewrite [Set.subset_def, B]
+    assumption
+  apply inferInstance
+```
+
+The beginning of our proof stays the same
+
+```lean4
+lemma instB : B = ({-4, -2, 0, 2, 4, 6, 8, 10, 12, 14} : Finset Int) := by
+  let S : Finset Int := {-4, -2, 0, 2, 4, 6, 8, 10, 12, 14}
+  change (B = ↑S)
+
+  -- To show equality, we need to show that
+  -- each is a subset of each other
+  suffices ((B ⊆ ↑S) ∧ (↑S ⊆ B)) by
+    rewrite [Set.Subset.antisymm_iff]
+    assumption
+ 
+  have H2 : ↑S ⊆ B := by decide
+```
+
+For the other direction we want to show that is $n$ meets the condition to be in $B$, then it must be in $S$.
+
+```lean4
+have H1 : B ⊆ ↑S := by
+  intro (n : ℤ)
+  intro (H : n ∈ B)
+
+  have H1 : -4 ≤ n ∧ n ≤ 15 ∧ n % 2 = 0 := by
+    rewrite [B] at H; assumption
+  clear H
+
+  show n ∈ S
+```
+
+Since $S$ is a finset, we can say that $n$ must be equal to one of the elements of $S$. 
+
+```lean4
+repeat rewrite [Finset.mem_insert]
+rewrite [Finset.mem_singleton]
+```
+
+At this point, the problem is integer arithmetic and we can call the `omega` tactic to finish the subproof.
+
+```lean4
+omega
+```
+
+With both sides subset proven, we use and introduction to prove the goal
+
+```lean4
+exact show ((B ⊆ ↑S) ∧ (↑S ⊆ B)) from And.intro H1 H2
+```
+
+The full proof is below.
+
+```lean4
+lemma instB : B = ({-4, -2, 0, 2, 4, 6, 8, 10, 12, 14} : Finset Int) := by
+  let S : Finset Int := {-4, -2, 0, 2, 4, 6, 8, 10, 12, 14}
+  change (B = ↑S)
+
+  -- To show equality, we need to show that
+  -- each is a subset of each other
+  suffices ((B ⊆ ↑S) ∧ (↑S ⊆ B)) by
+    rewrite [Set.Subset.antisymm_iff]
+    assumption
+
+  have H1 : B ⊆ ↑S := by
+    intro (n : ℤ)
+    intro (H : n ∈ B)
+
+    have H1 : -4 ≤ n ∧ n ≤ 15 ∧ n % 2 = 0 := by
+      rewrite [B] at H; assumption
+    clear H
+
+    show n ∈ S
+    repeat rewrite [Finset.mem_insert]
+    rewrite [Finset.mem_singleton]
+    omega
+
+  have H2 : ↑S ⊆ B := by decide
+
+  exact show ((B ⊆ ↑S) ∧ (↑S ⊆ B)) from And.intro H1 H2
+```
+
+## Example 3
+
+Finally let's define our last set.
+
+```lean4
+def C : Set Int := {n | n^2 = 6}
+```
+
+We're aiming to show that $C$ is equivalent to the empty set. Therefore, we don't have a need to show decidability for membership or finite subsets. We can't make use of the mathlib theorem from Example 1, so how will we go about proving this?
+
+Analyzing the last example more carefully, we had upper and lower bounds to work with. We can similarly identify these bounds for this example.
+
+Let's define the integer squared to be the upper bound.
+
+```lean4
+lemma IntPow2GeSelf (H : (a : Int)^2 = z) : a ≤ z := by
+  have H1 : a ≤ a ^ 2 := Int.le_self_sq a
+  rewrite [H] at H1
+  assumption
+```
+
+For the lower bound, take its negation.
+
+```lean4
+lemma NegIntPow2LeSelf (H : (a : Int)^2 = z) : a ≥ -z := by
+```
+
+To prove the lower bound, split up between positives and negatives using the law of excluded middle
+
+```lean4
+have H1 : a ≥ 0 ∨ a < 0 := le_or_lt 0 a
+```
+
+For a positive $a$, we can rely on the `linarith` tactic
+
+```lean4
+have H_LEFT : a ≥ 0 → a ≥ -z := by
+  have HL1 : a ≤ z := IntPow2GeSelf H
+  intro (HL2 : a ≥ 0)
+  linarith
+```
+
+For a negative $a$, we need to prove it by induction
+
+```lean4
+have H_RIGHT : a < 0 → a ≥ -z := by
+  intro (HR1: a < 0)
+  have HR1 : a ≤ -1 := Int.le_sub_one_iff.mpr HR1
+  revert HR1
+
+  suffices a ≤ -1 → a ≥ -(a^2) by
+    rewrite [<- H]; assumption
+
+  let P : ℤ → Prop := fun x => x ≥ -(x^2)
+
+  have H_base : P (-1) := by decide
+
+  have H_ind : ∀ (n : ℤ), n ≤ -1 → P n → P (n - 1) := by
+    intro (n : ℤ)
+    intro (H21 : n ≤ -1)
+    intro (H22 : P n)
+    simp_all
+    linarith
+
+  exact Int.le_induction_down H_base H_ind a
+```
+
+We have shown that this lower bound holds for both positive and negative $a$, therefore we can show that it holds for all $a$.
+
+```lean4
+exact Or.elim H1 H_LEFT H_RIGHT
+```
+
+All together the lower bound proof is the following
+
+```lean4
+lemma NegIntPow2LeSelf (H : (a : Int)^2 = z) : a ≥ -z := by
+  have H1 : a ≥ 0 ∨ a < 0 := by omega
+
+  have H_LEFT : a ≥ 0 → a ≥ -z := by
+    have HL1 : a ≤ z := IntPow2GeSelf H
+    intro (HL2 : a ≥ 0)
+    linarith
+
+  have H_RIGHT : a < 0 → a ≥ -z := by
+    intro (HR1: a < 0)
+    have HR1 : a ≤ -1 := Int.le_sub_one_iff.mpr HR1
+    revert HR1
+
+    suffices a ≤ -1 → a ≥ -(a^2) by
+      rewrite [<- H]; assumption
+
+    let P : ℤ → Prop := fun x => x ≥ -(x^2)
+
+    have H_base : P (-1) := by decide
+
+    have H_ind : ∀ (n : ℤ), n ≤ -1 → P n → P (n - 1) := by
+      intro (n : ℤ)
+      intro (H21 : n ≤ -1)
+      intro (H22 : P n)
+      simp_all
+      linarith
+
+    exact Int.le_induction_down H_base H_ind a
+
+
+  exact Or.elim H1 H_LEFT H_RIGHT
+```
+
+With our lower and upper bounds in place, we can look at the original problem. That is, we want to prove that $C = \emptyset$. We'll start the same proof like before.
+
+```lean4
+example : C = (∅ : Set Int) := by
+  suffices C ⊆ ∅ ∧ ∅ ⊆ C by
+    rewrite [Set.Subset.antisymm_iff]
+    assumption
+  have H2 : ∅ ⊆ C := Set.empty_subset C
+```
+
+We start the other direction the same as well.
+
+```lean4
+have H1 : C ⊆ ∅ := by
+  intro (n : ℤ)
+  intro (H1_1 : n ∈ C)
+  have H1_1 : n^2 = 6 := by
+    rewrite [C, Set.mem_setOf_eq] at H1_1
+    assumption
+```
+
+Now bring in our bounds
+
+```lean4
+have H1_2 : n ≤ 6 := by apply IntPow2GeSelf H1_1
+have H2_3 : n ≥ -6 := by apply NegIntPow2LeSelf H1_1
+```
+
+We can use `omega` to show that if the integer is within these bounds then $n$ must equal one of the integers. 
+
+```lean4
+have H1_4 :  n ∈ ({-6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6} : Finset ℤ) := by
+  repeat rewrite [Finset.mem_insert]
+  rewrite [Finset.mem_singleton]
+  omega
+```
+
+Turn this set into a disjunction
+
+```lean4
+-- Make H1_4 a disjunction (n = -6 ∨ ... ∨ n = 6)
+repeat rewrite [Finset.mem_insert] at H1_4
+rewrite [Finset.mem_singleton] at H1_4
+```
+
+Trying to show that $n$ is within the empty set is the same as trying to prove a contradiction
+
+```lean4
+show False
+```
+
+So let's go through each disjunct in `H1_4` and show that we derive a contradiction.
+
+```lean4
+repeat (
+  cases' H1_4 with H1_4H H1_4
+  -- Plug in n = ?? to n^2 = 6
+  rewrite [H1_4H] at H1_1
+  contradiction
+)
+```
+
+The last $n = 6$ is under a different name
+
+```lean4
+rewrite [H1_4] at H1_1
+contradiction
+```
+
+We can finally put it all together with and introduction
+
+```lean4
+exact show C ⊆ ∅ ∧ ∅ ⊆ C from And.intro H1 H2
+```
+
+All together it's the following:
+
+```lean4
+example : C = (∅ : Set Int) := by
+
+  suffices C ⊆ ∅ ∧ ∅ ⊆ C by
+    rewrite [Set.Subset.antisymm_iff]
+    assumption
+
+  have H1 : C ⊆ ∅ := by
+    intro (n : ℤ)
+    intro (H1_1 : n ∈ C)
+    have H1_1 : n^2 = 6 := by
+      rewrite [C, Set.mem_setOf_eq] at H1_1
+      assumption
+
+    show False
+
+    have H1_2 : n ≤ 6 := by apply IntPow2GeSelf H1_1
+    have H2_3 : n ≥ -6 := by apply NegIntPow2LeSelf H1_1
+
+
+    have H1_4 :  n ∈ ({-6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6} : Finset ℤ) := by
+      repeat rewrite [Finset.mem_insert]
+      rewrite [Finset.mem_singleton]
+      omega
+
+    -- Make H3 a disjunction (n = -6 ∨ ... ∨ n = 6)
+    repeat rewrite [Finset.mem_insert] at H1_4
+    rewrite [Finset.mem_singleton] at H1_4
+
+    -- Try each one, plug in n = a into n^2 = 6 and show it doesn't work
+    repeat (
+      cases' H1_4 with H1_4H H1_4
+      rewrite [H1_4H] at H1_1
+      contradiction
+    )
+
+    -- Last n = 6 has a different name
+    rewrite [H1_4] at H1_1
+    contradiction
+
+
+  have H2 : ∅ ⊆ C := Set.empty_subset C
+
+  exact show C ⊆ ∅ ∧ ∅ ⊆ C from And.intro H1 H2
+```
+
+## Conclusion
+
+We gave three examples on working with finite integer sets. The two key lessons from this post are:
+
+**1. If the set is equal to a non-empty finite set, then try to prove decidability of membership and if a finset is a subset of it.**
+
+If you're looking at a set of integers and this set is constructed with conditions that are mostly built-in (such as the `<` relation), then this is hopefully not too difficult. Unfold the definitions of your set using `rewrite` and have Lean auto-infer which decidability instance to call using `apply inferInstance`
+
+**2. Try to establish a lower and upper bound for the elements of your set.**
+
+This gives the `omega` tactic something additional to work with. In the second example, `omega` was able to close out the goal completely given the linear inequalities presented. In our last example, we only used `omega` to construct a finite set of possible integers.
+
+If you develop any other general techniques for dealing with integer sets let me know. Otherwise, feel free to get in touch with any questions you have.
+