-- 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 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⟩ • α + χ)
⊢ ⁅x, z⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
suffices genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q by
  apply this
  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:
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) • α + χ) ≤ genWeightSpaceChain M α χ p q

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) • α + χ) ≤ genWeightSpaceChain M α χ p q

Tactic:
rw [genWeightSpaceChain]

Result:
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 • α + χ)

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
⊢ α + (k • α + χ) = (k + 1) • α + χ

Tactic:
rw [add_smul]

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
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
⊢ α + (k • α + χ) = k • α + 1 • α + χ

Proof state:
case h0
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 : M
⊢ ⁅x, 0⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
simp

Result:
no goals

Proof state:
case hN
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 : M
k : Subtype (Membership.mem (Ioo p q))
z : M
hz : z ∈ genWeightSpace M (↑k • α + χ)
⊢ ⁅x, z⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
obtain ⟨k, hk⟩ := k

Result:
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⟩ • α + χ)
⊢ ⁅x, z⁆ ∈ genWeightSpaceChain M α χ p q

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
⊢ α + (k • α + χ) = k • α + 1 • α + χ

Tactic:
abel

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⟩ • α + χ)
hk' : k + 1 ≠ q
⊢ p < k + 1

Tactic:
linarith [hk.1]

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 : M
hy : y ∈ genWeightSpaceChain M α χ p q
⊢ ⁅x, y⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
rw [genWeightSpaceChain, iSup_subtype'] at hy

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