-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
lemma zero_lt_posForm_iff {x y : span S (range P.root)} :
    0 < B.posForm x y ↔ ∃ s > 0, algebraMap S R s = B.form x y

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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
x✝ : ∃ s > 0, (algebraMap S R) s = (B.form ↑x) ↑y
s : S
h : s > 0
h' : (algebraMap S R) s = (B.form ↑x) ↑y
⊢ 0 < (B.posForm x) y

Tactic:
rw [← B.algebraMap_posForm] at h'

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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
x✝ : ∃ s > 0, (algebraMap S R) s = (B.form ↑x) ↑y
s : S
h : s > 0
h' : (algebraMap S R) s = (algebraMap S R) ((B.posForm x) y)
⊢ 0 < (B.posForm x) y

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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ 0 < (B.posForm x) y ↔ ∃ s > 0, (algebraMap S R) s = (B.form ↑x) ↑y

Tactic:
refine ⟨fun h ↦ ⟨B.posForm x y, h, by simp⟩, fun ⟨s, h, h'⟩ ↦ ?_⟩

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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
x✝ : ∃ s > 0, (algebraMap S R) s = (B.form ↑x) ↑y
s : S
h : s > 0
h' : (algebraMap S R) s = (B.form ↑x) ↑y
⊢ 0 < (B.posForm x) y

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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
x✝ : ∃ s > 0, (algebraMap S R) s = (B.form ↑x) ↑y
s : S
h : s > 0
h' : (algebraMap S R) s = (algebraMap S R) ((B.posForm x) y)
⊢ 0 < (B.posForm x) y

Tactic:
rwa [← FaithfulSMul.algebraMap_injective S R 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
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
h : 0 < (B.posForm x) y
⊢ (algebraMap S R) ((B.posForm x) y) = (B.form ↑x) ↑y

Tactic:
simp

Result:
no goals