-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma isOrthogonal_comm (h : IsOrthogonal P i j) : Commute (P.reflection i) (P.reflection j)

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 : ι
v : M
h : P.pairing i j = 0 ∧ P.pairing j i = 0
⊢ v - (P.toPerfectPairing v) (P.coroot i) • P.root i - (P.toPerfectPairing v) (P.coroot j) • P.root j =
    v - (P.toPerfectPairing v) (P.coroot j) • P.root j - (P.toPerfectPairing v) (P.coroot i) • P.root i

Tactic:
abel

Result:
no goals

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 : ι
h : P.IsOrthogonal i j
v : M
⊢ P.pairing i j = 0 ∧ P.pairing j i = 0

Tactic:
simpa [IsOrthogonal] using h

Result:
no goals

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 : ι
h : P.IsOrthogonal i j
⊢ Commute (P.reflection i) (P.reflection j)

Tactic:
rw [commute_iff_eq]

Result:
ι : 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 : ι
h : P.IsOrthogonal i j
⊢ P.reflection i * P.reflection j = P.reflection j * P.reflection i

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 : ι
h : P.IsOrthogonal i j
v : M
⊢ (P.reflection i * P.reflection j) v = (P.reflection j * P.reflection i) v

Tactic:
replace h : P.pairing i j = 0 ∧ P.pairing j i = 0 := by simpa [IsOrthogonal] using h

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 : ι
v : M
h : P.pairing i j = 0 ∧ P.pairing j i = 0
⊢ (P.reflection i * P.reflection j) v = (P.reflection j * P.reflection i) v

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 : ι
v : M
h : P.pairing i j = 0 ∧ P.pairing j i = 0
⊢ (P.reflection i * P.reflection j) v = (P.reflection j * P.reflection i) v

Tactic:
erw [LinearMap.mul_apply, LinearMap.mul_apply]

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 : ι
v : M
h : P.pairing i j = 0 ∧ P.pairing j i = 0
⊢ ↑(P.reflection i) (↑(P.reflection j) v) = ↑(P.reflection j) (↑(P.reflection i) v)

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 : ι
v : M
h : P.pairing i j = 0 ∧ P.pairing j i = 0
⊢ ↑(P.reflection i) (↑(P.reflection j) v) = ↑(P.reflection j) (↑(P.reflection i) v)

Tactic:
simp only [LinearEquiv.coe_coe, reflection_apply, PerfectPairing.flip_apply_apply, map_sub,
  map_smul, root_coroot_eq_pairing, h, zero_smul, sub_zero]

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 : ι
v : M
h : P.pairing i j = 0 ∧ P.pairing j i = 0
⊢ v - (P.toPerfectPairing v) (P.coroot i) • P.root i - (P.toPerfectPairing v) (P.coroot j) • P.root j =
    v - (P.toPerfectPairing v) (P.coroot j) • P.root j - (P.toPerfectPairing v) (P.coroot i) • P.root i

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 : ι
h : P.IsOrthogonal i j
⊢ P.reflection i * P.reflection j = P.reflection j * P.reflection i

Tactic:
ext v

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 : ι
h : P.IsOrthogonal i j
v : M
⊢ (P.reflection i * P.reflection j) v = (P.reflection j * P.reflection i) v