awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
rwa : ∀ (hχ : Nontrivial.{u_4} ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
rwa₁ : ∀ (hχ : 0 < Module.rank R ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
rwa₂ :
  ∀ (hχ : LT.lt.{u_4 + 1} (α := Cardinal.{u_4}) 0 (↑(finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) : Cardinal.{u_4})),
    0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (hχ : 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
⊢ 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)

Tactic:
rwa [← LieSubmodule.nontrivial_iff_ne_bot, ← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank,
    Nat.cast_pos] at hχ

Premises used: Nat.cast_pos, rank_pos_iff_nontrivial, Module.finrank_eq_rank, LieSubmodule.nontrivial_iff_ne_bot
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥

Tactic:
(LieSubmodule.nontrivial_iff_ne_bot _ _ _).mp h

Premises used: LieSubmodule.nontrivial_iff_ne_bot, Iff.mp
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)

Tactic:
nontriviality shiftedGenWeightSpace R L M χ

Premises used: LieModule.shiftedGenWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
simp : ⁅x, m⁆ + ⁅y, m⁆ - (χ x • m + χ y • m) = ⁅x, m⁆ - χ x • m + (⁅y, m⁆ - χ y • m)
⊢ ⁅x + y, m⁆ - χ (x + y) • m = ⁅x, m⁆ - χ x • m + (⁅y, m⁆ - χ y • m)

Tactic:
simp only [add_lie, LinearWeights.map_add χ (aux R L M χ), add_smul]

Premises used: _private.0.LieModule.shiftedGenWeightSpace.aux, LieModule.LinearWeights.map_add, add_smul, add_lie
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, m⁆ + ⁅y, m⁆ - (χ x • m + χ y • m) = ⁅x, m⁆ - χ x • m + (⁅y, m⁆ - χ y • m)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x : L
m n : ↥(shiftedGenWeightSpace R L M χ)
⊢ Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)

Tactic:
nontriviality shiftedGenWeightSpace R L M χ

Premises used: LieModule.shiftedGenWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x : L
m n : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
simp : ⁅x, m⁆ + ⁅x, n⁆ - (χ x • m + χ x • n) = ⁅x, m⁆ - χ x • m + (⁅x, n⁆ - χ x • n)
⊢ ⁅x, m + n⁆ - χ x • (m + n) = ⁅x, m⁆ - χ x • m + (⁅x, n⁆ - χ x • n)

Tactic:
simp only [lie_add, smul_add]

Premises used: smul_add, lie_add
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x : L
m n : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, m⁆ + ⁅x, n⁆ - (χ x • m + χ x • n) = ⁅x, m⁆ - χ x • m + (⁅x, n⁆ - χ x • n)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
simp :
  ⁅x, ⁅y, m⁆⁆ - χ y • ⁅x, m⁆ - (χ x • ⁅y, m⁆ - χ y • χ x • m) =
    ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ + (⁅y, ⁅x, m⁆⁆ - χ x • ⁅y, m⁆ - (χ y • ⁅x, m⁆ - χ y • χ x • m))
⊢ ⁅x, ⁅y, m⁆ - χ y • m⁆ - χ x • (⁅y, m⁆ - χ y • m) =
    ⁅⁅x, y⁆, m⁆ - χ ⁅x, y⁆ • m + (⁅y, ⁅x, m⁆ - χ x • m⁆ - χ y • (⁅x, m⁆ - χ x • m))

Tactic:
simp only [lie_sub, lie_smul, lie_lie, LinearWeights.map_lie χ (aux R L M χ), zero_smul,
      sub_zero, smul_sub, smul_comm (χ x)]

Premises used: sub_zero, lie_smul, _private.0.LieModule.shiftedGenWeightSpace.aux, smul_sub, zero_smul, LieModule.LinearWeights.map_lie, lie_sub, SMulCommClass.smul_comm, lie_lie
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, ⁅y, m⁆⁆ - χ y • ⁅x, m⁆ - (χ x • ⁅y, m⁆ - χ y • χ x • m) =
    ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ + (⁅y, ⁅x, m⁆⁆ - χ x • ⁅y, m⁆ - (χ y • ⁅x, m⁆ - χ y • χ x • m))

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ (↑⁅x, m⁆ : M) = ⁅x, (↑m : M)⁆ - χ x • (↑m : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)

Tactic:
nontriviality shiftedGenWeightSpace R L M χ

Premises used: LieModule.shiftedGenWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
a : (↑⁅t • x, m⁆ : M) = (↑(t • ⁅x, m⁆) : M)
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
a : ⁅t • x, (↑m : M)⁆ - χ (t • x) • (↑m : M) = (↑(t • ⁅x, m⁆) : M)
⊢ (↑⁅t • x, m⁆ : M) = (↑(t • ⁅x, m⁆) : M)

Tactic:
rw [coe_lie_shiftedGenWeightSpace_apply]

Premises used: LieModule.shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
a : t • ⁅x, (↑m : M)⁆ - t • χ x • (↑m : M) = t • (↑⁅x, m⁆ : M)
⊢ ⁅t • x, (↑m : M)⁆ - χ (t • x) • (↑m : M) = (↑(t • ⁅x, m⁆) : M)

