fixed statement of main3

Eaton, I'll let you decide if you want to include main3 in your slides or not

FriezePatterns/chapter3.lean

@@ -467,11 +467,16 @@ lemma main2 (n : ℕ) (hn : n ≠ 0) : ∃ (f : ℕ × ℕ → ℚ) (hf : arith_
     rw [hk]
     assumption
 
-theorem main3 (n : ℕ) (hn: n≠ 0) : ∀ (f : ℕ × ℕ → ℚ) (hf : arith_fp f n), ∀ (a : ℕ × ℕ),
-f a ≥ Nat.fib n → f a = Nat.fib n := by
-  intro f hf ⟨i,m⟩
-  have h : f (i,m) ≤ Nat.fib n := main1 n hn f hf (i,m)
-  intro h'
-  linarith
-
-
+theorem main3 (n : ℕ) (hn: n≠ 0) : ∃ (g : ℕ × ℕ → ℚ) (_ : arith_fp g n), ∃ (b : ℕ × ℕ ), (∀ (f : ℕ × ℕ → ℚ) (_ : arith_fp f n), ∀ (a : ℕ × ℕ),
+(f a ≥ g b → f a = g b)) ∧ g b = Nat.fib n := by
+  have h : ∃ (g : ℕ × ℕ → ℚ) (_ : arith_fp g n), ∃ (b : ℕ × ℕ), g b = Nat.fib n := main2 n hn
+  choose g hg b hb using h
+  use g; use hg; use b
+  constructor
+  · intro f hf ⟨i,m⟩
+    have h : f (i,m) ≤ g b := by
+      calc f (i,m) ≤ Nat.fib n := main1 n hn f hf (i,m)
+      _ = g b := by rw [hb]
+    intro h'
+    linarith
+  · exact hb