-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
lemma coxeterWeight_zero_iff_isOrthogonal :
    P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j

Proof state:
case inl
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
h : P.pairing i j = 0
⊢ P.IsOrthogonal i j

Tactic:
exact ⟨h, (pairing_zero_iff B i j).mp h⟩

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
⊢ P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j

Tactic:
rw [coxeterWeight, mul_eq_zero]

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
⊢ P.pairing i j = 0 ∨ P.pairing j i = 0 ↔ P.IsOrthogonal i j

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
h : P.pairing i j = 0 ∨ P.pairing j i = 0
⊢ P.IsOrthogonal i j

Tactic:
rcases h with h | h

Result:
case inl
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
h : P.pairing i j = 0
⊢ P.IsOrthogonal i j

case inr
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
h : P.pairing j i = 0
⊢ P.IsOrthogonal i j

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
⊢ P.pairing i j = 0 ∨ P.pairing j i = 0 ↔ P.IsOrthogonal i j

Tactic:
refine ⟨fun h => ?_, fun h => Or.inl h.1⟩

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
h : P.pairing i j = 0 ∨ P.pairing j i = 0
⊢ P.IsOrthogonal i j

Proof state:
case inr
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
h : P.pairing j i = 0
⊢ P.IsOrthogonal i j

Tactic:
exact ⟨(pairing_zero_iff B j i).mp h, h⟩

Result:
no goals