-- Mathlib/LinearAlgebra/Reflection.lean
/-- A formula for $(r_1 r_2)^m x$, where $m$ is an integer. This is the special case of
`Module.reflection_mul_reflection_zpow_apply` with $z = x$. -/
lemma reflection_mul_reflection_zpow_apply_self (m : ℤ)
    (t : R := f y * g x - 2) (ht : t = f y * g x - 2

Proof state:
case hp
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
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ ↑m) x =
    (Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • x + (Polynomial.eval t (S R (↑m - 1)) * -g x) • y
⊢ ((reflection hf * reflection hg) ^ (↑m + 1)) x =
    (Polynomial.eval t (S R (↑m + 1)) + Polynomial.eval t (S R (↑m + 1 - 1))) • x +
      (Polynomial.eval t (S R (↑m + 1 - 1)) * -g x) • y

Tactic:
rw [add_comm (m : ℤ) 1, zpow_one_add, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]

Result:
case hp
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
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ ↑m) x =
    (Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • x + (Polynomial.eval t (S R (↑m - 1)) * -g x) • y
⊢ (reflection hf)
      ((reflection hg)
        ((Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • x +
          (Polynomial.eval t (S R (↑m - 1)) * -g x) • y)) =
    (Polynomial.eval t (S R (1 + ↑m)) + Polynomial.eval t (S R (1 + ↑m - 1))) • x +
      (Polynomial.eval t (S R (1 + ↑m - 1)) * -g x) • y

Proof state:
case hn
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
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y
⊢ (reflection hg)
      ((reflection hf)
        ((Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
          (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y)) =
    (Polynomial.eval t (S R (-1 + -↑m)) + Polynomial.eval t (S R (-1 + -↑m - 1))) • x +
      (Polynomial.eval t (S R (-1 + -↑m - 1)) * -g x) • y

Tactic:
simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]

Result:
case hn
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
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y
⊢ (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • (x - g x • y - 2 • (x - g x • y)) +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • (y - 2 • y - f y • (x - g x • y)) =
    (Polynomial.eval t (S R (-1 + -↑m)) + Polynomial.eval t (S R (-1 + -↑m - 1))) • x +
      (Polynomial.eval t (S R (-1 + -↑m - 1)) * -g x) • y

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 : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
⊢ ((reflection hf * reflection hg) ^ m) x =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x + (Polynomial.eval t (S R (m - 1)) * -g x) • y

Tactic:
have S_eval_t_sub_two (k : ℤ) :
    (S R (k - 2)).eval t = (f y * g x - 2) * (S R (k - 1)).eval t - (S R k).eval t := by
  simp [S_sub_two, ht]

Result:
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 : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
⊢ ((reflection hf * reflection hg) ^ m) x =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x + (Polynomial.eval t (S R (m - 1)) * -g x) • y

Proof state:
case hp
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
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ ↑m) x =
    (Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • x + (Polynomial.eval t (S R (↑m - 1)) * -g x) • y
⊢ (reflection hf)
      ((reflection hg)
        ((Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • x +
          (Polynomial.eval t (S R (↑m - 1)) * -g x) • y)) =
    (Polynomial.eval t (S R (1 + ↑m)) + Polynomial.eval t (S R (1 + ↑m - 1))) • x +
      (Polynomial.eval t (S R (1 + ↑m - 1)) * -g x) • y

Tactic:
simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]

Result:
case hp
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
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ ↑m) x =
    (Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • x + (Polynomial.eval t (S R (↑m - 1)) * -g x) • y
⊢ (Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • (x - 2 • x - g x • (y - f y • x)) +
      (Polynomial.eval t (S R (↑m - 1)) * -g x) • (y - f y • x - 2 • (y - f y • x)) =
    (Polynomial.eval t (S R (1 + ↑m)) + Polynomial.eval t (S R (1 + ↑m - 1))) • x +
      (Polynomial.eval t (S R (1 + ↑m - 1)) * -g x) • y

Proof state:
case hz
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
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
⊢ ((reflection hf * reflection hg) ^ 0) x =
    (Polynomial.eval t (S R 0) + Polynomial.eval t (S R (0 - 1))) • x + (Polynomial.eval t (S R (0 - 1)) * -g x) • y

Tactic:
simp

Result:
no goals