Tactic:
simp only [smul_lie, LinearWeights.map_smul χ (aux R L M χ), smul_assoc t, SetLike.val_smul]

Premises used: smul_assoc, LieModule.LinearWeights.map_smul, _private.0.LieModule.shiftedGenWeightSpace.aux, smul_lie, SetLike.val_smul
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
a : t • (⁅x, (↑m : M)⁆ - χ x • (↑m : M)) = t • (↑⁅x, m⁆ : M)
⊢ t • ⁅x, (↑m : M)⁆ - t • χ x • (↑m : M) = t • (↑⁅x, m⁆ : M)

Tactic:
rw [← smul_sub]

Premises used: smul_sub
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ t • (⁅x, (↑m : M)⁆ - χ x • (↑m : M)) = t • (↑⁅x, m⁆ : M)

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
a : (↑⁅x, t • m⁆ : M) = (↑(t • ⁅x, m⁆) : M)
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
a : ⁅x, (↑(t • m) : M)⁆ - χ x • (↑(t • m) : M) = (↑(t • ⁅x, m⁆) : M)
⊢ (↑⁅x, t • m⁆ : M) = (↑(t • ⁅x, m⁆) : M)

Tactic:
rw [coe_lie_shiftedGenWeightSpace_apply]

Premises used: LieModule.shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
a : t • ⁅x, (↑m : M)⁆ - χ x • t • (↑m : M) = t • (↑⁅x, m⁆ : M)
⊢ ⁅x, (↑(t • m) : M)⁆ - χ x • (↑(t • m) : M) = (↑(t • ⁅x, m⁆) : M)

Tactic:
simp only [SetLike.val_smul, lie_smul]

Premises used: lie_smul, SetLike.val_smul
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
a : t • (⁅x, (↑m : M)⁆ - χ x • (↑m : M)) = t • (↑⁅x, m⁆ : M)
⊢ t • ⁅x, (↑m : M)⁆ - χ x • t • (↑m : M) = t • (↑⁅x, m⁆ : M)

Tactic:
rw [smul_comm (χ x), ← smul_sub]

Premises used: smul_sub, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
x : L
⊢ Eq.{u_4 + 1} (α := Module.End R ↥(shiftedGenWeightSpace R L M χ))
    (((toEnd.{u_2, u_3, u_4} R L ↥(shiftedGenWeightSpace R L M χ) :
            LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(shiftedGenWeightSpace R L M χ))) :
          (a : L) → Module.End R ↥(shiftedGenWeightSpace R L M χ))
        x :
      Module.End R ↥(shiftedGenWeightSpace R L M χ))
    ((LinearEquiv.conj (shift R L M χ) :
          (a : Module.End R ↥(genWeightSpace M χ)) → Module.End R ↥(shiftedGenWeightSpace R L M χ))
        (HSub.hSub (α := Module.End R ↥(genWeightSpace M χ))
          (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                  LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
                (a : L) → Module.End R ↥(genWeightSpace M χ))
              x :
            Module.End R ↥(genWeightSpace M χ))
          (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id)) :
      Module.End R ↥(shiftedGenWeightSpace R L M χ))

Tactic:
tauto
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
⊢ IsNilpotent.{u_3, u_4} L ↥(shiftedGenWeightSpace R L M χ)

Tactic:
LieModule.isNilpotent_iff_forall'.mpr fun x ↦ isNilpotent_toEnd_sub_algebraMap M χ x

Premises used: Iff.mpr, LieModule.isNilpotent_toEnd_sub_algebraMap, LieModule.isNilpotent_iff_forall'
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
⊢ Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))

Tactic:
replace hχ : Nontrivial (shiftedGenWeightSpace R L M χ) :=
    (LieSubmodule.nontrivial_iff_ne_bot R L M).mpr χ.genWeightSpace_ne_bot
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
obtain :
  ∀ (m : M) (property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m)
    (hm₁ :
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property))
    (hm₂ :
      Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
          Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
            (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
          hm₁ ≠
        0),
    ∃ (m : M), m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
⊢ ∃ (m : M), m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m

Tactic:
obtain ⟨⟨⟨m, _⟩, hm₁⟩, hm₂⟩ :=
    @exists_ne _ (nontrivial_max_triv_of_isNilpotent R L (shiftedGenWeightSpace R L M χ)) 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁ :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁ ≠
    0
⊢ ∀ (x : L),
    (↑⁅x,
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
        M) =
      0

Tactic:
simp_rw [mem_maxTrivSubmodule, Subtype.ext_iff,
    ZeroMemClass.coe_zero] at hm₁

Premises used: LieModule.mem_maxTrivSubmodule, Subtype.ext_iff, ZeroMemClass.coe_zero
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁_1 :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁_1 ≠
    0
hm₁ :
  ∀ (x : L),
    (↑⁅x,
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
        M) =
      0
⊢ m ≠ 0

Tactic:
simpa [LieSubmodule.mk_eq_zero] using hm₂

Premises used: LieSubmodule.mk_eq_zero
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁_1 :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁_1 ≠
    0
hm₁ :
  ∀ (x : L),
    (↑⁅x,
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
        M) =
      0
refine : ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
⊢ ∃ (m : M), m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m

Tactic:
refine ⟨m, by simpa [LieSubmodule.mk_eq_zero] using hm₂, ?_⟩