refactor(LinearAlgebra/Orientation,LinearAlgebra/AffineSpace/FiniteDimensional): instances for arbitrary orientations

Archive/Imo/Imo2019Q2.lean

@@ -93,11 +93,6 @@ structure Imo2019q2Cfg where
   -- A hypothesis implicit in the first named angle.
   C_ne_Q₁ : C ≠ Q₁
 
-/-- A default choice of orientation, for lemmas that need to pick one. -/
-@[instance_reducible]
-def someOrientation [hd2 : Fact (finrank ℝ V = 2)] : Module.Oriented ℝ V (Fin 2) :=
-  ⟨Basis.orientation (finBasisOfFinrankEq _ _ hd2.out)⟩
-
 variable {V Pt}
 
 namespace Imo2019q2Cfg
@@ -263,6 +258,8 @@ end Oriented
 
 /-! ### More obvious configuration properties -/
 
+open scoped Module.Oriented.Arbitrary
+
 section
 
 variable [hd2 : Fact (finrank ℝ V = 2)]
@@ -275,7 +272,6 @@ theorem A₁_ne_B : cfg.A₁ ≠ cfg.B := by
     rw [AffineSubspace.eq_iff_direction_eq_of_mem (left_mem_affineSpan_pair _ _ _)
       hwbtw.mem_affineSpan]
     exact cfg.PQ_parallel_AB.direction_eq
-  haveI := someOrientation V
   have haQ : (2 : ℤ) • ∡ cfg.C cfg.B cfg.Q = (2 : ℤ) • ∡ cfg.C cfg.B cfg.A := by
     rw [Collinear.two_zsmul_oangle_eq_right _ cfg.A_ne_B cfg.Q_ne_B]
     rw [Set.pair_comm, Set.insert_comm]
@@ -389,7 +385,6 @@ end Oriented
 
 
 theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.Q, cfg.P, cfg.A₂} : Set Pt) := by
-  haveI := someOrientation V
   rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂, ←
     affineIndependent_iff_not_collinear_set]
   have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by
@@ -464,7 +459,6 @@ end Oriented
 
 
 theorem cospherical_QPB₂A₂ : Cospherical ({cfg.Q, cfg.P, cfg.B₂, cfg.A₂} : Set Pt) :=
-  haveI := someOrientation V
   cospherical_of_two_zsmul_oangle_eq_of_not_collinear
     cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂A₂ cfg.not_collinear_QPA₂
 
@@ -515,13 +509,11 @@ end Oriented
 
 
 theorem not_collinear_CA₂A₁ : ¬Collinear ℝ ({cfg.C, cfg.A₂, cfg.A₁} : Set Pt) := by
-  haveI := someOrientation V
   rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA,
     Set.pair_comm, Set.insert_comm, Set.pair_comm]
   exact cfg.not_collinear_ABC
 
 theorem cospherical_A₁Q₁CA₂ : Cospherical ({cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂} : Set Pt) := by
-  haveI := someOrientation V
   rw [Set.insert_comm cfg.Q₁, Set.insert_comm cfg.A₁, Set.pair_comm, Set.insert_comm cfg.A₁,
     Set.pair_comm]
   exact cospherical_of_two_zsmul_oangle_eq_of_not_collinear
@@ -555,7 +547,6 @@ end Oriented
 
 
 theorem Q₁_mem_ω : cfg.Q₁ ∈ cfg.ω :=
-  haveI := someOrientation V
   Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq (by decide : (0 : Fin 3) ≠ 1)
     (by decide : (0 : Fin 3) ≠ 2) (by decide) cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂
 

Mathlib/Geometry/Euclidean/Angle/Sphere.lean

