-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
f g : Dual R M
hf : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hg : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 3 / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) •
              y -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x) +
      (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑m : ℤ) 2)) +
            Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)))) •
        (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
              ((f : (a : M) → R) z : R) •
            x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R) y)
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    HPow.hPow (β := ℕ) (Polynomial.eval t (S R k)) 2 + HPow.hPow (β := ℕ) (Polynomial.eval t (S R (k + 1))) 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
⊢ z - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R)
            (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x) +
        (Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 2) / 2)) *
            (Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 1) / 2)) +
              Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 3) / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) •
              (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x -
                HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
                  (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x)) -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R)
              (x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 x -
                HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R)
                  (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x))) +
      (Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 1) / 2)) *
          (Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2) / 2)) +
            Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 2) / 2)))) •
        (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
              ((f : (a : M) → R) z : R) •
            (x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 x -
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R)
                (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x)) -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R)
            (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x -
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
                (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x))) =
    z +
        (Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 2) / 2)) *
            (Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 1) / 2)) +
              Polynomial.eval t
                (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 3) / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) •
              y -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x) +
      (Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 1) / 2)) *
          (Polynomial.eval t (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1) / 2)) +
            Polynomial.eval t
              (S R ((2 * HDiv.hDiv (α := ℤ) (↑m : ℤ) 2 + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 2) / 2)))) •
        (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
              ((f : (a : M) → R) z : R) •
            x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R) y)
have succ : let k := HDiv.hDiv (α := ℤ) (↑m : ℤ) 2;
∀
  (ih :
    ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
      z +
          (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
              (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
                Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 3 / 2)))) •
            (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                  ((g : (a : M) → R) z : R) •
                y -
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x) +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
            (Polynomial.eval t (S R k) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
                ((f : (a : M) → R) z : R) •
              x -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R) y)),
  z - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R)
            (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x) +
        (Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 2) / 2)) *
            (Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 1) / 2)) +
              Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 3) / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) •
              (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x -
                HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
                  (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x)) -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R)
              (x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 x -
                HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R)
                  (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x))) +
      (Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 1) / 2)) *
          (Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2) / 2)) +
            Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 - 2) / 2)))) •
        (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
              ((f : (a : M) → R) z : R) •
            (x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 x -
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R)
                (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x)) -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R)
            (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x -
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2
                (y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x))) =
    z +
        (Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 2) / 2)) *
            (Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 1) / 2)) +
              Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 3) / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) •
              y -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x) +
      (Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 1) / 2)) *
          (Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1) / 2)) +
            Polynomial.eval t (S R ((2 * k + HMod.hMod (α := ℤ) (↑m : ℤ) 2 + 1 - 2) / 2)))) •
        (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
              ((f : (a : M) → R) z : R) •
            x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R) y)
Tactic: set k : ℤ := m / 2
Cleared hypotheses: ih