Merge pull request #193 from trishullab/george

optParam and notational improvements.

lean4/src/putnam_1962_a2.lean

@@ -6,8 +6,10 @@ open MeasureTheory
 abbrev putnam_1962_a2_solution : Set (ℝ → ℝ) := sorry
 -- {f : ℝ → ℝ | ∃ a c : ℝ, a > 0 ∧ f = fun x => a / (1 - c * x)^2}
 theorem putnam_1962_a2
-(hf : ℝ → (ℝ → ℝ) → Prop := fun (e : ℝ) (f : ℝ → ℝ) => ∀ x ∈ Set.Ioo 0 e, (⨍ v in Set.Icc 0 x, f v) = Real.sqrt ((f 0) * (f x)))
-(hfinf : (ℝ → ℝ) → Prop := fun (f : ℝ → ℝ) => ∀ x > 0, (⨍ v in Set.Icc 0 x, f v) = Real.sqrt ((f 0) * (f x)))
+(hf : ℝ → (ℝ → ℝ) → Prop)
+(hf_def : hf = fun (e : ℝ) (f : ℝ → ℝ) => ∀ x ∈ Set.Ioo 0 e, (⨍ v in Set.Icc 0 x, f v) = Real.sqrt ((f 0) * (f x)))
+(hfinf : (ℝ → ℝ) → Prop)
+(hfinf_def : hfinf = fun (f : ℝ → ℝ) => ∀ x > 0, (⨍ v in Set.Icc 0 x, f v) = Real.sqrt ((f 0) * (f x)))
 : (∀ f : ℝ → ℝ, (hfinf f → ∃ g ∈ putnam_1962_a2_solution, ∀ x ≥ 0, g x = f x) ∧
 ∀ e > 0, hf e f → ∃ g ∈ putnam_1962_a2_solution, ∀ x ∈ Set.Ico 0 e, g x = f x) ∧
 ∀ f ∈ putnam_1962_a2_solution, hfinf f ∨ (∃ e > 0, hf e f) :=

lean4/src/putnam_1962_a4.lean

@@ -1,8 +1,6 @@
 import Mathlib
 open BigOperators
 
-open MeasureTheory
-
 theorem putnam_1962_a4
 (f : ℝ → ℝ)
 (a b : ℝ)

lean4/src/putnam_1962_a5.lean

@@ -1,8 +1,6 @@
 import Mathlib
 open BigOperators
 
-open MeasureTheory
-
 abbrev putnam_1962_a5_solution : ℕ → ℕ := sorry
 -- fun n : ℕ => n * (n + 1) * 2^(n - 2)
 theorem putnam_1962_a5

lean4/src/putnam_1962_a6.lean

@@ -1,8 +1,6 @@
 import Mathlib
 open BigOperators
 
-open MeasureTheory
-
 theorem putnam_1962_a6
 (S : Set ℚ)
 (hSadd : ∀ a ∈ S, ∀ b ∈ S, a + b ∈ S)

lean4/src/putnam_1962_b1.lean

@@ -1,8 +1,6 @@
 import Mathlib
 open BigOperators
 
-open MeasureTheory
-
 theorem putnam_1962_b1
 (p : ℕ → ℝ → ℝ)
 (x y : ℝ)

lean4/src/putnam_1962_b6.lean

@@ -1,14 +1,14 @@
 import Mathlib
 open BigOperators
 
-open MeasureTheory
+open MeasureTheory Real
 
 theorem putnam_1962_b6
-(π : ℝ := Real.pi)
 (n : ℕ)
 (a b : ℕ → ℝ)
 (xs : Set ℝ)
-(f : ℝ → ℝ := fun x : ℝ => ∑ k in Finset.Icc 0 n, ((a k) * Real.sin (k * x) + (b k) * Real.cos (k * x)))
+(f : ℝ → ℝ)
+(hf : f = fun x : ℝ => ∑ k in Finset.Icc 0 n, ((a k) * Real.sin (k * x) + (b k) * Real.cos (k * x)))
 (hf1 : ∀ x ∈ Set.Icc 0 (2 * π), |f x| ≤ 1)
 (hxs : xs.ncard = 2 * n ∧ xs ⊆ Set.Ico 0 (2 * π))
 (hfxs : ∀ x ∈ xs, |f x| = 1)

