Fix a few minor Lean misformalisations

lean4/src/putnam_1962_a2.lean

@@ -1,16 +1,15 @@
 import Mathlib
 open BigOperators
 
-open MeasureTheory
+open MeasureTheory Set
 
 abbrev putnam_1962_a2_solution : Set (ℝ → ℝ) := sorry
--- {f : ℝ → ℝ | ∃ a c : ℝ, a > 0 ∧ f = fun x => a / (1 - c * x)^2}
+-- {f : ℝ → ℝ | ∃ a c : ℝ, a ≥ 0 ∧ f = fun x ↦ a / (1 - c * x) ^ 2}
 theorem putnam_1962_a2
-(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) :=
-sorry
+    (P : Set ℝ → (ℝ → ℝ) → Prop)
+    (P_def : ∀ s f, P s f ↔ ∀ x ∈ s, ⨍ t in Ico 0 x, f t = √(f 0 * f x)) :
+    (∀ f,
+      (P (Ioi 0) f → ∃ g ∈ putnam_1962_a2_solution, EqOn f g (Ici 0)) ∧
+      (∀ e > 0, P (Ioo 0 e) f → ∃ g ∈ putnam_1962_a2_solution, EqOn f g (Ico 0 e))) ∧
+    ∀ f ∈ putnam_1962_a2_solution, P (Ioi 0) f ∨ (∃ e > 0, P (Ioo 0 e) f) :=
+  sorry

lean4/src/putnam_1963_a4.lean

@@ -1,12 +1,12 @@
 import Mathlib
 open BigOperators
 
-open Topology Filter
+open Filter Set
 
 theorem putnam_1963_a4
-(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
+    (T : (ℕ → ℝ) → (ℕ → ℝ))
+    (T_def : ∀ a n, T a n = n * ((1 + a (n + 1)) / a n - 1))
+    (P : (ℕ → ℝ) → ℝ → Prop)
+    (P_def : ∀ a C, P a C ↔ C ≤ limsup (T a) atTop ∨ ¬ BddAbove (range (T a))) :
+    (∀ a, (∀ n, 0 < a n) → P a 1) ∧ (∀ C > 1, ∃ a, (∀ n, 0 < a n) ∧ ¬ P a C) := by
+  sorry

lean4/src/putnam_1964_b1.lean

@@ -4,10 +4,9 @@ open BigOperators
 open Set Function Filter Topology
 
 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)
-(hb : b = fun (n : ℕ) ↦ ({k : ℕ | a k ≤ n}.encard : ENNReal))
-: (Tendsto (fun n : ℕ ↦ b n / n) atTop (𝓝 0)) :=
-sorry
+    (a b : ℕ → ℕ)
+    (h₁ : ∀ n, 0 < a n)
+    (h₂ : Summable fun n ↦ (1 : ℝ) / a n)
+    (h₃ : ∀ n, b n = {k | a k ≤ n}.ncard) :
+    Tendsto (fun n ↦ (b n : ℝ) / n) atTop (𝓝 0) :=
+  sorry

lean4/src/putnam_1965_a6.lean

@@ -4,10 +4,14 @@ open BigOperators
 open EuclideanGeometry Topology Filter Complex
 
 theorem putnam_1965_a6
-(u v m : ℝ)
-(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) :=
-sorry
+    (u v m : ℝ)
+    (hu : 0 < u)
+    (hv : 0 < v)
+    (hm : 1 < m) :
+    (∃ᵉ (x > 0) (y > 0),
+      u * x + v * y = 1 ∧
+      x ^ m + y ^ m = 1 ∧
+      u = x ^ (m - 1) ∧
+      v = y ^ (m - 1)) ↔
+    ∃ n, u ^ n + v ^ n = 1 ∧ m⁻¹ + n⁻¹ = 1 :=
+  sorry

lean4/src/putnam_1968_a3.lean

@@ -1,12 +1,12 @@
 import Mathlib
 open BigOperators
 