@@ -425,19 +425,15 @@ theorem mem_circumsphere_of_two_zsmul_oangle_eq {t : Triangle ℝ P} {p : P} {i
 
 end Oriented
 
+open scoped Affine.Simplex Module.Oriented.Arbitrary in
 /-- The circumradius of a triangle may be expressed explicitly as half the length of a side
 divided by the sine of the angle at the third point (a version of the law of sines or sine rule). -/
 theorem dist_div_sin_angle_div_two_eq_circumradius (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3}
     (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
     dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2 =
       t.circumradius := by
-  set S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points) with hS
+  let S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
   let t' : Triangle ℝ S := t.restrict S le_rfl
-  have hf2 : Fact (finrank ℝ S.direction = 2) := ⟨by
-    rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan]
-    simp⟩
-  have : Module.Oriented ℝ S.direction (Fin 2) :=
-    ⟨Basis.orientation (finBasisOfFinrankEq _ _ hf2.out)⟩
   convert! t'.dist_div_sin_oangle_div_two_eq_circumradius h₁₂ h₁₃ h₂₃ using 3
   · rw [← Real.Angle.sin_toReal,
       Real.abs_sin_eq_sin_abs_of_abs_le_pi (Real.Angle.abs_toReal_le_pi _),

Mathlib/Geometry/Euclidean/Sphere/Power.lean

@@ -160,6 +160,7 @@ private lemma cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi_aux
   apply similar_of_side_angle_side h_notcol_p₁pp₄ h_notcol_p₃pp₂ h_angle_eq ?_
   grind [dist_comm]
 
+open scoped Affine.Simplex Module.Oriented.Arbitrary in
 /-- If `p` lies strictly between `p₁` and `p₂` on one line and strictly between `p₃` and `p₄`
 on another line, and if `dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p`,
 then the points `p₁`, `p₂`, `p₃`, and `p₄` are cospherical. -/
@@ -171,7 +172,7 @@ theorem cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi {p₁ p₂ p₃ p₄
   have hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄ := angle_eq_pi_iff_sbtw.mp hp₃p₄
   have hindep : AffineIndependent ℝ ![p₁, p, p₃] := affineIndependent_iff_not_collinear_set.mpr hn
   set t : Affine.Triangle ℝ P := ⟨_, hindep⟩ with ht
-  set S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points) with hS
+  let S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
   have hp₂ : p₂ ∈ S := by
     suffices hmem : p₂ ∈ affineSpan ℝ {p₁, p} by exact affineSpan_mono ℝ (by simp [ht]; grind) hmem
     simp [hp₁p₂_sbtw.wbtw.collinear.mem_affineSpan_of_mem_of_ne _ _ _ hp₁p₂_sbtw.left_ne]
@@ -195,16 +196,12 @@ theorem cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi {p₁ p₂ p₃ p₄
     canonicalizer; a minimization would help. The original proof was:
     `grind [Set.image_insert_eq, Set.image_singleton]` -/
     simpa [Set.image_insert_eq, Set.image_singleton] using Cospherical.subtype_val h_cospherical'
-  have hf2 : Fact (finrank ℝ S.direction = 2) := ⟨by
-    rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan]
-    simp⟩
-  let : Module.Oriented ℝ S.direction (Fin 2) :=
-    ⟨Basis.orientation (finBasisOfFinrankEq _ _ hf2.out)⟩
   have hncol : ¬ Collinear ℝ {p₁', p', p₃'} := by
     rw [← affineIndependent_iff_not_collinear_set,
       ← s_isom.toAffineMap.affineIndependent_iff s_isom.injective]
     convert! hindep
     ext i; fin_cases i <;> rfl
+  have : Fact (finrank ℝ S.direction = 2) := Affine.Simplex.fact_finrank_direction_affineSpan_eq
   exact cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi_aux h_dist' hp₁'p₂' hp₃'p₄' hncol
 
 /-- **Intersecting Secants Theorem**. -/

Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

@@ -168,6 +168,16 @@ theorem AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one [FiniteDi
     vectorSpan k (Set.range p) = ⊤ :=
   Submodule.eq_top_of_finrank_eq <| hi.finrank_vectorSpan hc
 
+namespace Affine.Simplex
+
+/-- A convenience instance for use when restricting to the affine subspace spanned by the vertices
+of a simplex. -/
+scoped instance fact_finrank_direction_affineSpan_eq {n : ℕ} {s : Simplex k P n} :
+    Fact (finrank k (affineSpan k (Set.range s.points)).direction = n) :=
+  ⟨by rw [direction_affineSpan]; exact s.independent.finrank_vectorSpan (Fintype.card_fin _)⟩
+
+end Affine.Simplex
+
 variable (k)
 
 /-- The `vectorSpan` of `n + 1` points in an indexed family has

Mathlib/LinearAlgebra/Orientation.lean

@@ -191,6 +191,15 @@ theorem orientation_isEmpty [IsEmpty ι] (b : Basis ι R M) :
 
 end Module.Basis
 
+namespace Module.Oriented.Arbitrary
+
+/-- An arbitrary choice of orientation. -/
+scoped instance (priority := 100) {n : ℕ} [Module.Finite R M] [Module.Free R M]
+    [Fact (finrank R M = n)] : Module.Oriented R M (Fin n) :=
+  ⟨Basis.orientation (finBasisOfFinrankEq _ _ Fact.out)⟩
+
+end Module.Oriented.Arbitrary
+
 end OrderedCommRing
 
 section LinearOrderedCommRing