-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
hm :
  (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)) : (a : PE) → PE)
      ((f.symm : (a : PF) → PE)
          (((toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y))) :
                  PF ≃ᵢ PF) :
                (a : PF) → PF)
              ((f : (a : PE) → PF) (midpoint ℝ x y) : PF) :
            PF) :
        PE) =
    midpoint ℝ x y
rwa :
  ∀
    (hm :
      Eq.{u_2 + 1} (α := PE)
        ((f.symm : (a : PF) → PE)
            (((toIsometryEquiv (𝕜 := ℝ)
                      (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y))) :
                    PF ≃ᵢ PF) :
                  (a : PF) → PF)
                ((f : (a : PE) → PF) (midpoint ℝ x y) : PF) :
              PF) :
          PE)
        ((IsometryEquiv.symm (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y))) : (a : PE) → PE) (midpoint ℝ x y) :
          PE)),
    Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
      (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
rwa₁ :
  ∀
    (hm :
      Eq.{u_2 + 1} (α := PE)
        ((f.symm : (a : PF) → PE)
            (((toIsometryEquiv (𝕜 := ℝ)
                      (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y))) :
                    PF ≃ᵢ PF) :
                  (a : PF) → PF)
                ((f : (a : PE) → PF) (midpoint ℝ x y) : PF) :
              PF) :
          PE)
        ((toIsometryEquiv (AffineIsometryEquiv.symm (pointReflection ℝ (midpoint ℝ x y))) : (a : PE) → PE)
            (midpoint ℝ x y) :
          PE)),
    Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
      (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
⊢ Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
    (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
have rwa₂ : ∀
  (hm :
    Eq.{u_2 + 1} (α := PE)
      ((f.symm : (a : PF) → PE)
          (((toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y))) :
                  PF ≃ᵢ PF) :
                (a : PF) → PF)
              ((f : (a : PE) → PF) (midpoint ℝ x y) : PF) :
            PF) :
        PE)
      ((toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)) : (a : PE) → PE) (midpoint ℝ x y) : PE)),
  Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
    (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
Tactic: rwa [← eq_symm_apply, ← toIsometryEquiv_symm, pointReflection_symm, coe_toIsometryEquiv,
    coe_toIsometryEquiv, pointReflection_self, symm_apply_eq, @pointReflection_fixed_iff] at hm
Cleared hypotheses: hm