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

Proof state:
case neg
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✝
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
aux : ∀ (a b : ℤ), autoParam (a + b = -3) _auto✝ → a / 2 = -(b / 2) - 2
⊢ z +
        (Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
          ((g x * f z - g z) • y - f z • 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)))) •
        ((f y * g z - f z) • x - g z • y) =
    z +
        (Polynomial.eval t (S R (-((↑m - 1) / 2) - 2)) *
            (Polynomial.eval t (S R (-((↑m - 2) / 2) - 2)) + Polynomial.eval t (S R (-(↑m / 2) - 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R (-((↑m - 2) / 2) - 2)) *
          (Polynomial.eval t (S R (-((↑m - 3) / 2) - 2)) + Polynomial.eval t (S R (-((↑m - 1) / 2) - 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
simp only [S_neg_sub_two, Polynomial.eval_neg]

Result:
case neg
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✝
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
aux : ∀ (a b : ℤ), autoParam (a + b = -3) _auto✝ → a / 2 = -(b / 2) - 2
⊢ z +
        (Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
          ((g x * f z - g z) • y - f z • 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)))) •
        ((f y * g z - f z) • x - g z • y) =
    z +
        (-Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (-Polynomial.eval t (S R ((↑m - 2) / 2)) + -Polynomial.eval t (S R (↑m / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (-Polynomial.eval t (S R ((↑m - 2) / 2)) *
          (-Polynomial.eval t (S R ((↑m - 3) / 2)) + -Polynomial.eval t (S R ((↑m - 1) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Proof state:
case neg
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✝
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
aux : ∀ (a b : ℤ), autoParam (a + b = -3) _auto✝ → a / 2 = -(b / 2) - 2
⊢ z +
        (Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
          ((g x * f z - g z) • y - f z • 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)))) •
        ((f y * g z - f z) • x - g z • y) =
    z +
        (-Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (-Polynomial.eval t (S R ((↑m - 2) / 2)) + -Polynomial.eval t (S R (↑m / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (-Polynomial.eval t (S R ((↑m - 2) / 2)) *
          (-Polynomial.eval t (S R ((↑m - 3) / 2)) + -Polynomial.eval t (S R ((↑m - 1) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
ring_nf

Result:
no goals

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
m : ℤ
z : M
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
⊢ ((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)

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 omega) : a / 2 = -(b / 2) - 2 := by omega
  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

Result:
no goals