lean4/src/putnam_1963_a3.lean

@@ -8,10 +8,12 @@ noncomputable abbrev putnam_1963_a3_solution : (ℝ → ℝ) → ℕ → ℝ →
 theorem putnam_1963_a3
 (n : ℕ)
 (f : ℝ → ℝ)
-(P : ℕ → (ℝ → ℝ) → (ℝ → ℝ))
-(δ : (ℝ → ℝ) → (ℝ → ℝ) := fun g : ℝ → ℝ ↦ (fun x : ℝ ↦ x) * deriv g)
-(D : ℕ → (ℝ → ℝ) → (ℝ → ℝ) := fun (m : ℕ) (g : ℝ → ℝ) ↦ δ g - (fun x : ℝ ↦ (m : ℝ)) * g)
-(y : ℝ → ℝ := fun x : ℝ ↦ ∫ t in Set.Ioo 1 x, putnam_1963_a3_solution f n x t)
+(P D : ℕ → (ℝ → ℝ) → (ℝ → ℝ))
+(δ : (ℝ → ℝ) → (ℝ → ℝ))
+(hδ : δ = fun g : ℝ → ℝ ↦ (fun x : ℝ ↦ x) * deriv g)
+(hD : D = fun (m : ℕ) (g : ℝ → ℝ) ↦ δ g - (fun x : ℝ ↦ (m : ℝ)) * g)
+(y : ℝ → ℝ)
+(hy : y = fun x : ℝ ↦ ∫ t in Set.Ioo 1 x, putnam_1963_a3_solution f n x t)
 (hn : n ≥ 1)
 (hf : Continuous f)
 (hP : P 0 y = y ∧ ∀ m ∈ Finset.range n, P (m + 1) y = D (n - 1 - m) (P m y))

lean4/src/putnam_1963_a4.lean

@@ -4,7 +4,9 @@ open BigOperators
 open Topology Filter
 
 theorem putnam_1963_a4
-(apos : (ℕ → ℝ) → Prop := fun a => ∀ n, a n > 0)
-(f : (ℕ → ℝ) → ℕ → ℝ := fun a n => n * (((1 + a (n+1)) / (a n)) - 1))
+(apos : (ℕ → ℝ) → Prop)
+(hapos : apos = fun a => ∀ n, a n > 0)
+(f : (ℕ → ℝ) → ℕ → ℝ)
+(hf : f = fun (a : ℕ → ℝ) n => n * (((1 + a (n+1)) / (a n)) - 1))
 : (∀ a, apos a → limsup (f a) atTop ≥ 1) ∧ (¬∃ c > 1, ∀ a, apos a → limsup (f a) atTop ≥ c) :=
 sorry

lean4/src/putnam_1963_a6.lean

@@ -6,8 +6,10 @@ open Topology Filter
 theorem putnam_1963_a6
 (F1 F2 U V A B C D P Q : EuclideanSpace ℝ (Fin 2))
 (r : ℝ)
-(E : Set (Fin 2 → ℝ) := {H : EuclideanSpace ℝ (Fin 2) | dist F1 H + dist F2 H = r})
-(M : EuclideanSpace ℝ (Fin 2) := midpoint ℝ U V)
+(E : Set (EuclideanSpace ℝ (Fin 2)))
+(hE : E = {H : EuclideanSpace ℝ (Fin 2) | dist F1 H + dist F2 H = r})
+(M : EuclideanSpace ℝ (Fin 2))
+(hM : M = midpoint ℝ U V)
 (hr : r > dist F1 F2)
 (hUV : U ∈ E ∧ V ∈ E ∧ U ≠ V)
 (hAB : A ∈ E ∧ B ∈ E ∧ A ≠ B)

