Merge branch 'incenter_map' into angle_incenter_unoriented

Author: jsm28

Mathlib/Geometry/Euclidean/Incenter.lean

@@ -386,8 +386,8 @@ variable {s} in
     haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
     (s.restrict S hS).excenter signs = s.excenter signs := by
   rw [← s.excenterExists_restrict S hS] at h
-  rw [eq_comm]
-  convert h.excenter_map S.subtypeₐᵢ
+  haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
+  exact (h.excenter_map S.subtypeₐᵢ).symm
 
 /-- The incenter of a simplex. -/
 def incenter : P :=
@@ -796,8 +796,8 @@ variable {s} in
     haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
     (s.restrict S hS).touchpoint signs i = s.touchpoint signs i := by
   rw [← s.excenterExists_restrict S hS] at h
-  rw [eq_comm]
-  convert h.touchpoint_map S.subtypeₐᵢ i
+  haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
+  exact (h.touchpoint_map S.subtypeₐᵢ i).symm
 
 lemma touchpoint_mem_affineSpan (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) :
     s.touchpoint signs i ∈ affineSpan ℝ (Set.range (s.faceOpposite i).points) :=
@@ -1144,8 +1144,8 @@ variable {s} in
     haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
     (s.restrict S hS).touchpointWeights signs = s.touchpointWeights signs := by
   rw [← s.excenterExists_restrict S hS] at h
-  rw [eq_comm]
-  convert h.touchpointWeights_map S.subtypeₐᵢ
+  haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
+  exact (h.touchpointWeights_map S.subtypeₐᵢ).symm
 
 variable {s} in
 lemma ExcenterExists.sign_touchpointWeights {signs : Finset (Fin (n + 1))}