-open Finset
+open Finset symmDiff
 
 theorem putnam_1968_a3
-{a : Type}
-(S : Finset a)
-(ha : SDiff (Finset a))
-: ∃ l : List (Finset a), (∀ i : Fin l.length, l[i] ⊆ S) ∧ l[0]! = ∅ ∧ (∀ s ⊆ S, ∃! i : Fin l.length, l[i] = s) ∧
-∀ i ∈ Finset.range (l.length - 1), (l[i]! ⊆ l[i+1]! ∧ (l[i+1]! \ l[i]!).card = 1) ∨ (l[i+1]! ⊆ l[i]! ∧ (l[i]! \ l[i+1]!).card = 1) :=
-sorry
+    (α : Type*) [Finite α] :
+    ∃ (n : ℕ) (s : Fin (2 ^ n) → Set α),
+      s 0 = ∅ ∧
+      (∀ t, ∃! i, s i = t) ∧
+      (∀ i, i + 1 < 2 ^ n → (s i ∆ s (i + 1)).ncard = 1) := by
+  sorry

lean4/src/putnam_1969_a5.lean

@@ -4,7 +4,16 @@ open BigOperators
 open Matrix Filter Topology Set Nat
 
 theorem putnam_1969_a5
-: ∀ x y : ℝ → ℝ, (Differentiable ℝ x ∧ Differentiable ℝ y) → ∀ t > 0,
-(x 0 = y 0 ↔ ∃ u : ℝ → ℝ, Continuous u ∧ x t = 0 ∧ y t = 0 ∧
-deriv x = (fun _ : ℝ ↦ -2) * y + u ∧ deriv y = (fun _ : ℝ ↦ -2) * x + u) :=
-sorry
+    (x0 y0 t : ℝ)
+    (ht : 0 < t) :
+    x0 = y0 ↔ ∃ x y u : ℝ → ℝ,
+      Differentiable ℝ x ∧
+      Differentiable ℝ y ∧
+      Continuous u ∧
+      deriv x = - 2 • y + u ∧
+      deriv y = - 2 • x + u ∧
+      x 0 = x0 ∧
+      y 0 = y0 ∧
+      x t = 0 ∧
+      y t = 0 := by
+  sorry

lean4/src/putnam_1969_b2.lean

@@ -6,9 +6,8 @@ open Matrix Filter Topology Set Nat
 abbrev putnam_1969_b2_solution : Prop := sorry
 -- False
 theorem putnam_1969_b2
-(G : Type*)
-[Group G] [Finite G]
-(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
+    (P : ℕ → Prop)
+    (P_def : ∀ n, P n ↔ ∀ (G : Type) [Group G] [Finite G],
+      ∀ H : Fin n → Subgroup G, (∀ i, H i < ⊤) → ⋃ i, (H i : Set G) < ⊤) :
+    P 2 ∧ (P 3 ↔ putnam_1969_b2_solution) :=
+  sorry

lean4/src/putnam_2018_b5.lean

@@ -6,8 +6,8 @@ open Function
 theorem putnam_2018_b5
     (f : (Fin 2 → ℝ) → (Fin 2 → ℝ))
     (h₁ : ContDiff ℝ 1 f)
-    (h₂ : ∀ x i j, 0 < fderiv ℝ f x i j)
-    (h₃ : ∀ x, 0 < fderiv ℝ f x 0 0 * fderiv ℝ f x 1 1 -
-      (1 / 4) * (fderiv ℝ f x 0 1 + fderiv ℝ f x 1 0) ^ 2) :
+    (h₂ : ∀ x i j, 0 < fderiv ℝ f x (Pi.single i 1) j)
+    (h₃ : ∀ x, 0 < fderiv ℝ f x ![1, 0] 0 * fderiv ℝ f x ![0, 1] 1 -
+      (1 / 4) * (fderiv ℝ f x ![1, 0] 1 + fderiv ℝ f x ![0, 1] 0) ^ 2) :
     Injective f :=
   sorry