diff --git a/lean4/src/putnam_1991_a4.lean b/lean4/src/putnam_1991_a4.lean
index 5e44ac8..8a7275f 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 a2c374e..f2249b6 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 902ac7f..0aa8cbd 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 4cd7bea..832a203 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