lean4/src/putnam_1963_b2.lean

@@ -6,7 +6,7 @@ open Topology Filter Polynomial
 abbrev putnam_1963_b2_solution : Prop := sorry
 -- True
 theorem putnam_1963_b2
-(S : Set ℝ := {2 ^ m * 3 ^ n | (m : ℤ) (n : ℤ)})
-(P : Set ℝ := Set.Ioi 0)
-: closure S ⊇ P ↔ putnam_1963_b2_solution :=
+(S : Set ℝ)
+(hS : S = {2 ^ m * 3 ^ n | (m : ℤ) (n : ℤ)})
+: closure S ⊇ Set.Ioi (0 : ℝ) ↔ putnam_1963_b2_solution :=
 sorry

lean4/src/putnam_1963_b3.lean

@@ -7,6 +7,7 @@ abbrev putnam_1963_b3_solution : Set (ℝ → ℝ) := sorry
 -- {(fun u : ℝ => A * Real.sinh (k * u)) | (A : ℝ) (k : ℝ)} ∪ {(fun u : ℝ => A * u) | A : ℝ} ∪ {(fun u : ℝ => A * Real.sin (k * u)) | (A : ℝ) (k : ℝ)}
 theorem putnam_1963_b3
 (f : ℝ → ℝ)
-(fdiff : Prop := ContDiff ℝ 1 f ∧ Differentiable ℝ (deriv f))
+(fdiff : Prop)
+(hfdiff : fdiff ↔ ContDiff ℝ 1 f ∧ Differentiable ℝ (deriv f))
 : (fdiff ∧ ∀ x y : ℝ, (f x) ^ 2 - (f y) ^ 2 = f (x + y) * f (x - y)) ↔ f ∈ putnam_1963_b3_solution :=
 sorry

lean4/src/putnam_1963_b6.lean

@@ -5,7 +5,8 @@ open Topology Filter Polynomial
 
 theorem putnam_1963_b6
 (d : ℕ)
-(S : Set (Fin d → ℝ) → Set (Fin d → ℝ) := (fun A : Set (Fin d → ℝ) => ⋃ p ∈ A, ⋃ q ∈ A, segment ℝ p q))
+(S : Set (Fin d → ℝ) → Set (Fin d → ℝ))
+(hS : S = (fun A : Set (Fin d → ℝ) => ⋃ p ∈ A, ⋃ q ∈ A, segment ℝ p q))
 (A : ℕ → Set (Fin d → ℝ))
 (ddim : 1 ≤ d ∧ d ≤ 3)
 (hA0 : Nonempty (A 0))

lean4/src/putnam_1964_a1.lean

@@ -4,6 +4,7 @@ open BigOperators
 theorem putnam_1964_a1
 (A : Finset (EuclideanSpace ℝ (Fin 2)))
 (hAcard : A.card = 6)
-(dists : Set ℝ := {d : ℝ | ∃ a b : EuclideanSpace ℝ (Fin 2), a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ d = dist a b})
+(dists : Set ℝ)
+(hdists : dists = {d : ℝ | ∃ a b : EuclideanSpace ℝ (Fin 2), a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ d = dist a b})
 : (sSup dists / sInf dists ≥ Real.sqrt 3) :=
 sorry

lean4/src/putnam_1964_a3.lean

@@ -7,7 +7,7 @@ theorem putnam_1964_a3
 (x a b : ℕ → ℝ)
 (hxdense : range x ⊆ Ioo 0 1 ∧ closure (range x) ⊇ Ioo 0 1)
 (hxinj : Injective x)
