chore(Geometry/Convex): uninstantiate AddTorsor.toConvexSpace (#39461)

This instance is defined through choice and is therefore very diamond-prone.

Author: YaelDillies

Mathlib/Analysis/Convex/MetricSpace.lean

@@ -40,6 +40,8 @@ public section
 
 namespace Convexity
 
+attribute [local instance] AddTorsor.toConvexSpace
+
 open ConvexSpace
 
 variable {I X : Type*} [ConvexSpace ℝ X] [MetricSpace X]

Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean

@@ -98,11 +98,18 @@ theorem convexCombination_assoc (f : StdSimplex R (StdSimplex R P)) :
       simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, hp', mul_zero,
         not_true_eq_false] at hp
 
-instance instConvexSpace : ConvexSpace R P where
+/-- Any affine space is a convex space.
+
+This is not an instance because its convex combination operation is defined through the choice of an
+arbitrary basepoint, which makes it very diamond-prone. -/
+@[implicit_reducible]
+def toConvexSpace : ConvexSpace R P where
   sConvexComb := convexCombination
   sConvexComb_single := convexCombination_single
   assoc := convexCombination_assoc
 
+attribute [local instance] toConvexSpace
+
 /-- `ConvexSpace.sConvexComb` in an affine space is the affine combination. -/
 theorem sConvexComb_eq_affineCombination (s : StdSimplex R P) :
     s.sConvexComb = s.weights.support.affineCombination R id s.weights := by
@@ -156,6 +163,8 @@ open Finsupp
 
 namespace Convexity
 
+attribute [local instance] AddTorsor.toConvexSpace
+
 theorem sConvexComb_eq_sum (f : StdSimplex R V) :
     f.sConvexComb = f.weights.sum fun i r ↦ r • i := by
   simp [AddTorsor.sConvexComb_eq_affineCombination,