-- Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
/-- SGA3 XXI Prop. 2.3.1 -/
lemma coxeterWeightIn_le_four (S : Type*) [LinearOrderedCommRing S] [Algebra S R] [FaithfulSMul S R]
    [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] (i j : ι) :
    P.coxeterWeightIn S i j ≤ 4

Proof state:
case intro.intro.intro.intro
ι : 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
inst✝⁶ : Finite ι
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
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := ((P.posRootForm S).posForm ri) ri
lj : S := ((P.posRootForm S).posForm rj) rj
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : si > 0
sj : S
hsj : sj > 0
hsi' : si = li
hsj' : sj = lj
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
rw [hsi'] at hsi

Result:
case intro.intro.intro.intro
ι : 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
inst✝⁶ : Finite ι
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
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := ((P.posRootForm S).posForm ri) ri
lj : S := ((P.posRootForm S).posForm rj) rj
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : sj > 0
hsi' : si = li
hsj' : sj = lj
⊢ P.coxeterWeightIn S i j ≤ 4

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
inst✝⁶ : Finite ι
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
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := ((P.posRootForm S).posForm ri) ri
lj : S := ((P.posRootForm S).posForm rj) rj
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
cs : 4 * lij ^ 2 ≤ 4 * (li * lj)
⊢ (algebraMap S R) (4 • lij ^ 2) = (algebraMap S R) (P.coxeterWeightIn S i j • (li * lj))

Tactic:
simpa [map_ofNat, lij, posRootForm, ri, rj, li, lj] using
   P.four_smul_rootForm_sq_eq_coxeterWeight_smul i j

Result:
no goals

Proof state:
case intro.intro.intro.intro
ι : 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
inst✝⁶ : Finite ι
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
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := ((P.posRootForm S).posForm ri) ri
lj : S := ((P.posRootForm S).posForm rj) rj
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
cs : 4 * lij ^ 2 ≤ 4 * (li * lj)
key : 4 * lij ^ 2 = P.coxeterWeightIn S i j * (li * lj)
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
rwa [key, mul_le_mul_right (by positivity)] at cs

Result:
no goals

Proof state:
case intro.intro.intro.intro
ι : 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
inst✝⁶ : Finite ι
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
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := ((P.posRootForm S).posForm ri) ri
lj : S := ((P.posRootForm S).posForm rj) rj
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : sj > 0
hsi' : si = li
hsj' : sj = lj
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
rw [hsj'] at hsj

Result:
case intro.intro.intro.intro
ι : 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
inst✝⁶ : Finite ι
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
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := ((P.posRootForm S).posForm ri) ri
lj : S := ((P.posRootForm S).posForm rj) rj
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
⊢ P.coxeterWeightIn S i j ≤ 4

Proof state:
case intro.intro
ι : 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
inst✝⁶ : Finite ι
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
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := ((P.posRootForm S).posForm ri) ri
lj : S := ((P.posRootForm S).posForm rj) rj
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
x : ↥(span S (range ⇑P.root))
s : S
hs : s ≥ 0
hs' : (algebraMap S R) s = ((P.posRootForm S).form ↑x) ↑x
⊢ 0 ≤ ((P.posRootForm S).posForm x) x

Tactic:
rw [(P.posRootForm S).algebraMap_apply_eq_form_iff] at hs'

Result:
case intro.intro
ι : 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
inst✝⁶ : Finite ι
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
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := ((P.posRootForm S).posForm ri) ri
lj : S := ((P.posRootForm S).posForm rj) rj
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
x : ↥(span S (range ⇑P.root))
s : S
hs : s ≥ 0
hs' : s = ((P.posRootForm S).posForm x) x
⊢ 0 ≤ ((P.posRootForm S).posForm x) x