From f99343dc3c5b812aa5fb2d2d02c66d2b21886b05 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Mon, 28 Oct 2024 19:00:33 +0000
Subject: [PATCH 1/2] Add missing arguments to rank

---
 lean4/src/putnam_1991_a4.lean | 2 +-
 lean4/src/putnam_2006_b4.lean | 4 ++--
 lean4/src/putnam_2008_b3.lean | 2 +-
 lean4/src/putnam_2009_b4.lean | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/lean4/src/putnam_1991_a4.lean b/lean4/src/putnam_1991_a4.lean
index 5e44ac87..8a7275f8 100644
--- a/lean4/src/putnam_1991_a4.lean
+++ b/lean4/src/putnam_1991_a4.lean
@@ -17,6 +17,6 @@ theorem putnam_1991_a4 :
       (¬ ∃ p, MapClusterPt p atTop c) ∧
       (Summable <| fun i ↦ r i ^ 2) ∧
       (∀ L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)),
-        finrank L.direction = 1 → ∃ i, (↑L ∩ closedBall (c i) (r i)).Nonempty)) ↔
+        finrank ℝ L.direction = 1 → ∃ i, (↑L ∩ closedBall (c i) (r i)).Nonempty)) ↔
     putnam_1991_a4_solution :=
   sorry
diff --git a/lean4/src/putnam_2006_b4.lean b/lean4/src/putnam_2006_b4.lean
index a2c374e6..f2249b62 100644
--- a/lean4/src/putnam_2006_b4.lean
+++ b/lean4/src/putnam_2006_b4.lean
@@ -11,7 +11,7 @@ theorem putnam_2006_b4
 (hk : k ≤ n)
 (Z : Set (Fin n → ℝ))
 (hZ : Z = {P : Fin n → ℝ | ∀ j : Fin n, P j = 0 ∨ P j = 1})
-(hmaxeq : ∃ V : Subspace ℝ (Fin n → ℝ), Module.rank V = k ∧ (Z ∩ V).ncard = max)
-(hmaxub : ∀ V : Subspace ℝ (Fin n → ℝ), Module.rank V = k → (Z ∩ V).ncard ≤ max)
+(hmaxeq : ∃ V : Subspace ℝ (Fin n → ℝ), Module.rank ℝ V = k ∧ (Z ∩ V).ncard = max)
+(hmaxub : ∀ V : Subspace ℝ (Fin n → ℝ), Module.rank ℝ V = k → (Z ∩ V).ncard ≤ max)
 : (max = putnam_2006_b4_solution k) :=
 sorry
diff --git a/lean4/src/putnam_2008_b3.lean b/lean4/src/putnam_2008_b3.lean
index 902ac7f4..0aa8cbd2 100644
--- a/lean4/src/putnam_2008_b3.lean
+++ b/lean4/src/putnam_2008_b3.lean
@@ -13,7 +13,7 @@ theorem putnam_2008_b3
     (contains : ℝ → Prop)
     (contains_def : ∀ r, contains r ↔
       ∃ᵉ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 4))) (C ∈ A),
-        finrank A.direction = 2 ∧
+        finrank ℝ A.direction = 2 ∧
         sphere C r ∩ A ⊆ H) :
     IsGreatest contains putnam_2008_b3_solution :=
   sorry
diff --git a/lean4/src/putnam_2009_b4.lean b/lean4/src/putnam_2009_b4.lean
index 4cd7bea2..832a2033 100644
--- a/lean4/src/putnam_2009_b4.lean
+++ b/lean4/src/putnam_2009_b4.lean
@@ -12,5 +12,5 @@ theorem putnam_2009_b4
 (hbalanced : balanced = fun P ↦ ∀ r > 0, (∫ x in Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) r, MvPolynomial.eval x P) / (2 * Real.pi * r) = 0)
 (V : Set (MvPolynomial (Fin 2) ℝ)) [AddCommGroup V] [Module ℝ V]
 (hV : ∀ P : MvPolynomial (Fin 2) ℝ, P ∈ V ↔ balanced P ∧ P.totalDegree ≤ 2009)
-: (Module.rank V = putnam_2009_b4_solution) :=
+: (Module.rank ℝ V = putnam_2009_b4_solution) :=
 sorry

From 053106232b81a6886ee06465722b2cb7bedd0e05 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Tue, 29 Oct 2024 16:44:15 +0000
Subject: [PATCH 2/2] Add back trailing newline

---
 lean4/src/putnam_2009_b4.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean4/src/putnam_2009_b4.lean b/lean4/src/putnam_2009_b4.lean
index 298c1260..6e4c16cf 100644
--- a/lean4/src/putnam_2009_b4.lean
+++ b/lean4/src/putnam_2009_b4.lean
@@ -14,4 +14,4 @@ theorem putnam_2009_b4
     (V : Submodule ℝ (MvPolynomial (Fin 2) ℝ))
     (V_def : ∀ P, P ∈ V ↔ IsBalanced P ∧ P.totalDegree ≤ 2009) :
     Module.rank ℝ V = putnam_2009_b4_solution :=
-  sorry
\ No newline at end of file
+  sorry