-- 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:
ι : 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
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
set lj := (P.posRootForm S).posForm rj rj

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
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
⊢ P.coxeterWeightIn S i j ≤ 4

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
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
hsj' : (algebraMap S R) sj = ((P.posRootForm S).form (P.root j)) (P.root j)
hsi' : si = li
⊢ (algebraMap S R) sj = (algebraMap S R) lj

Tactic:
simpa [lj] using hsj'

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
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
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
set lij := (P.posRootForm S).posForm ri rj

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
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
⊢ 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 : si > 0
hsi' : (algebraMap S R) si = ((P.posRootForm S).form (P.root i)) (P.root i)
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
obtain ⟨sj, hsj, hsj'⟩ := (P.posRootForm S).exists_pos_eq j

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 : si > 0
hsi' : (algebraMap S R) si = ((P.posRootForm S).form (P.root i)) (P.root i)
sj : S
hsj : sj > 0
hsj' : (algebraMap S R) sj = ((P.posRootForm S).form (P.root j)) (P.root j)
⊢ P.coxeterWeightIn S i j ≤ 4

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
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 : ι
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
have : Fintype ι := Fintype.ofFinite ι

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
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 ι
⊢ P.coxeterWeightIn S i j ≤ 4