-- Mathlib/LinearAlgebra/Reflection.lean
/-- A formula for $(r_1 r_2)^m z$, where $m$ is a natural number and $z \in M$. -/
lemma reflection_mul_reflection_pow_apply (m : ℕ) (z : M)
    (t : R := f y * g x - 2) (ht : t = f y * g x - 2

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ 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)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • 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)
k : ℤ
⊢ Polynomial.eval t (S R k) ^ 2 + Polynomial.eval t (S R (k + 1)) ^ 2 -
      t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
    1

Tactic:
simpa using congr_arg (Polynomial.eval t) (S_sq_add_S_sq R k)

Result:
no goals

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ 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)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • 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 : ℤ),
    Polynomial.eval t (S R k) ^ 2 + Polynomial.eval t (S R (k + 1)) ^ 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
⊢ z - f z • x - g z • (y - f y • x) +
        (Polynomial.eval t (S R ((↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • (y - f y • x - 2 • (y - f y • x)) - f z • (x - 2 • x - g x • (y - f y • x))) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • (x - 2 • x - g x • (y - f y • x)) - g z • (y - f y • x - 2 • (y - f y • x))) =
    z +
        (Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)) *
            (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) *
          (Polynomial.eval t (S R (↑(m + 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
push_cast

Result:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ 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)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • 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 : ℤ),
    Polynomial.eval t (S R k) ^ 2 + Polynomial.eval t (S R (k + 1)) ^ 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
⊢ z - f z • x - g z • (y - f y • x) +
        (Polynomial.eval t (S R ((↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • (y - f y • x - 2 • (y - f y • x)) - f z • (x - 2 • x - g x • (y - f y • x))) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • (x - 2 • x - g x • (y - f y • x)) - g z • (y - f y • x - 2 • (y - f y • x))) =
    z +
        (Polynomial.eval t (S R ((↑m + 1 - 2) / 2)) *
            (Polynomial.eval t (S R ((↑m + 1 - 1) / 2)) + Polynomial.eval t (S R ((↑m + 1 - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m + 1 - 1) / 2)) *
          (Polynomial.eval t (S R ((↑m + 1) / 2)) + Polynomial.eval t (S R ((↑m + 1 - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ 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)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
⊢ ((reflection hf * reflection hg) ^ (m + 1)) z =
    z +
        (Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)) *
            (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) *
          (Polynomial.eval t (S R (↑(m + 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
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]

Result:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ 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)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • 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)
⊢ ((reflection hf * reflection hg) ^ (m + 1)) z =
    z +
        (Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)) *
            (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) *
          (Polynomial.eval t (S R (↑(m + 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)