-- Mathlib/Algebra/Lie/Weights/Chain.lean
/-- Given a (potential) root `α` relative to a Cartan subalgebra `H`, if we restrict to the ideal
`I = corootSpace α` of `H` (informally, `I = ⁅H(α), H(-α)⁆`), we may find an
integral linear combination between `α` and any weight `χ` of a representation.

This is Proposition 4.4 from [carter2005] and is a key step in the proof that the roots of a
semisimple Lie algebra form a root system. It shows that the restriction of `α` to `I` vanishes iff
the restriction of every root to `I` vanishes (which cannot happen in a semisimple Lie algebra). -/
lemma exists_forall_mem_corootSpace_smul_add_eq_zero
    [IsDomain R] [IsPrincipalIdealRing R] [CharZero R] [NoZeroSMulDivisors R M] [IsNoetherian R M]
    (hα : α ≠ 0) (hχ : genWeightSpace M χ ≠ ⊥) :
    ∃ a b : ℤ, 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k => ↑(genWeightSpace M (k • α + χ))
⊢ iSupIndep fun i => genWeightSpace M (↑i • α + χ)

Tactic:
refine (iSupIndep_genWeightSpace R H M).comp fun i j hij ↦ ?_

Result:
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k => ↑(genWeightSpace M (k • α + χ))
i j : { x // x ∈ Finset.Ioo p q }
hij : ↑i • α + χ = ↑j • α + χ
⊢ i = j

Proof state:
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k => ↑(genWeightSpace M (k • α + χ))
i j : { x // x ∈ Finset.Ioo p q }
hij : ↑i • α + χ = ↑j • α + χ
⊢ (fun c => c • α) ↑i = (fun c => c • α) ↑j

Tactic:
rwa [add_left_inj] at hij

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k => ↑(genWeightSpace M (k • α + χ))
⊢ (a • α + ↑b • χ) x = 0

Tactic:
have h₁ : iSupIndep fun (i : Finset.Ioo p q) ↦ N i := by
  rw [← LieSubmodule.iSupIndep_iff_toSubmodule]
  refine (iSupIndep_genWeightSpace R H M).comp fun i j hij ↦ ?_
  exact SetCoe.ext <| smul_left_injective ℤ hα <| by rwa [add_left_inj] at hij

Result:
case intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k => ↑(genWeightSpace M (k • α + χ))
h₁ : iSupIndep fun i => N ↑i
⊢ (a • α + ↑b • χ) x = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k => ↑(genWeightSpace M (k • α + χ))
⊢ iSupIndep fun i => N ↑i

Tactic:
rw [← LieSubmodule.iSupIndep_iff_toSubmodule]

Result:
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k => ↑(genWeightSpace M (k • α + χ))
⊢ iSupIndep fun i => genWeightSpace M (↑i • α + χ)