-- Module: Mathlib.LinearAlgebra.Reflection
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 : ℤ
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) =
      (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2) *
          Polynomial.eval t (S R (k - 1)) -
        Polynomial.eval t (S R k)
zero :
  (HPow.hPow (β := ℤ) (reflection hf * reflection hg) 0 : (a : M) → M) x =
    (Polynomial.eval t (S R 0) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) 0 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) 0 1))) (-(g : (a : M) → R) x : R) • y
succ :
  ∀ (m : ℕ)
    (ih :
      (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (↑m : ℤ) : (a : M) → M) x =
        (Polynomial.eval t (S R (↑m : ℤ)) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) • x +
          HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1))) (-(g : (a : M) → R) x : R) • y),
    ((reflection hf * reflection hg) ^ HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 : (a : M) → M) x =
      (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) +
            Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 1))) •
          x +
        HMul.hMul (β := R) (Polynomial.eval t (S R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 1))) (-(g : (a : M) → R) x : R) • y
pred :
  ∀ (m : ℕ)
    (ih :
      (HPow.hPow (β := ℤ) (reflection hf * reflection hg) (-(↑m : ℤ)) : (a : M) → M) x =
        (Polynomial.eval t (S R (-(↑m : ℤ))) + Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) • x +
          HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1))) (-(g : (a : M) → R) x : R) •
            y),
    ((reflection hf * reflection hg) ^ HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 : (a : M) → M) x =
      (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) +
            Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 - 1))) •
          x +
        HMul.hMul (β := R) (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 - 1))) (-(g : (a : M) → R) x : R) •
          y
⊢ ((reflection hf * reflection hg) ^ m : (a : M) → M) x =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x +
      HMul.hMul (β := R) (Polynomial.eval t (S R (m - 1))) (-(g : (a : M) → R) x : R) • y

Tactic:
induction m with
  | zero => simp
  | succ m ih =>
    -- Apply the inductive hypothesis.
    rw [add_comm (m : ℤ) 1, zpow_one_add, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- Equate coefficients of `x` and `y`.
    match_scalars
    · linear_combination (norm := ring_nf) -S_eval_t_sub_two (m + 1)
    · ring_nf
  | pred m ih =>
    -- Apply the inductive hypothesis.
    rw [sub_eq_add_neg (-m : ℤ) 1, add_comm (-m : ℤ) (-1), zpow_add, zpow_neg_one, mul_inv_rev,
      reflection_inv, reflection_inv, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- Equate coefficients of `x` and `y`.
    match_scalars
    · linear_combination (norm := ring_nf) -S_eval_t_sub_two (-m)
    · linear_combination (norm := ring_nf) g x * S_eval_t_sub_two (-m)

Premises used: zpow_add, map_sub, zpow_neg_one, Module.reflection_inv, Int.pred, sub_eq_add_neg, LinearEquiv.mul_apply, zpow_one_add, map_add, add_comm, HAdd.hAdd, Int.succ, mul_inv_rev, Module.reflection_apply, OfNat.ofNat, DFunLike.coe, Neg.neg, map_smul