diff --git a/lean4/src/putnam_2012_a4.lean b/lean4/src/putnam_2012_a4.lean
index 8a9a6c6..9834700 100644
--- a/lean4/src/putnam_2012_a4.lean
+++ b/lean4/src/putnam_2012_a4.lean
@@ -6,13 +6,17 @@ open Matrix Function
 Let $q$ and $r$ be integers with $q>0$, and let $A$ and $B$ be intervals on the real line. Let $T$ be the set of all $b+mq$ where $b$ and $m$ are integers with $b$ in $B$, and let $S$ be the set of all integers $a$ in $A$ such that $ra$ is in $T$. Show that if the product of the lengths of $A$ and $B$ is less than $q$, then $S$ is the intersection of $A$ with some arithmetic progression.
 -/
 theorem putnam_2012_a4
-(q r : ℤ)
-(A B : Fin 2 → ℝ)
-(T : Set ℝ)
-(S : Set ℤ)
-(qpos : q > 0)
-(ABlt : A 0 < A 1 ∧ B 0 < B 1)
-(hT : T = {x : ℝ | ∃ b m : ℤ, ((b : ℝ) ∈ Set.Icc (B 0) (B 1)) ∧ (x = b + m * q)})
-(hS : S = {a : ℤ | ((a : ℝ) ∈ Set.Icc (A 0) (A 1)) ∧ (∃ t ∈ T, r * a = t)})
-: ((A 1 - A 0) * (B 1 - B 0) < q) → (∃ n : ℕ, ∃ a1 d : ℝ, n > 2 ∧ {s : ℝ | s = round s ∧ round s ∈ S} = (Set.Icc (A 0) (A 1)) ∩ {x : ℝ | ∃ i : Fin n, x = a1 + i * d}) :=
-sorry
+    (IsFiniteAP : Set ℤ → Prop)
+    (IsFiniteAP_def : ∀ s,
+      IsFiniteAP s ↔ ∃ n : ℕ, ∃ a d : ℤ, 0 < d ∧ s = {a + i * d | i : Fin n})
+    (q r : ℤ)
+    (A B : Fin 2 → ℝ)
+    (T : Set ℤ)
+    (S : Set ℤ)
+    (qpos : q > 0)
+    (ABlt : A 0 < A 1 ∧ B 0 < B 1)
+    (hT : T = {x : ℤ | ∃ b m : ℤ, (b : ℝ) ∈ Set.Icc (B 0) (B 1) ∧ x = b + m * q})
+    (hS : S = {a : ℤ | (a : ℝ) ∈ Set.Icc (A 0) (A 1) ∧ r * a ∈ T})
+    (prod_lt : (A 1 - A 0) * (B 1 - B 0) < q) :
+    IsFiniteAP {x | x ∈ S ∧ (x : ℝ) ∈ Set.Icc (A 0) (A 1)} :=
+  sorry