-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
@[simp]
lemma zero_lt_apply_root_root_iff
    (hi : P.root i ∈ span S (range P.root) := subset_span (mem_range_self i))
    (hj : P.root j ∈ span S (range P.root) := subset_span (mem_range_self j)) :
    0 < B.posForm ⟨P.root i, hi⟩ ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S 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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
this : 2 * (B.posForm ri) rj = P.pairingIn S i j * (B.posForm rj) rj
⊢ 0 < 2 * (B.posForm ri) rj ↔ 0 < P.pairingIn S i j * (B.posForm rj) rj

Tactic:
rw [this]

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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
this : 2 * (B.posForm ri) rj = P.pairingIn S i j * (B.posForm rj) rj
⊢ 0 < (B.posForm ri) rj ↔ 0 < 2 * (B.posForm ri) rj

Tactic:
rw [mul_pos_iff_of_pos_left zero_lt_two]

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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S i j

Tactic:
let rj : span S (range P.root) := ⟨P.root j, hj⟩

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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S 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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S i j

Tactic:
let ri : span S (range P.root) := ⟨P.root i, hi⟩

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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S 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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
this : 2 * (B.posForm ri) rj = P.pairingIn S i j * (B.posForm rj) rj
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S i j

Tactic:
calc  0 < B.posForm ri rj
    ↔ 0 < 2 * B.posForm ri rj := by rw [mul_pos_iff_of_pos_left zero_lt_two]
  _ ↔ 0 < P.pairingIn S i j * B.posForm rj rj := by rw [this]
  _ ↔ 0 < P.pairingIn S i j := by rw [mul_pos_iff_of_pos_right (B.zero_lt_posForm_apply_root j)]

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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S i j

Tactic:
have : 2 * B.posForm ri rj = P.pairingIn S i j * B.posForm rj rj := by
  apply FaithfulSMul.algebraMap_injective S R
  simpa [map_ofNat] using two_mul_apply_root_root B i j

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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
this : 2 * (B.posForm ri) rj = P.pairingIn S i j * (B.posForm rj) rj
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S 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✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
this : 2 * (B.posForm ri) rj = P.pairingIn S i j * (B.posForm rj) rj
⊢ 0 < P.pairingIn S i j * (B.posForm rj) rj ↔ 0 < P.pairingIn S i j

Tactic:
rw [mul_pos_iff_of_pos_right (B.zero_lt_posForm_apply_root j)]

Result:
no goals