Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: case calc_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ 2 • (P.toLinearMap x) (P.coroot i) • P.root i = (P.toLinearMap x) (P.coroot i) • 2 • P.root i

pp: case calc_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.coroot i) • 2 • P.root i = (P.toLinearMap x) (P.coroot i) • P.pairing i j • P.root j

pp: case calc_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.coroot i) • P.pairing i j • P.root j = (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j

pp: case calc_4
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j = (P.toLinearMap x) (2 • P.coroot j) • P.root j

pp: case calc_5
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (2 • P.coroot j) • P.root j = 2 • (P.toLinearMap x) (P.coroot j) • P.root j

Tactic:
· rw [smul_comm, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]

Goal state after:
case calc_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.coroot i) • 2 • P.root i = (P.toLinearMap x) (P.coroot i) • P.pairing i j • P.root j

case calc_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.coroot i) • P.pairing i j • P.root j = (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j

case calc_4
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j = (P.toLinearMap x) (2 • P.coroot j) • P.root j

case calc_5
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (2 • P.coroot j) • P.root j = 2 • (P.toLinearMap x) (P.coroot j) • P.root j