-(a := fun n ↦ x n - sSup ({0} ∪ {p : ℝ | p < x n ∧ ∃ i < n, p = x i}))
-(b := fun n ↦ sInf ({1} ∪ {p : ℝ | p > x n ∧ ∃ i < n, p = x i}) - x n)
+(ha : a = fun n ↦ x n - sSup ({0} ∪ {p : ℝ | p < x n ∧ ∃ i < n, p = x i}))
+(hb : b = fun n ↦ sInf ({1} ∪ {p : ℝ | p > x n ∧ ∃ i < n, p = x i}) - x n)
 : (∑' n : ℕ, a n * b n * (a n + b n) = 1 / 3) :=
 sorry

lean4/src/putnam_1964_a5.lean

@@ -4,6 +4,7 @@ open BigOperators
 open Set Function Filter Topology
 
 theorem putnam_1964_a5
-(pa : (ℕ → ℝ) → Prop := fun a ↦ (∀ n : ℕ, a n > 0) ∧ ∃ L : ℝ, Tendsto (fun N ↦ ∑ n in Finset.range N, 1 / a n) atTop (𝓝 L))
+(pa : (ℕ → ℝ) → Prop)
+(hpa : pa = fun a ↦ (∀ n : ℕ, a n > 0) ∧ ∃ L : ℝ, Tendsto (fun N ↦ ∑ n in Finset.range N, 1 / a n) atTop (𝓝 L))
 : (∃ k : ℝ, ∀ a : ℕ → ℝ, pa a → ∑' n : ℕ, (n + 1) / (∑ i in Finset.range (n + 1), a i) ≤ k * ∑' n : ℕ, 1 / a n) :=
 sorry

lean4/src/putnam_1964_a6.lean

@@ -5,8 +5,10 @@ open Set Function Filter Topology
 
 theorem putnam_1964_a6
 (S : Finset ℝ)
-(pairs : Set (ℝ × ℝ) := {(a, b) | (a ∈ S) ∧ (b ∈ S) ∧ (a < b)})
-(distance : ℝ × ℝ → ℝ := fun (a, b) ↦ b - a)
+(pairs : Set (ℝ × ℝ))
+(hpairs : pairs = {(a, b) | (a ∈ S) ∧ (b ∈ S) ∧ (a < b)})
+(distance : ℝ × ℝ → ℝ)
+(hdistance : distance = fun (a, b) ↦ b - a)
 (hrepdist : ∀ p ∈ pairs, (∃ m ∈ pairs, distance m > distance p) → ∃ q ∈ pairs, q ≠ p ∧ distance p = distance q)
 : (∀ p q : pairs, q ≠ p → ∃ r : ℚ, distance p / distance q = r) :=
 sorry

lean4/src/putnam_1964_b1.lean

@@ -7,6 +7,7 @@ theorem putnam_1964_b1
 (a : ℕ → ℤ)
 (apos : a > 0)
 (ha : ∃ L : ℝ, Tendsto (fun N ↦ ∑ n in Finset.range N, (1 : ℝ) / a n) atTop (𝓝 L))
-(b : ℕ → ENNReal := fun n ↦ {k : ℕ | a k ≤ n}.encard)
+(b : ℕ → ENNReal)
+(hb : b = fun (n : ℕ) ↦ ({k : ℕ | a k ≤ n}.encard : ENNReal))
 : (Tendsto (fun n : ℕ ↦ b n / n) atTop (𝓝 0)) :=
 sorry

lean4/src/putnam_1964_b6.lean

@@ -4,7 +4,9 @@ open BigOperators
 open Set Function Filter Topology
 
 theorem putnam_1964_b6
-(D : Set (EuclideanSpace ℝ (Fin 2)) := {v : EuclideanSpace ℝ (Fin 2) | dist 0 v ≤ 1})
-(cong : Set (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2)) → Prop := fun A B ↦ ∃ f : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)), B = f '' A ∧ ∀ v w : EuclideanSpace ℝ (Fin 2), dist v w = dist (f v) (f w))
+(D : Set (EuclideanSpace ℝ (Fin 2)))
+(hD : D = {v : EuclideanSpace ℝ (Fin 2) | dist 0 v ≤ 1})
+(cong : Set (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2)) → Prop)
+(hcong : cong = fun A B ↦ ∃ f : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)), B = f '' A ∧ ∀ v w : EuclideanSpace ℝ (Fin 2), dist v w = dist (f v) (f w))
 : (¬∃ A B : Set (Fin 2 → ℝ), cong A B ∧ A ∩ B = ∅ ∧ A ∪ B = D) :=
 sorry

