Fix uses of optParam

trishullab · Oct 21, 2024 · fe8a301 · fe8a301
1 parent 258bbe8
commit fe8a301
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 3 deletions.
diff --git a/lean4/src/putnam_1970_a1.lean b/lean4/src/putnam_1970_a1.lean
@@ -14,6 +14,7 @@ theorem putnam_1970_a1
 (f_def : f = fun x : ℝ => Real.exp (a*x) * Real.cos (b*x))
 (p : ℕ → ℝ)
 (hp : ∃ c : ℝ, c > 0 ∧ ∀ x ∈ ball 0 c, ∑' n : ℕ, (p n)*x^n = f x)
-(S : Set ℕ := {n : ℕ | p n = 0})
+(S : Set ℕ)
+(S_def : S = {n : ℕ | p n = 0})
 : S = ∅ ∨ ¬Finite S :=
 sorry
diff --git a/lean4/src/putnam_1982_a6.lean b/lean4/src/putnam_1982_a6.lean
@@ -18,7 +18,8 @@ $\lim_{n \rightarrow \infty}\sum_{k = 1}^{n} x_k = 1$.
 Prove or disprove: these conditions imply that $$\lim_{n \rightarrow \infty} \sum_{k = 1}^{n} x_{b(k)} = 1.$$
 -/
 theorem putnam_1982_a6
-(S : Set ℕ := Ici 1)
+(S : Set ℕ)
+(S_def : S = Ici 1)
 (hb : (ℕ → ℕ) → Prop)
 (hb_def : hb = fun b : ℕ → ℕ => BijOn b S S)
 (hx : (ℕ → ℝ) → Prop)

diff --git a/lean4/src/putnam_1998_a6.lean b/lean4/src/putnam_1998_a6.lean
@@ -13,6 +13,7 @@ theorem putnam_1998_a6
 (hint : ∀ i : Fin 2, ∃ a b c : ℤ, A i = a ∧ B i = b ∧ C i = c)
 (htriangle : A ≠ B ∧ A ≠ C ∧ B ≠ C)
 (harea : (dist A B + dist B C) ^ 2 < 8 * (MeasureTheory.volume (convexHull ℝ {A, B, C})).toReal + 1)
-(threesquare : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Prop := fun P Q R ↦ dist Q P = dist Q R ∧ Matrix.dotProduct (P - Q) (R - Q) = 0)
+(threesquare : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Prop)
+(threesquare_def : threesquare = fun P Q R ↦ dist Q P = dist Q R ∧ Matrix.dotProduct (P - Q) (R - Q) = 0)
 : (threesquare A B C ∨ threesquare B C A ∨ threesquare C A B) :=
 sorry