Fix a few minor Lean misformalisations

lean4/src/putnam_1991_a6.lean

@@ -9,12 +9,12 @@ theorem putnam_1991_a6
 (agt bge bg1 bg2 : ℕ × (ℕ → ℕ) → Prop)
 (A g B: ℕ → ℕ)
 (hnabsum : ∀ n ≥ 1, ∀ ab : ℕ × (ℕ → ℕ), nabsum n ab = (ab.1 ≥ 1 ∧ (∀ i < ab.1, ab.2 i > 0) ∧ (∀ i ≥ ab.1, ab.2 i = 0) ∧ (∑ i : Fin ab.1, ab.2 i) = n))
-(hagt : ∀ a : ℕ × (ℕ → ℕ), agt a = (∀ i : Fin (a.1 - 2), a.2 i > a.2 (i + 1) + a.2 (i + 2)) ∧ a.2 (a.1 - 2) > a.2 (a.1 - 1))
+(hagt : ∀ a : ℕ × (ℕ → ℕ), agt a ↔ (∀ i : Fin (a.1 - 2), a.2 i > a.2 (i + 1) + a.2 (i + 2)) ∧ 1 < a.1 → a.2 (a.1 - 2) > a.2 (a.1 - 1))
 (hA : ∀ n ≥ 1, A n = {a : ℕ × (ℕ → ℕ) | nabsum n a ∧ agt a}.encard)
 (hbge : ∀ b : ℕ × (ℕ → ℕ), bge b = ∀ i : Fin (b.1 - 1), b.2 i ≥ b.2 (i + 1))
 (hg : g 0 = 1 ∧ g 1 = 2 ∧ (∀ j ≥ 2, g j = g (j - 1) + g (j - 2) + 1))
-(hbg1 : ∀ b : ℕ × (ℕ → ℕ), bg1 b = ∀ i : Fin b.1, ∃ j : ℕ, b.2 i = g j)
-(hbg2 : ∀ b : ℕ × (ℕ → ℕ), bg2 b = ∃ k : ℕ, b.2 0 = g k ∧ (∀ j ≤ k, ∃ i : Fin b.1, b.2 i = g j))
+(hbg1 : ∀ b : ℕ × (ℕ → ℕ), bg1 b ↔ ∀ i : Fin b.1, ∃ j : ℕ, b.2 i = g j)
+(hbg2 : ∀ b : ℕ × (ℕ → ℕ), bg2 b ↔ ∃ k : ℕ, b.2 0 = g k ∧ (∀ j ≤ k, ∃ i : Fin b.1, b.2 i = g j))
 (hB : ∀ n ≥ 1, B n = {b : ℕ × (ℕ → ℕ) | nabsum n b ∧ bge b ∧ bg1 b ∧ bg2 b}.encard)
 : ∀ n ≥ 1, A n = B n :=
 sorry