-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left [LieRing.IsNilpotent H]
    (hp : genWeightSpace M (p • α + χ) = ⊥)
    {x : L} (hx : x ∈ rootSpace H (-α))
    {y : M} (hy : y ∈ genWeightSpaceChain M α χ p q) :
    ⁅x, y⁆ ∈ 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
hp : genWeightSpace M (p • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : y ∈ genWeightSpaceChain M α χ p q
⊢ genWeightSpace M (-p • -α + χ) = ⊥

Tactic:
rwa [smul_neg, neg_smul, neg_neg]

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
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : y ∈ genWeightSpaceChain M (-α) χ (-q) (-p)
hp : genWeightSpace M (-p • -α + χ) = ⊥
⊢ ⁅x, y⁆ ∈ genWeightSpaceChain M (-α) χ (-q) (-p)

Tactic:
exact lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right M (-α) χ (-q) (-p) hp hx hy

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
hp : genWeightSpace M (p • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : y ∈ genWeightSpaceChain M α χ p q
⊢ ⁅x, y⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
replace hp : genWeightSpace M ((-p) • (-α) + χ) = ⊥ := by rwa [smul_neg, neg_smul, neg_neg]

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
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : y ∈ genWeightSpaceChain M α χ p q
hp : genWeightSpace M (-p • -α + χ) = ⊥
⊢ ⁅x, y⁆ ∈ 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
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : y ∈ genWeightSpaceChain M α χ p q
hp : genWeightSpace M (-p • -α + χ) = ⊥
⊢ ⁅x, y⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
rw [← genWeightSpaceChain_neg] 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
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : y ∈ genWeightSpaceChain M (-α) χ (-q) (-p)
hp : genWeightSpace M (-p • -α + χ) = ⊥
⊢ ⁅x, y⁆ ∈ genWeightSpaceChain M (-α) χ (-q) (-p)