From 3658d1db1fa979c00cc6cb93188f64928ecd746d Mon Sep 17 00:00:00 2001
From: George Tsoukalas <george.tsoukalas@utexas.edu>
Date: Sat, 3 Aug 2024 16:01:05 +0000
Subject: [PATCH] Caught some stragglers.

---
 lean4/src/putnam_1971_b2.lean | 3 ++-
 lean4/src/putnam_1974_b6.lean | 3 ++-
 lean4/src/putnam_1980_b5.lean | 3 ++-
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/lean4/src/putnam_1971_b2.lean b/lean4/src/putnam_1971_b2.lean
index a4c84b34..f70b6a7f 100644
--- a/lean4/src/putnam_1971_b2.lean
+++ b/lean4/src/putnam_1971_b2.lean
@@ -8,6 +8,7 @@ abbrev putnam_1971_b2_solution : Set (ℝ → ℝ) := sorry
 theorem putnam_1971_b2
 (S : Set ℝ)
 (hS : S = univ \ {0, 1})
-(P : (ℝ → ℝ) → Prop := fun (F : ℝ → ℝ) => ∀ x ∈ S, F x + F ((x - 1)/x) = 1 + x)
+(P : (ℝ → ℝ) → Prop)
+(hP : P = fun (F : ℝ → ℝ) => ∀ x ∈ S, F x + F ((x - 1)/x) = 1 + x)
 : (∀ F ∈ putnam_1971_b2_solution, P F) ∧ ∀ f : ℝ → ℝ, P f → ∃ F ∈ putnam_1971_b2_solution, (∀ x ∈ S, f x = F x) :=
 sorry
diff --git a/lean4/src/putnam_1974_b6.lean b/lean4/src/putnam_1974_b6.lean
index 9f5923e0..aabac694 100644
--- a/lean4/src/putnam_1974_b6.lean
+++ b/lean4/src/putnam_1974_b6.lean
@@ -6,7 +6,8 @@ open Set Nat Polynomial Filter Topology
 abbrev putnam_1974_b6_solution : (ℕ × ℕ × ℕ) := sorry
 -- ((2^1000 - 1)/3, (2^1000 - 1)/3, 1 + (2^1000 - 1)/3)
 theorem putnam_1974_b6
-(n : ℤ := 1000)
+(n : ℤ)
+(hn : n = 1000)
 (count0 count1 count2 : ℕ)
 (hcount0 : count0 = {S | S ⊆ Finset.Icc 1 n ∧ S.card ≡ 0 [MOD 3]}.ncard)
 (hcount1 : count1 = {S | S ⊆ Finset.Icc 1 n ∧ S.card ≡ 1 [MOD 3]}.ncard)
diff --git a/lean4/src/putnam_1980_b5.lean b/lean4/src/putnam_1980_b5.lean
index b90c07a5..876e7fbf 100644
--- a/lean4/src/putnam_1980_b5.lean
+++ b/lean4/src/putnam_1980_b5.lean
@@ -6,7 +6,8 @@ open Set
 abbrev putnam_1980_b5_solution : ℝ → Prop := sorry
 -- fun t : ℝ => 1 ≥ t
 theorem putnam_1980_b5
-(T : Set ℝ := Icc 0 1)
+(T : Set ℝ)
+(hT : T = Icc 0 1)
 (P : ℝ → (ℝ → ℝ) → Prop)
 (Convex : (ℝ → ℝ) → Prop)
 (S : ℝ → Set (ℝ → ℝ))