lean4/src/putnam_1965_a1.lean

@@ -1,12 +1,11 @@
 import Mathlib
 open BigOperators
 
-open EuclideanGeometry
+open EuclideanGeometry Real
 
 noncomputable abbrev putnam_1965_a1_solution : ℝ := sorry
 -- Real.pi / 15
 theorem putnam_1965_a1
-(π : ℝ := Real.pi)
 (A B C X Y : EuclideanSpace ℝ (Fin 2))
 (hABC : ¬Collinear ℝ {A, B, C})
 (hangles : ∠ C A B < ∠ B C A ∧ ∠ B C A < π/2 ∧ π/2 < ∠ A B C)

lean4/src/putnam_1965_a6.lean

@@ -5,7 +5,8 @@ open EuclideanGeometry Topology Filter Complex
 
 theorem putnam_1965_a6
 (u v m : ℝ)
-(pinter : ℝ × ℝ → Prop := (fun p : ℝ × ℝ => u*p.1 + v*p.2 = 1 ∧ (p.1)^m + (p.2)^m = 1))
+(pinter : ℝ × ℝ → Prop)
+(hpinter : pinter = (fun p : ℝ × ℝ => u*p.1 + v*p.2 = 1 ∧ (p.1)^m + (p.2)^m = 1))
 (hm : m > 1)
 (huv : u ≥ 0 ∧ v ≥ 0)
 : ((∃! p : ℝ × ℝ, pinter p) ∧ (∃ p : ℝ × ℝ, p.1 ≥ 0 ∧ p.2 ≥ 0 ∧ pinter p)) ↔ (∃ n : ℝ, u^n + v^n = 1 ∧ m^(-(1 : ℤ)) + n^(-(1 : ℤ)) = 1) :=

lean4/src/putnam_1965_b2.lean

@@ -9,7 +9,8 @@ theorem putnam_1965_b2
 (won : Fin n → Fin n → Bool)
 (hirrefl : ∀ i : Fin n, won i i = False)
 (hantisymm : ∀ i j : Fin n, i ≠ j → won i j = ¬won j i)
-(w : Fin n → ℤ := fun r : Fin n => ∑ j : Fin n, (if won r j then 1 else 0))
-(l : Fin n → ℤ := fun r : Fin n => n - 1 - w r)
+(w l : Fin n → ℤ)
+(hw : w = fun r : Fin n => ∑ j : Fin n, (if won r j then 1 else 0))
+(hl : l = fun r : Fin n => n - 1 - w r)
 : ∑ r : Fin n, (w r)^2 = ∑ r : Fin n, (l r)^2 :=
 sorry

lean4/src/putnam_1965_b5.lean

@@ -5,8 +5,8 @@ open EuclideanGeometry Topology Filter Complex SimpleGraph.Walk
 
 theorem putnam_1965_b5
 [Fintype K]
-(V : ℕ := Nat.card K)
-(E : ℕ)
+(V E : ℕ)
+(hV : V = Nat.card K)
 (hE: 4*E ≤ V^2)
 : ∃ G : SimpleGraph K, G.edgeSet.ncard = E ∧ ∀ a : K, ∀ w : G.Walk a a, w.length ≠ 3 :=
 sorry

lean4/src/putnam_1965_b6.lean

@@ -5,9 +5,11 @@ open EuclideanGeometry Topology Filter Complex SimpleGraph.Walk
 
 theorem putnam_1965_b6
 (A B C D : EuclideanSpace ℝ (Fin 2))
-(S : Set (EuclideanSpace ℝ (Fin 2)) := {A, B, C, D})
+(S : Set (EuclideanSpace ℝ (Fin 2)))
+(hS : S = {A, B, C, D})
 (hdistinct : S.ncard = 4)
