-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right [LieRing.IsNilpotent H]
    (hq : genWeightSpace M (q • α + χ) = ⊥)
    {x : L} (hx : x ∈ rootSpace H α)
    {y : M} (hy : y ∈ genWeightSpaceChain M α χ p q) :
    ⁅x, y⁆ ∈ genWeightSpaceChain M α χ p q

Proof state:
case a
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
this : genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q
⊢ ⁅x, z⁆ ∈ genWeightSpace M ((k + 1) • α + χ)

Tactic:
simpa only [zsmul_eq_mul, Int.cast_add, Pi.intCast_def, Int.cast_one] using
  (rootSpaceWeightSpaceProduct R L H M α (k • α + χ) ((k + 1) • α + χ)
      (by rw [add_smul]; abel) (⟨x, hx⟩ ⊗ₜ ⟨z, hz⟩)).property

Result:
no goals

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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
this : genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q
⊢ ⁅x, z⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
apply this

Result:
case a
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
this : genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q
⊢ ⁅x, z⁆ ∈ genWeightSpace M ((k + 1) • α + χ)

Proof state:
case hN.mk.inr
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
hk' : k + 1 ≠ q
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ)

Tactic:
replace hk' : k + 1 ∈ Ioo p q := ⟨by linarith [hk.1], lt_of_le_of_ne hk.2 hk'⟩

Result:
case hN.mk.inr
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
hk' : k + 1 ∈ Ioo p q
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ)

Proof state:
case hN.mk
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ)

Tactic:
rcases eq_or_ne (k + 1) q with rfl | hk'

Result:
case hN.mk.inl
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
p : ℤ
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hq : genWeightSpace M ((k + 1) • α + χ) = ⊥
hk : k ∈ Ioo p (k + 1)
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k_1 ∈ Ioo p (k + 1), genWeightSpace M (k_1 • α + χ)

case hN.mk.inr
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
hk' : k + 1 ≠ q
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ)

Proof state:
case hadd
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hy✝ : y✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hz₁ : ⁅x, x✝⁆ ∈ genWeightSpaceChain M α χ p q
hz₂ : ⁅x, y✝⁆ ∈ genWeightSpaceChain M α χ p q
⊢ ⁅x, x✝ + y✝⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
rw [lie_add]

Result:
case hadd
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hy✝ : y✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hz₁ : ⁅x, x✝⁆ ∈ genWeightSpaceChain M α χ p q
hz₂ : ⁅x, y✝⁆ ∈ genWeightSpaceChain M α χ p q
⊢ ⁅x, x✝⁆ + ⁅x, y✝⁆ ∈ genWeightSpaceChain M α χ p q

Proof state:
case hadd
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hy✝ : y✝ ∈ ⨆ i, genWeightSpace M (↑i • α + χ)
hz₁ : ⁅x, x✝⁆ ∈ genWeightSpaceChain M α χ p q
hz₂ : ⁅x, y✝⁆ ∈ genWeightSpaceChain M α χ p q
⊢ ⁅x, x✝⁆ + ⁅x, y✝⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
exact add_mem hz₁ hz₂

Result:
no goals

Proof state:
case hN.mk.inr
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
hk' : k + 1 ∈ Ioo p q
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ)

Tactic:
exact le_biSup (fun k ↦ genWeightSpace M (k • α + χ)) hk'

Result:
no goals