Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

Goal state before:
pp: case inl.inl
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i = 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

pp: case inl.inr
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

pp: case inr.inl
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i = 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

pp: case inr.inr
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

Tactic:
· rw [hij, hji]

Goal state after:
case inl.inr
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

case inr.inl
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i = 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

case inr.inr
ι : 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
S : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0