-(through : (ℝ × (EuclideanSpace ℝ (Fin 2))) → (EuclideanSpace ℝ (Fin 2)) → Prop := fun (r, P) => fun Q => dist P Q = r)
+(through : (ℝ × (EuclideanSpace ℝ (Fin 2))) → (EuclideanSpace ℝ (Fin 2)) → Prop)
+(through_def : through = fun (r, P) => fun Q => dist P Q = r)
 (hABCD : ∀ r s : ℝ, ∀ P Q : EuclideanSpace ℝ (Fin 2), through (r, P) A ∧ through (r, P) B ∧ through (s, Q) C ∧ through (s, Q) D →
 ∃ I : EuclideanSpace ℝ (Fin 2), through (r, P) I ∧ through (s, Q) I)
 : Collinear ℝ S ∨ ∃ r : ℝ, ∃ P : EuclideanSpace ℝ (Fin 2), ∀ Q ∈ S, through (r, P) Q :=

lean4/src/putnam_1966_a1.lean

@@ -2,6 +2,7 @@ import Mathlib
 open BigOperators
 
 theorem putnam_1966_a1
-(f : ℤ → ℤ := fun n : ℤ => ∑ m in Finset.Icc 0 n, (if Even m then m / 2 else (m - 1)/2))
+(f : ℤ → ℤ)
+(hf : f = fun n : ℤ => ∑ m in Finset.Icc 0 n, (if Even m then m / 2 else (m - 1)/2))
 : ∀ x y : ℤ, x > 0 ∧ y > 0 ∧ x > y → x * y = f (x + y) - f (x - y) :=
 sorry

lean4/src/putnam_1966_a2.lean

@@ -5,10 +5,11 @@ theorem putnam_1966_a2
 (r : ℝ)
 (A B C : EuclideanSpace ℝ (Fin 2))
 (hABC : ¬Collinear ℝ {A, B, C})
