-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
theorem exists_ge_zero_eq_rootForm [Fintype ι] (x : M) (hx : x ∈ span S (range P.root)) :
    ∃ s ≥ 0, algebraMap S R s = P.RootForm x x

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
S : Type u_5
inst✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
⊢ ∃ s ≥ 0, (algebraMap S R) s = (P.RootForm x) x

Tactic:
refine ⟨(P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩, IsSumSq.nonneg ?_, by simp [posRootForm]⟩

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
S : Type u_5
inst✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
⊢ IsSumSq (((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩)

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
S : Type u_5
inst✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
⊢ IsSumSq (((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩)

Tactic:
choose s hs using P.coroot'_apply_apply_mem_of_mem_span S hx

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
S : Type u_5
inst✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
s : ι → S
hs : ∀ (i : ι), (algebraMap S R) (s i) = (P.coroot' i) x
⊢ IsSumSq (((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩)

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
S : Type u_5
inst✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
⊢ (algebraMap S R) (((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩) = (P.RootForm x) x

Tactic:
simp [posRootForm]

Result:
no goals

Proof state:
case a
ι : 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✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
s : ι → S
hs : ∀ (i : ι), (algebraMap S R) (s i) = (P.coroot' i) x
⊢ (P.RootForm x) x = ∑ x : ι, (algebraMap S R) (s x) * (algebraMap S R) (s x)

Tactic:
simp [← Algebra.linearMap_apply, hs, rootForm_apply_apply]

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
S : Type u_5
inst✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
s : ι → S
hs : ∀ (i : ι), (algebraMap S R) (s i) = (P.coroot' i) x
⊢ IsSumSq (((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩)

Tactic:
suffices (P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩ = ∑ i, s i * s i from
  this ▸ IsSumSq.sum_mul_self Finset.univ s

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
S : Type u_5
inst✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
s : ι → S
hs : ∀ (i : ι), (algebraMap S R) (s i) = (P.coroot' i) x
⊢ ((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩ = ∑ i : ι, s i * s i

Proof state:
case a
ι : 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✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
s : ι → S
hs : ∀ (i : ι), (algebraMap S R) (s i) = (P.coroot' i) x
⊢ (algebraMap S R) (((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩) = (algebraMap S R) (∑ i : ι, s i * s i)

Tactic:
simp only [posRootForm, RootPositiveForm.algebraMap_posForm, map_sum, map_mul]

Result:
case a
ι : 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✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
s : ι → S
hs : ∀ (i : ι), (algebraMap S R) (s i) = (P.coroot' i) x
⊢ (P.RootForm x) x = ∑ x : ι, (algebraMap S R) (s x) * (algebraMap S R) (s x)

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
S : Type u_5
inst✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
s : ι → S
hs : ∀ (i : ι), (algebraMap S R) (s i) = (P.coroot' i) x
⊢ ((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩ = ∑ i : ι, s i * s i

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Result:
case a
ι : 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✝⁶ : LinearOrderedCommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : M
hx : x ∈ span S (range ⇑P.root)
s : ι → S
hs : ∀ (i : ι), (algebraMap S R) (s i) = (P.coroot' i) x
⊢ (algebraMap S R) (((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩) = (algebraMap S R) (∑ i : ι, s i * s i)