Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: 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 : R
ht : t = f y * g x - 2
m : ℕ
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
k : ℤ := ↑m / 2
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 k) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
e : ℤ
he : e = 0 ∨ e = 1
⊢ -(f z * 1) - g z * -(f y * 1) +
        Polynomial.eval t (S R ((e - 2) / 2 + k)) *
            (Polynomial.eval t (S R ((e - 1) / 2 + k)) + Polynomial.eval t (S R ((e - 3) / 2 + k))) *
          ((g x * f z - g z) * (-(f y * 1) - 2 * -(f y * 1)) - f z * (1 - 2 * 1 - g x * -(f y * 1))) +
      Polynomial.eval t (S R ((e - 1) / 2 + k)) *
          (Polynomial.eval t (S R (e / 2 + k)) + Polynomial.eval t (S R ((e - 2) / 2 + k))) *
        ((f y * g z - f z) * (1 - 2 * 1 - g x * -(f y * 1)) - g z * (-(f y * 1) - 2 * -(f y * 1))) =
    Polynomial.eval t (S R ((e + 1 - 2) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 3) / 2 + k))) *
        -(f z * 1) +
      Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 2) / 2 + k))) *
        ((f y * g z - f z) * 1)

pp: 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 : R
ht : t = f y * g x - 2
m : ℕ
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
k : ℤ := ↑m / 2
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 k) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
e : ℤ
he : e = 0 ∨ e = 1
⊢ -(g z * 1) +
        Polynomial.eval t (S R ((e - 2) / 2 + k)) *
            (Polynomial.eval t (S R ((e - 1) / 2 + k)) + Polynomial.eval t (S R ((e - 3) / 2 + k))) *
          ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
      Polynomial.eval t (S R ((e - 1) / 2 + k)) *
          (Polynomial.eval t (S R (e / 2 + k)) + Polynomial.eval t (S R ((e - 2) / 2 + k))) *
        ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) =
    Polynomial.eval t (S R ((e + 1 - 2) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 3) / 2 + k))) *
        ((g x * f z - g z) * 1) +
      Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 2) / 2 + k))) *
        -(g z * 1)

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

Goal state after:
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 : R
ht : t = f y * g x - 2
m : ℕ
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
k : ℤ := ↑m / 2
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 k) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
e : ℤ
he : e = 0 ∨ e = 1
⊢ -(g z * 1) +
        Polynomial.eval t (S R ((e - 2) / 2 + k)) *
            (Polynomial.eval t (S R ((e - 1) / 2 + k)) + Polynomial.eval t (S R ((e - 3) / 2 + k))) *
          ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
      Polynomial.eval t (S R ((e - 1) / 2 + k)) *
          (Polynomial.eval t (S R (e / 2 + k)) + Polynomial.eval t (S R ((e - 2) / 2 + k))) *
        ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) =
    Polynomial.eval t (S R ((e + 1 - 2) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 3) / 2 + k))) *
        ((g x * f z - g z) * 1) +
      Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 2) / 2 + k))) *
        -(g z * 1)