-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hc :
  (Finset.affineCombination ℝ Finset.univ (s.map f.toAffineMap ⋯).points : (a : Fin (n + 1) → ℝ) → P₂)
      ((s.map f.toAffineMap ⋯).touchpointWeights signs i) =
    (s.map f.toAffineMap ⋯).touchpoint signs i
h₁ :
  ∀
    (hc :
      Eq.{u_4 + 1} (α := P₂)
        ((Finset.affineCombination ℝ Finset.univ (s.map f.toAffineMap ⋯).points : (a : Fin (n + 1) → ℝ) → P₂)
            ((s.map f.toAffineMap ⋯).touchpointWeights signs i) :
          P₂)
        ((f : (a : P) → P₂) (s.touchpoint signs i) : P₂)),
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        ((s.map f.toAffineMap ⋯).touchpointWeights signs i) =
      s.touchpoint signs i
h₂ :
  ∀
    (hc :
      Eq.{u_4 + 1} (α := P₂)
        ((Finset.affineCombination ℝ Finset.univ ((⇑f.toAffineMap : (a : P) → P₂) ∘ s.points) :
              (a : Fin (n + 1) → ℝ) → P₂)
            ((s.map f.toAffineMap ⋯).touchpointWeights signs i) :
          P₂)
        ((f : (a : P) → P₂) (s.touchpoint signs i) : P₂)),
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        ((s.map f.toAffineMap ⋯).touchpointWeights signs i) =
      s.touchpoint signs i
h₃ :
  ∀
    (hc :
      Eq.{u_4 + 1} (α := P₂)
        ((f.toAffineMap : (a : P) → P₂)
            ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) fun (j : Fin (n + 1)) ↦
                (s.map f.toAffineMap ⋯).touchpointWeights signs i j :
              P) :
          P₂)
        ((f : (a : P) → P₂) (s.touchpoint signs i) : P₂)),
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        ((s.map f.toAffineMap ⋯).touchpointWeights signs i) =
      s.touchpoint signs i
h₄ :
  ∀
    (hc :
      Eq.{u_4 + 1} (α := P₂)
        ((f : (a : P) → P₂)
            ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) fun (j : Fin (n + 1)) ↦
                (s.map f.toAffineMap ⋯).touchpointWeights signs i j :
              P) :
          P₂)
        ((f : (a : P) → P₂) (s.touchpoint signs i) : P₂)),
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        ((s.map f.toAffineMap ⋯).touchpointWeights signs i) =
      s.touchpoint signs i
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
      ((s.map f.toAffineMap ⋯).touchpointWeights signs i) =
    s.touchpoint signs i
have h₅ : ∀
  (hc :
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) fun (j : Fin (n + 1)) ↦
        (s.map f.toAffineMap sorry).touchpointWeights signs i j) =
      s.touchpoint signs i),
  (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
      ((s.map f.toAffineMap sorry).touchpointWeights signs i) =
    s.touchpoint signs i
Tactic: rwa [h.touchpoint_map, map_points, ← Finset.univ.map_affineCombination _ _
    ((s.map f.toAffineMap f.injective).sum_touchpointWeights _ _), AffineIsometry.coe_toAffineMap,
    AffineIsometry.map_eq_iff] at hc
Cleared hypotheses: hc