-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma two_nsmul_reflection_eq_of_perm_eq (hij : P.reflection_perm i = P.reflection_perm j) :
    2 • ⇑(P.reflection i) = 2 • P.reflection j

Proof state:
case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.toLin x) (P.pairing i j • P.coroot i) • P.root j = (P.toLin x) (2 • P.coroot j) • P.root j

Tactic:
rw [← P.pairing_smul_coroot_eq j i j hij.symm, pairing_same]

Result:
no goals

Proof state:
case h
ι : 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.reflection_perm i = P.reflection_perm j
x : M
⊢ 2 • (P.toLin x) (P.coroot i) • P.root i = 2 • (P.toLin x) (P.coroot j) • P.root j

Tactic:
calc 2 • P.toLin x (P.coroot i) • P.root i
    = P.toLin x (P.coroot i) • ((2 : R) • P.root i) := ?_
  _ = P.toLin x (P.coroot i) • (P.pairing i j • P.root j) := ?_
  _ = P.toLin x (P.pairing i j • P.coroot i) • (P.root j) := ?_
  _ = P.toLin x ((2 : R) • P.coroot j) • (P.root j) := ?_
  _ = 2 • P.toLin x (P.coroot j) • P.root j := ?_

Result:
case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ 2 • (P.toLin x) (P.coroot i) • P.root i = (P.toLin x) (P.coroot i) • 2 • P.root i

case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.toLin x) (P.coroot i) • 2 • P.root i = (P.toLin x) (P.coroot i) • P.pairing i j • P.root j

case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.toLin x) (P.coroot i) • P.pairing i j • P.root j = (P.toLin x) (P.pairing i j • P.coroot i) • P.root j

case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.toLin x) (P.pairing i j • P.coroot i) • P.root j = (P.toLin x) (2 • P.coroot j) • P.root j

case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.toLin x) (2 • P.coroot j) • P.root j = 2 • (P.toLin x) (P.coroot j) • P.root j

Proof state:
ι : 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.reflection_perm i = P.reflection_perm j
⊢ 2 • ⇑(P.reflection i) = 2 • ⇑(P.reflection j)

Tactic:
ext x

Result:
case h
ι : 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.reflection_perm i = P.reflection_perm j
x : M
⊢ (2 • ⇑(P.reflection i)) x = (2 • ⇑(P.reflection j)) x

Proof state:
case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.toLin x) (2 • P.coroot j) • P.root j = 2 • (P.toLin x) (P.coroot j) • P.root j

Tactic:
rw [map_smul, smul_assoc, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]

Result:
no goals

Proof state:
case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.toLin x) (P.coroot i) • P.pairing i j • P.root j = (P.toLin x) (P.pairing i j • P.coroot i) • P.root j

Tactic:
rw [← smul_comm, ← smul_assoc, map_smul]

Result:
no goals

Proof state:
case h
ι : 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.reflection_perm i = P.reflection_perm j
x : M
⊢ (2 • ⇑(P.reflection i)) x = (2 • ⇑(P.reflection j)) x

Tactic:
suffices 2 • P.toLin x (P.coroot i) • P.root i = 2 • P.toLin x (P.coroot j) • P.root j by
  simpa [reflection_apply, smul_sub]

Result:
case h
ι : 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.reflection_perm i = P.reflection_perm j
x : M
⊢ 2 • (P.toLin x) (P.coroot i) • P.root i = 2 • (P.toLin x) (P.coroot j) • P.root j

Proof state:
ι : 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.reflection_perm i = P.reflection_perm j
x : M
this : 2 • (P.toLin x) (P.coroot i) • P.root i = 2 • (P.toLin x) (P.coroot j) • P.root j
⊢ (2 • ⇑(P.reflection i)) x = (2 • ⇑(P.reflection j)) x

Tactic:
simpa [reflection_apply, smul_sub]

Result:
no goals

Proof state:
case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ 2 • (P.toLin x) (P.coroot i) • P.root i = (P.toLin x) (P.coroot i) • 2 • P.root i

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

Result:
no goals

Proof state:
case h.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.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.toLin x) (P.coroot i) • 2 • P.root i = (P.toLin x) (P.coroot i) • P.pairing i j • P.root j

Tactic:
rw [P.pairing_smul_root_eq j i i hij.symm, pairing_same]

Result:
no goals