-- Module: Mathlib.Analysis.Normed.Affine.MazurUlam
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)
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)
rwa₃ :
  ∀
    (hm :
      Eq.{u_2 + 1} (α := PE)
        ((f.symm : (a : PF) → PE)
            (((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)
rwa₄ :
  ∀
    (hm :
      Eq.{u_2 + 1} (α := PE)
        ((f.symm : (a : PF) → PE)
            (((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)
        ((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 :
      (f.symm : (a : PF) → PE)
          (((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) =
        midpoint ℝ x y),
    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_4 + 1} (α := PF)
        (((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)
        ((f : (a : PE) → PF) (midpoint ℝ x 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)
rwa₇ rwa₈ rwa₉ rwa₁₀ :
  ∀
    (hm :
      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)
⊢ 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

Premises used: AffineIsometryEquiv.pointReflection_fixed_iff, AffineIsometryEquiv.coe_toIsometryEquiv, AffineIsometryEquiv.pointReflection_self, AffineIsometryEquiv.pointReflection_symm, IsometryEquiv.symm_apply_eq, IsometryEquiv.eq_symm_apply, AffineIsometryEquiv.toIsometryEquiv_symm