-- 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)
m : ℤ
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
nat :
  ∀ (m : ℕ),
    (HPow.hPow (β := ℤ) (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)
⊢ ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R ((m - 2) / 2)) *
            (Polynomial.eval t (S R ((m - 1) / 2)) + Polynomial.eval t (S R ((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 ((m - 1) / 2)) *
          (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((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)
have neg : (∀ (n : ℕ),
    (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑n : ℤ) : (a : M) → M) z =
      z +
          (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2 / 2)) *
              (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1 / 2)) +
                Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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 (α := ℤ) (↑n : ℤ) 1 / 2)) *
            (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑n : ℤ) 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 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)) →
  ∀ (m : ℕ),
    (HPow.hPow (β := ℤ) (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)
Tactic: induction m using Int.negInduction with
  | nat m => exact_mod_cast reflection_mul_reflection_pow_apply hf hg m z t ht
  | neg _ m =>
    have ht' : t = g x * f y - 2 := by rwa [mul_comm (g x)]
    rw [zpow_neg, ← inv_zpow, mul_inv_rev, reflection_inv, reflection_inv, zpow_natCast,
      reflection_mul_reflection_pow_apply hg hf m z t ht', add_right_comm z]
    have aux (a b : ℤ) (hab : a + b = -3 := by lia) : a / 2 = -(b / 2) - 2 := by lia
    rw [aux (-m - 3) m, aux (-m - 2) (m - 1), aux (-m - 1) (m - 2), aux (-m) (m - 3)]
    simp only [S_neg_sub_two, Polynomial.eval_neg]
    ring_nf
Cleared hypotheses: m