chore: make AffineSubspace.toAddTorsor and AffineSubspace.nonempty_map instances (#28467)

The loops with the `Nonempty` instances are no longer an issue in Lean 4.

Author: gasparattila

Mathlib/Analysis/Convex/Intrinsic.lean

@@ -215,8 +215,6 @@ variable [NormedField 𝕜] [SeminormedAddCommGroup V] [SeminormedAddCommGroup W
   [NormedSpace 𝕜 W] [MetricSpace P] [PseudoMetricSpace Q] [NormedAddTorsor V P]
   [NormedAddTorsor W Q]
 
-attribute [local instance] AffineSubspace.toNormedAddTorsor AffineSubspace.nonempty_map
-
 @[simp]
 theorem image_intrinsicInterior (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) :
     intrinsicInterior 𝕜 (φ '' s) = φ '' intrinsicInterior 𝕜 s := by

Mathlib/Analysis/Normed/Affine/Isometry.lean

@@ -767,8 +767,6 @@ theorem AffineMap.isOpenMap_linear_iff {f : P →ᵃ[𝕜] P₂} : IsOpenMap f.l
   rw [this]
   simp only [Homeomorph.comp_isOpenMap_iff, Homeomorph.comp_isOpenMap_iff']
 
-attribute [local instance] AffineSubspace.nonempty_map
-
 namespace AffineSubspace
 
 /-- An affine subspace is isomorphic to its image under an injective affine map.

Mathlib/Geometry/Euclidean/Circumcenter.lean

@@ -335,8 +335,6 @@ theorem circumcenter_reindex {m n : ℕ} (s : Simplex ℝ P m) (e : Fin (m + 1)
 theorem circumradius_reindex {m n : ℕ} (s : Simplex ℝ P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :
     (s.reindex e).circumradius = s.circumradius := by simp_rw [circumradius, circumsphere_reindex]
 
-attribute [local instance] AffineSubspace.toAddTorsor
-
 theorem dist_circumcenter_sq_eq_sq_sub_circumradius {n : ℕ} {r : ℝ} (s : Simplex ℝ P n) {p₁ : P}
     (h₁ : ∀ i : Fin (n + 1), dist (s.points i) p₁ = r)
     (h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter)

Mathlib/Geometry/Euclidean/Projection.lean

@@ -92,8 +92,6 @@ theorem orthogonalProjectionFn_vsub_mem_direction_orthogonal {s : AffineSubspace
   direction_mk' p s.directionᗮ ▸
     vsub_mem_direction (orthogonalProjectionFn_mem_orthogonal p) (self_mem_mk' _ _)
 
-attribute [local instance] AffineSubspace.toAddTorsor
-
 /-- Auxiliary definition for setting up the orthogonal projection. This one is a bundled affine
 map; the final `orthogonalProjection` is a continuous affine map. -/
 nonrec def orthogonalProjectionAux (s : AffineSubspace ℝ P) [Nonempty s]

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

@@ -59,9 +59,7 @@ theorem vsub_left_mem_direction_iff_mem {s : AffineSubspace k P} {p : P} (hp : p
   rw [mem_direction_iff_eq_vsub_left hp]
   simp
 
--- See note [reducible non instances]
-/-- This is not an instance because it loops with `AddTorsor.nonempty`. -/
-abbrev toAddTorsor (s : AffineSubspace k P) [Nonempty s] : AddTorsor s.direction s where
+instance toAddTorsor (s : AffineSubspace k P) [Nonempty s] : AddTorsor s.direction s where
   vadd a b := ⟨(a : V) +ᵥ (b : P), vadd_mem_of_mem_direction a.2 b.2⟩
   zero_vadd := fun a => by
     ext
@@ -77,8 +75,6 @@ abbrev toAddTorsor (s : AffineSubspace k P) [Nonempty s] : AddTorsor s.direction
     ext
     apply AddTorsor.vadd_vsub'
 
-attribute [local instance] toAddTorsor
-
 @[simp, norm_cast]
 theorem coe_vsub (s : AffineSubspace k P) [Nonempty s] (a b : s) : ↑(a -ᵥ b) = (a : P) -ᵥ (b : P) :=
   rfl
@@ -151,8 +147,6 @@ theorem preimage_coe_affineSpan_singleton (x : P) :
 
 variable (P)
 
-attribute [local instance] toAddTorsor
-
 /-- The top affine subspace is linearly equivalent to the affine space.
 This is the affine version of `Submodule.topEquiv`. -/
 @[simps! linear apply symm_apply_coe]
@@ -312,10 +306,6 @@ theorem vectorSpan_range_eq_span_range_vsub_right_ne (p : ι → P) (i₀ : ι)
 
 variable {k}
 
-section WithLocalInstance
-
-attribute [local instance] AffineSubspace.toAddTorsor
-
 /-- A set, considered as a subset of its spanned affine subspace, spans the whole subspace. -/
 @[simp]
 theorem affineSpan_coe_preimage_eq_top (A : Set P) [Nonempty A] :
@@ -326,8 +316,6 @@ theorem affineSpan_coe_preimage_eq_top (A : Set P) [Nonempty A] :
   · exact subset_affineSpan _ _ hy
   · exact AffineSubspace.smul_vsub_vadd_mem _ _
 
-end WithLocalInstance
-
 /-- Suppose a set of vectors spans `V`.  Then a point `p`, together with those vectors added to `p`,
 spans `P`. -/
 theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top {s : Set V} (p : P)
@@ -575,8 +563,6 @@ theorem map_mono {s₁ s₂ : AffineSubspace k P₁} (h : s₁ ≤ s₂) : s₁.
 section inclusion
 variable {S₁ S₂ : AffineSubspace k P₁} [Nonempty S₁]
 
-attribute [local instance] AffineSubspace.toAddTorsor
-
 /-- Affine map from a smaller to a larger subspace of the same space.
 
 This is the affine version of `Submodule.inclusion`. -/
@@ -618,8 +604,6 @@ namespace AffineEquiv
 section ofEq
 variable (S₁ S₂ : AffineSubspace k P₁) [Nonempty S₁] [Nonempty S₂]
 
-attribute [local instance] AffineSubspace.toAddTorsor
-
 /-- Affine equivalence between two equal affine subspace.
 
 This is the affine version of `LinearEquiv.ofEq`. -/

Mathlib/LinearAlgebra/AffineSpace/Restrict.lean

@@ -27,14 +27,11 @@ This file defines restrictions of affine maps.
 variable {k V₁ P₁ V₂ P₂ : Type*} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁]
   [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂]
 
--- not an instance because it loops with `Nonempty`
-theorem AffineSubspace.nonempty_map {E : AffineSubspace k P₁} [Ene : Nonempty E] {φ : P₁ →ᵃ[k] P₂} :
-    Nonempty (E.map φ) := by
+instance AffineSubspace.nonempty_map {E : AffineSubspace k P₁} [Ene : Nonempty E]
+    {φ : P₁ →ᵃ[k] P₂} : Nonempty (E.map φ) := by
   obtain ⟨x, hx⟩ := id Ene
   exact ⟨⟨φ x, AffineSubspace.mem_map.mpr ⟨x, hx, rfl⟩⟩⟩
 
-attribute [local instance] AffineSubspace.nonempty_map AffineSubspace.toAddTorsor
-
 /-- Restrict domain and codomain of an affine map to the given subspaces. -/
 def AffineMap.restrict (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁} {F : AffineSubspace k P₂}
     [Nonempty E] [Nonempty F] (hEF : E.map φ ≤ F) : E →ᵃ[k] F := by

Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean

@@ -235,7 +235,6 @@ theorem reindex_map {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n
   rfl
 
 section restrict
-attribute [local instance] AffineSubspace.toAddTorsor
 
 /-- Restrict an affine simplex to an affine subspace that contains it. -/
 @[simps]
@@ -271,7 +270,6 @@ theorem restrict_map_restrict
     (S₁ : AffineSubspace k P) (S₂ : AffineSubspace k P₂)
     (hS₁ : affineSpan k (Set.range s.points) ≤ S₁) (hfS : AffineSubspace.map f S₁ ≤ S₂) :
     letI := Nonempty.map (AffineSubspace.inclusion hS₁) inferInstance
-    letI : Nonempty (S₁.map f) := AffineSubspace.nonempty_map
     letI := Nonempty.map (AffineSubspace.inclusion hfS) inferInstance
     (s.restrict S₁ hS₁).map (f.restrict hfS) (AffineMap.restrict.injective hf _) =
       (s.map f hf).restrict S₂ (

Mathlib/Topology/Algebra/AffineSubspace.lean

@@ -24,8 +24,6 @@ namespace AffineSubspace
 variable {R V P : Type*} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P]
   [AddTorsor V P]
 
-attribute [local instance] toAddTorsor
-
 /-- Embedding of an affine subspace to the ambient space, as a continuous affine map. -/
 def subtypeA (s : AffineSubspace R P) [Nonempty s] : s →ᴬ[R] P where
   toAffineMap := s.subtype