-- Mathlib/LinearAlgebra/Reflection.lean
/-- Composite of reflections in "parallel" hyperplanes is a shear (special case). -/
lemma reflection_reflection_iterate
    (hfx : f x = 2) (hgy : g y = 2) (hgxfy : f y * g x = 4) (n : ℕ) :
    ((reflection hgy).trans (reflection hfx))^[n] y = y + n • (f y • x - (2 : R) • y)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  have hz : ∀ z : M, f y • g x • z = 2 • 2 • z := by
    intro z
    rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
      Nat.cast_ofNat]
  simp only [iterate_succ', comp_apply, ih, two_smul, smul_sub, smul_add, map_add,
    LinearEquiv.trans_apply, reflection_apply_self, map_neg, reflection_apply, neg_sub, map_sub,
    map_nsmul, map_smul, smul_neg, hz, add_smul]
  abel

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
⊢ ∀ (z : M), f y • g x • z = 2 • 2 • z

Tactic:
intro z

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
z : M
⊢ f y • g x • z = 2 • 2 • z

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
hz : ∀ (z : M), f y • g x • z = 2 • 2 • z
⊢ f y • x - y +
      (-(n • f y • x) - (n • y + n • y + (n • y + n • y) - (n • f y • x + n • f y • x + (n • f y • x + n • f y • x))) -
        (n • f y • x - n • y + (n • f y • x - n • y))) =
    y + (n • f y • x + 1 • f y • x - (n • y + 1 • y + (n • y + 1 • y)))

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
z : M
⊢ f y • g x • z = 2 • 2 • z

Tactic:
rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
  Nat.cast_ofNat]

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 : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
hz : ∀ (z : M), f y • g x • z = 2 • 2 • z
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n + 1] y = y + (n + 1) • (f y • x - 2 • y)

Tactic:
simp only [iterate_succ', comp_apply, ih, two_smul, smul_sub, smul_add, map_add,
  LinearEquiv.trans_apply, reflection_apply_self, map_neg, reflection_apply, neg_sub, map_sub,
  map_nsmul, map_smul, smul_neg, hz, add_smul]

Result:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
hz : ∀ (z : M), f y • g x • z = 2 • 2 • z
⊢ f y • x - y +
      (-(n • f y • x) - (n • y + n • y + (n • y + n • y) - (n • f y • x + n • f y • x + (n • f y • x + n • f y • x))) -
        (n • f y • x - n • y + (n • f y • x - n • y))) =
    y + (n • f y • x + 1 • f y • x - (n • y + 1 • y + (n • y + 1 • y)))

Proof state:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[0] y = y + 0 • (f y • x - 2 • y)

Tactic:
simp

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 : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n + 1] y = y + (n + 1) • (f y • x - 2 • y)

Tactic:
have hz : ∀ z : M, f y • g x • z = 2 • 2 • z := by
  intro z
  rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
    Nat.cast_ofNat]

Result:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
hz : ∀ (z : M), f y • g x • z = 2 • 2 • z
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n + 1] y = y + (n + 1) • (f y • x - 2 • y)