-(a : ℝ := dist B C)
-(b : ℝ := dist C A)
-(c : ℝ := dist A B)
-(p : ℝ := (dist B C + dist C A + dist A B)/2)
+(a b c p : ℝ)
+(ha : a = dist B C)
+(hb : b = dist C A)
+(hc : c = dist A B)
+(hp : p = (dist B C + dist C A + dist A B)/2)
 (hr : ∃ I : EuclideanSpace ℝ (Fin 2),
 (∃! P : EuclideanSpace ℝ (Fin 2), dist I P = r ∧ Collinear ℝ {P, B, C}) ∧
 (∃! Q : EuclideanSpace ℝ (Fin 2), dist I Q = r ∧ Collinear ℝ {Q, C, A}) ∧

lean4/src/putnam_1966_a5.lean

@@ -4,7 +4,8 @@ open BigOperators
 open Topology Filter
 
 theorem putnam_1966_a5
-(C : Set (ℝ → ℝ) := {f : ℝ → ℝ | Continuous f})
+(C : Set (ℝ → ℝ))
+(hC : C = {f : ℝ → ℝ | Continuous f})
 (T : (ℝ → ℝ) → (ℝ → ℝ))
 (imageTC : ∀ f ∈ C, T f ∈ C)
 (linearT : ∀ a b : ℝ, ∀ f ∈ C, ∀ g ∈ C, T ((fun x => a)*f + (fun x => b)*g) = (fun x => a)*(T f) + (fun x => b)*(T g))

lean4/src/putnam_1966_b1.lean

@@ -1,7 +1,7 @@
 import Mathlib
 open BigOperators
 
-open Topology Filter
+open Topology
 
 theorem putnam_1966_b1
 (n : ℕ)

lean4/src/putnam_1966_b2.lean

@@ -1,9 +1,8 @@
 import Mathlib
 open BigOperators
 
-open Topology Filter
-
 theorem putnam_1966_b2
-(S : ℤ → Set ℤ := fun n : ℤ => {n, n + 1, n + 2, n + 3, n + 4, n + 5, n + 6, n + 7, n + 8, n + 9})
+(S : ℤ → Set ℤ)
+(hS : S = fun n : ℤ => {n, n + 1, n + 2, n + 3, n + 4, n + 5, n + 6, n + 7, n + 8, n + 9})
 : ∀ n : ℤ, n > 0 → (∃ k ∈ S n, ∀ m ∈ S n, k ≠ m → IsCoprime m k) :=
 sorry

lean4/src/putnam_1967_a1.lean

@@ -6,7 +6,8 @@ open Nat Topology Filter
 theorem putnam_1967_a1
 (n : ℕ)
 (a : Set.Icc 1 n → ℝ)
-(f : ℝ → ℝ := (fun x : ℝ => ∑ i : Set.Icc 1 n, a i * Real.sin (i * x)))
+(f : ℝ → ℝ)
+(hf : f = (fun x : ℝ => ∑ i : Set.Icc 1 n, a i * Real.sin (i * x)))
 (npos : n > 0)
 (flesin : ∀ x : ℝ, abs (f x) ≤ abs (Real.sin x))
 : abs (∑ i : Set.Icc 1 n, i * a i) ≤ 1 :=

lean4/src/putnam_1967_a3.lean

@@ -6,8 +6,9 @@ open Nat Topology Filter
 abbrev putnam_1967_a3_solution : ℕ := sorry
 -- 5
 theorem putnam_1967_a3
-(pform : Polynomial ℝ → Prop := (fun p : Polynomial ℝ => p.degree = 2 ∧ ∀ i ∈ Finset.range 3, p.coeff i = round (p.coeff i)))
-(pzeros : Polynomial ℝ → Prop := (fun p : Polynomial ℝ => ∃ z1 z2 : Set.Ioo (0 : ℝ) 1, z1 ≠ z2 ∧ p.eval z1.1 = 0 ∧ p.eval z2.1 = 0))
-(pall : Polynomial ℝ → Prop := (fun p : Polynomial ℝ => pform p ∧ pzeros p ∧ p.coeff 2 > 0))
+(pform pzeros pall : Polynomial ℝ → Prop)
+(hpform : pform = (fun p : Polynomial ℝ => p.degree = 2 ∧ ∀ i ∈ Finset.range 3, p.coeff i = round (p.coeff i)))
+(hpzeros : pzeros = (fun p : Polynomial ℝ => ∃ z1 z2 : Set.Ioo (0 : ℝ) 1, z1 ≠ z2 ∧ p.eval z1.1 = 0 ∧ p.eval z2.1 = 0))
+(hpall : pall = (fun p : Polynomial ℝ => pform p ∧ pzeros p ∧ p.coeff 2 > 0))
 : (∃ p : Polynomial ℝ, pall p ∧ p.coeff 2 = putnam_1967_a3_solution) ∧ (∀ p : Polynomial ℝ, pall p → p.coeff 2 ≥ putnam_1967_a3_solution) :=
 sorry

lean4/src/putnam_1967_a6.lean

@@ -6,7 +6,8 @@ open Nat Topology Filter
 abbrev putnam_1967_a6_solution : ℕ := sorry
 -- 8
 theorem putnam_1967_a6
-(abneq0 : (Fin 4 → ℝ) → (Fin 4 → ℝ) → Prop := (fun a b : Fin 4 → ℝ => a 0 * b 1 - a 1 * b 0 ≠ 0))
+(abneq0 : (Fin 4 → ℝ) → (Fin 4 → ℝ) → Prop)
+(habneq0 : abneq0 = (fun a b : Fin 4 → ℝ => a 0 * b 1 - a 1 * b 0 ≠ 0))
 (numtuples : (Fin 4 → ℝ) → (Fin 4 → ℝ) → ℕ)
 (hnumtuples : ∀ a b : Fin 4 → ℝ, numtuples a b = {s : Fin 4 → ℝ | ∃ x : Fin 4 → ℝ, (∀ i : Fin 4, x i ≠ 0) ∧ (∑ i : Fin 4, a i * x i) = 0 ∧ (∑ i : Fin 4, b i * x i) = 0 ∧ (∀ i : Fin 4, s i = Real.sign (x i))}.encard)
 : (∃ a b : Fin 4 → ℝ, abneq0 a b ∧ numtuples a b = putnam_1967_a6_solution) ∧ (∀ a b : Fin 4 → ℝ, abneq0 a b → numtuples a b ≤ putnam_1967_a6_solution) :=

lean4/src/putnam_1967_b1.lean

@@ -6,9 +6,10 @@ open Nat Topology Filter
 theorem putnam_1967_b1
 (r : ℝ)
 (L : ZMod 6 → (EuclideanSpace ℝ (Fin 2)))
-(P : EuclideanSpace ℝ (Fin 2) := midpoint ℝ (L 1) (L 2))
-(Q : EuclideanSpace ℝ (Fin 2) := midpoint ℝ (L 3) (L 4))
-(R : EuclideanSpace ℝ (Fin 2) := midpoint ℝ (L 5) (L 0))
+(P Q R: EuclideanSpace ℝ (Fin 2))
+(hP : P = midpoint ℝ (L 1) (L 2))
+(hQ : Q = midpoint ℝ (L 3) (L 4))
+(hR : R = midpoint ℝ (L 5) (L 0))
 (hr : r > 0)
 (hcyclic : ∃ (O : EuclideanSpace ℝ (Fin 2)), ∀ i : ZMod 6, dist O (L i) = r)
 (horder : ∀ i j : ZMod 6, i + 1 = j ∨ i = j + 1 ∨ segment ℝ (L i) (L j) ∩ interior (convexHull ℝ {L k | k : ZMod 6}) ≠ ∅)

lean4/src/putnam_1968_a5.lean

@@ -6,6 +6,7 @@ open Finset Polynomial
 abbrev putnam_1968_a5_solution : ℝ := sorry
 -- 8
 theorem putnam_1968_a5
-(V : Set ℝ[X] := {P : ℝ[X] | P.degree = 2 ∧ ∀ x ∈ Set.Icc 0 1, |P.eval x| ≤ 1})
+(V : Set ℝ[X])
+(V_def : V = {P : ℝ[X] | P.degree = 2 ∧ ∀ x ∈ Set.Icc 0 1, |P.eval x| ≤ 1})
 : sSup {|(derivative P).eval 0| | P ∈ V} = putnam_1968_a5_solution :=
 sorry

lean4/src/putnam_1969_a2.lean

@@ -4,6 +4,7 @@ open BigOperators
 open Matrix Filter Topology Set Nat
 
 theorem putnam_1969_a2
-(D : (n : ℕ) → Matrix (Fin n) (Fin n) ℝ := fun n => λ i j => |i.1 - j.1| )
+(D : (n : ℕ) → Matrix (Fin n) (Fin n) ℝ)
+(hD : D = fun (n : ℕ) => λ (i : Fin n) (j : Fin n) => |(i : ℝ) - (j : ℝ)| )
 : ∀ n, n ≥ 2 → (D n).det = (-1)^((n : ℤ)-1) * ((n : ℤ)-1) * 2^((n : ℤ)-2) :=
 sorry

lean4/src/putnam_1969_b2.lean

@@ -8,6 +8,7 @@ abbrev putnam_1969_b2_solution : Prop := sorry
 theorem putnam_1969_b2
 (G : Type*)
 [Group G] [Finite G]
-(h : ℕ → Prop := fun n => ∃ H : Fin n → Subgroup G, (∀ i : Fin n, (H i) < ⊤) ∧ ((⊤ : Set G) = ⋃ i : Fin n, (H i)))
+(h : ℕ → Prop)
+(h_def : h = fun n => ∃ H : Fin n → Subgroup G, (∀ i : Fin n, (H i) < ⊤) ∧ ((⊤ : Set G) = ⋃ i : Fin n, (H i)))
 : ¬(h 2) ∧ ((¬(h 3)) ↔ putnam_1969_b2_solution) :=
 sorry