-- 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 : ℕ
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
zero :
  (HPow.hPow (β := ℕ) (reflection hf * reflection hg) 0 : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑0 : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑0 : ℤ) 1 / 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑0 : ℤ) 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 (α := ℤ) (↑0 : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑0 : ℤ) 2)) +
            Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑0 : ℤ) 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)
succ :
  ∀ (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)),
    ((reflection hf * reflection hg) ^ (m + 1) : (a : M) → M) z =
      z +
          (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 2 / 2)) *
              (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 1 / 2)) +
                Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 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 (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 1 / 2)) *
            (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑(m + 1) : ℤ) 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑(m + 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)
⊢ ((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 with
  | zero => simp
  | succ m ih =>
    /- Now, let us collect two facts about the evaluations of `S r k`. These easily follow from the
    properties of the `S` polynomials. -/
    have S_eval_t_sub_two (k : ℤ) :
        (S R (k - 2)).eval t = t * (S R (k - 1)).eval t - (S R k).eval t := by
      simp [S_sub_two]
    have S_eval_t_sq_add_S_eval_t_sq (k : ℤ) :
        (S R k).eval t ^ 2 + (S R (k + 1)).eval t ^ 2 - t * (S R k).eval t * (S R (k + 1)).eval t
        = 1 := by
      simpa using congr_arg (Polynomial.eval t) (S_sq_add_S_sq R k)
    -- Apply the inductive hypothesis.
    rw [pow_succ', LinearEquiv.mul_apply, ih, LinearEquiv.mul_apply]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- `m` can be written in the form `2 * k + e`, where `e` is `0` or `1`.
    push_cast
    rw [← Int.mul_ediv_add_emod m 2]
    set k : ℤ := m / 2
    set e : ℤ := m % 2
    simp_rw [add_assoc (2 * k), add_sub_assoc (2 * k), add_comm (2 * k),
      add_mul_ediv_left _ k (by simp : (2 : ℤ) ≠ 0)]
    have he : e = 0 ∨ e = 1 := by lia
    clear_value e
    /- Now, equate the coefficients on both sides. These linear combinations were
    found using `polyrith`. -/
    match_scalars
    · rfl
    · linear_combination (norm := skip) (-g z * f y * (S R (e - 1 + k)).eval t +
          f z * (S R (e - 1 + k)).eval t) * S_eval_t_sub_two (e + k) +
          (-g z * f y + f z) * S_eval_t_sq_add_S_eval_t_sq (k - 1)
      subst ht
      obtain rfl | rfl : e = 0 ∨ e = 1 := he <;> ring_nf
    · linear_combination (norm := skip)
          g z * (S R (e - 1 + k)).eval t * S_eval_t_sub_two (e + k) +
          g z * S_eval_t_sq_add_S_eval_t_sq (k - 1)
      subst ht
      obtain rfl | rfl : e = 0 ∨ e = 1 := he <;> ring_nf

Premises used: HMul.hMul, map_sub, LinearEquiv.mul_apply, map_add, Int.mul_ediv_add_emod, Nat.cast, HAdd.hAdd, Int.succ, Module.reflection_apply, OfNat.ofNat, DFunLike.coe, pow_succ', Neg.neg, rfl, map_smul