From 27491bccc7f74bf3039a6612a916041fc8fec595 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Mon, 21 Oct 2024 11:19:38 +0000
Subject: [PATCH] =?UTF-8?q?Use=20`=E2=9F=AAx,=20y=E2=9F=AB=5F=E2=84=9D`=20?=
 =?UTF-8?q?instead=20of=20`Matrix.dotProduct`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lean4/src/putnam_1998_a6.lean | 3 ++-
 lean4/src/putnam_2002_a2.lean | 7 ++++---
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/lean4/src/putnam_1998_a6.lean b/lean4/src/putnam_1998_a6.lean
index 1f1d90d9..b9479aaa 100644
--- a/lean4/src/putnam_1998_a6.lean
+++ b/lean4/src/putnam_1998_a6.lean
@@ -2,6 +2,7 @@ import Mathlib
 open BigOperators
 
 open Set Function Metric
+open scoped InnerProductSpace
 
 /--
 Let $A, B, C$ denote distinct points with integer coordinates in $\mathbb R^2$. Prove that if
@@ -13,6 +14,6 @@ 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 := fun P Q R ↦ dist Q P = dist Q R ∧ ⟪P - Q, R - Q⟫_ℝ = 0)
 : (threesquare A B C ∨ threesquare B C A ∨ threesquare C A B) :=
 sorry
diff --git a/lean4/src/putnam_2002_a2.lean b/lean4/src/putnam_2002_a2.lean
index 8a0a317a..441af7f7 100644
--- a/lean4/src/putnam_2002_a2.lean
+++ b/lean4/src/putnam_2002_a2.lean
@@ -2,6 +2,7 @@ import Mathlib
 open BigOperators
 
 open Nat Metric
+open scoped InnerProductSpace
 
 /--
 Given any five points on a sphere, show that some four of them must lie on a closed hemisphere.
@@ -9,7 +10,7 @@ Given any five points on a sphere, show that some four of them must lie on a clo
 theorem putnam_2002_a2
 (unit_sphere : Set (EuclideanSpace ℝ (Fin 3)))
 (hsphere : unit_sphere = sphere 0 1)
-(hemi : (EuclideanSpace ℝ (Fin 3)) → Set (EuclideanSpace ℝ (Fin 3)))
-(hhemi : hemi = fun V ↦ {P : EuclideanSpace ℝ (Fin 3) | Matrix.dotProduct P V ≥ 0})
-: (∀ (S : Set (EuclideanSpace ℝ (Fin 3))), S ⊆ unit_sphere ∧ S.encard = 5 → ∃ V : (EuclideanSpace ℝ (Fin 3)), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) :=
+(hemi : EuclideanSpace ℝ (Fin 3) → Set (EuclideanSpace ℝ (Fin 3)))
+(hhemi : hemi = fun V ↦ {P : EuclideanSpace ℝ (Fin 3) | ⟪P, V⟫_ℝ ≥ 0})
+: (∀ (S : Set (EuclideanSpace ℝ (Fin 3))), S ⊆ unit_sphere ∧ S.encard = 5 → ∃ V : EuclideanSpace ℝ (Fin 3), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) :=
 sorry