awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : -(↑(chainBotCoeff α β) : ℤ) ≤ Int.ofNat n
hn' : Int.ofNat n ≤ (↑(chainTopCoeff α β) : ℤ)
ofNat : ∀ (hn' : n ≤ chainTopCoeff α β), Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (Int.ofNat n • α + (⇑β : (a : L) → R))) ⊥

Tactic:
simp only [Int.ofNat_eq_natCast, Nat.cast_le, Nat.cast_smul_eq_nsmul] at hn' ⊢

Premises used: Int.ofNat_eq_natCast, Nat.cast_smul_eq_nsmul, Nat.cast_le
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : -(↑(chainBotCoeff α β) : ℤ) ≤ Int.ofNat n
hn' : n ≤ chainTopCoeff α β
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥

Tactic:
genWeightSpace_nsmul_add_ne_bot_of_le α β hn'

Premises used: LieModule.genWeightSpace_nsmul_add_ne_bot_of_le
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : -(↑(chainBotCoeff α β) : ℤ) ≤ Int.ofNat n
hn' : n ≤ chainTopCoeff α β
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥

Tactic:
exact genWeightSpace_nsmul_add_ne_bot_of_le α β hn'

Premises used: LieModule.genWeightSpace_nsmul_add_ne_bot_of_le
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : -(↑(chainBotCoeff α β) : ℤ) ≤ Int.negSucc n
hn' : Int.negSucc n ≤ (↑(chainTopCoeff α β) : ℤ)
negSucc :
  ∀ (hn : n.succ ≤ chainBotCoeff α β),
    Ne (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (-(↑n.succ : ℤ)) α + (⇑β : (a : L) → R))) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (Int.negSucc n • α + (⇑β : (a : L) → R))) ⊥

Tactic:
simp only [Int.negSucc_eq, ← Nat.cast_succ, neg_le_neg_iff, Nat.cast_le] at hn ⊢

Premises used: Nat.cast_succ, Int.negSucc_eq, Nat.cast_le, neg_le_neg_iff
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn' : Int.negSucc n ≤ (↑(chainTopCoeff α β) : ℤ)
hn : n.succ ≤ chainBotCoeff α β
negSucc : Ne (α := LieSubmodule R L M) (genWeightSpace M (n.succ • -α + (⇑β : (a : L) → R))) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (-(↑n.succ : ℤ)) α + (⇑β : (a : L) → R))) ⊥

Tactic:
rw [neg_smul, ← smul_neg, Nat.cast_smul_eq_nsmul]

Premises used: neg_smul, smul_neg, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn' : Int.negSucc n ≤ (↑(chainTopCoeff α β) : ℤ)
hn : n.succ ≤ chainBotCoeff α β
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n.succ • -α + (⇑β : (a : L) → R))) ⊥

Tactic:
genWeightSpace_nsmul_add_ne_bot_of_le (-α) β hn

Premises used: LieModule.genWeightSpace_nsmul_add_ne_bot_of_le, Neg.neg
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn' : Int.negSucc n ≤ (↑(chainTopCoeff α β) : ℤ)
hn : n.succ ≤ chainBotCoeff α β
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n.succ • -α + (⇑β : (a : L) → R))) ⊥

Tactic:
exact genWeightSpace_nsmul_add_ne_bot_of_le (-α) β hn

Premises used: LieModule.genWeightSpace_nsmul_add_ne_bot_of_le, Neg.neg
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : n ≤ chainBotCoeff α β
hn₁ : LE.le (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) (-(↑n : ℤ))
hn' : LE.le (α := ℤ) (-(↑n : ℤ)) (↑(chainTopCoeff α β) : ℤ)
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) α + (⇑β : (a : L) → R))) ⊥

Tactic:
apply genWeightSpace_zsmul_add_ne_bot α β

Premises used: LieModule.genWeightSpace_zsmul_add_ne_bot
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : n ≤ chainBotCoeff α β
⊢ LE.le (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) (-(↑n : ℤ))

Tactic:
lia
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : n ≤ chainBotCoeff α β
⊢ LE.le (α := ℤ) (-(↑n : ℤ)) (↑(chainTopCoeff α β) : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ (⇑(chainTop α β) : (a : L) → R) = chainTopCoeff α β • α + (⇑β : (a : L) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
rw : (⇑(chainTop α β) : (a : L) → R) = chainTopCoeff α β • α + (⇑β : (a : L) → R)
⊢ (⇑(chainTop α β) : (a : L) → R) = HSMul.hSMul (α := ℤ) (↑(chainTopCoeff α β) : ℤ) α + (⇑β : (a : L) → R)

Tactic:
rw [Nat.cast_smul_eq_nsmul ℤ]

Premises used: Int, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ (⇑(chainTop α β) : (a : L) → R) = chainTopCoeff α β • α + (⇑β : (a : L) → R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ (⇑(chainBot α β) : (a : L) → R) = HSMul.hSMul (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) α + (⇑β : (a : L) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
h : ∀ (x : L), Eq.{u_1 + 1} (α := R) ((chainTop (-α) β : (a : L) → R) x : R) ((chainBot α β : (a : L) → R) x : R)
⊢ chainTop (-α) β = chainBot α β

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
x : L
⊢ Eq.{u_1 + 1} (α := R) ((chainTop (-α) β : (a : L) → R) x : R) ((chainBot α β : (a : L) → R) x : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
h : ∀ (x : L), Eq.{u_1 + 1} (α := R) ((chainBot (-α) β : (a : L) → R) x : R) ((chainTop α β : (a : L) → R) x : R)
⊢ chainBot (-α) β = chainTop α β

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
x : L
⊢ Eq.{u_1 + 1} (α := R) ((chainBot (-α) β : (a : L) → R) x : R) ((chainTop α β : (a : L) → R) x : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
β : Weight R L M
h : ∀ (x : L), Eq.{u_1 + 1} (α := R) ((chainTop 0 β : (a : L) → R) x : R) ((β : (a : L) → R) x : R)
⊢ chainTop 0 β = β

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
β : Weight R L M
x : L
⊢ Eq.{u_1 + 1} (α := R) ((chainTop 0 β : (a : L) → R) x : R) ((β : (a : L) → R) x : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
β : Weight R L M
h : ∀ (x : L), Eq.{u_1 + 1} (α := R) ((chainBot 0 β : (a : L) → R) x : R) ((β : (a : L) → R) x : R)
⊢ chainBot 0 β = β

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
β : Weight R L M
x : L
⊢ Eq.{u_1 + 1} (α := R) ((chainBot 0 β : (a : L) → R) x : R) ((β : (a : L) → R) x : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
rw : Eq (α := LieSubmodule R L M) (genWeightSpace M (α + (chainTopCoeff α β • α + (⇑β : (a : L) → R)))) ⊥
rw₁ : Eq (α := LieSubmodule R L M) (genWeightSpace M (α + chainTopCoeff α β • α + (⇑β : (a : L) → R))) ⊥
rw₂ : Eq (α := LieSubmodule R L M) (genWeightSpace M ((chainTopCoeff α β + 1) • α + (⇑β : (a : L) → R))) ⊥
rw₃ rw₄ : Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (α + (⇑(chainTop α β) : (a : L) → R))) ⊥

Tactic:
rw [coe_chainTop', ← add_assoc, ← succ_nsmul',
    genWeightSpace_chainTopCoeff_add_one_nsmul_add _ _ hα]

Premises used: add_assoc, succ_nsmul', LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, LieModule.coe_chainTop'
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
rw : Eq (α := LieSubmodule R L M) (genWeightSpace M (-α + (⇑(chainTop (-α) β) : (a : L) → R))) ⊥
rw₁ rw₂ : Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (-α + (⇑(chainBot α β) : (a : L) → R))) ⊥

Tactic:
rw [← chainTop_neg, genWeightSpace_add_chainTop _ _ (by simpa using hα)]

Premises used: LieModule.chainTop_neg, LieModule.genWeightSpace_add_chainTop
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : Ne (α := LieSubmodule R L M) (genWeightSpace M α) ⊥
by_contra : ∀ (e : (chainTop α β).IsZero), False
⊢ (chainTop α β).IsNonZero

Tactic:
by_contra e
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : Ne (α := LieSubmodule R L M) (genWeightSpace M α) ⊥
e : (chainTop α β).IsZero
apply : Eq (α := LieSubmodule R L M) (genWeightSpace M α) ⊥
⊢ False

Tactic:
apply hα'
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : Ne (α := LieSubmodule R L M) (genWeightSpace M α) ⊥
e : (chainTop α β).IsZero
rw : Eq (α := LieSubmodule R L M) (genWeightSpace M (α + 0)) ⊥
rw₁ : Eq (α := LieSubmodule R L M) (genWeightSpace M (α + (⇑(chainTop α β) : (a : L) → R))) ⊥
rw₂ rw₃ : Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M α) ⊥

Tactic:
rw [← add_zero (α : L → R), ← e, genWeightSpace_add_chainTop _ _ hα]

Premises used: add_zero, LieModule.genWeightSpace_add_chainTop
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
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 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α β : Weight R L M
hα : α.IsNonZero
⊢ (chainTop (⇑α : (a : L) → R) β).IsNonZero

Tactic:
chainTop_isNonZero' α β hα α.2

Premises used: LieModule.chainTop_isNonZero', DFunLike.coe, LieModule.Weight.genWeightSpace_ne_bot'
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
⊢ _root_.IsNilpotent.{u_3} (R := End K M)
    (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)

Tactic:
Module.End.isNilpotent_iff_of_finite.mpr fun m ↦ ?_

Premises used: Iff.mpr, Module.End.isNilpotent_iff_of_finite
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
refine :
  ∀ (m : M),
    ∃ (n : ℕ),
      Eq (α := M)
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
              (a : M) → M)
            m :
          M)
        (0 : M)
⊢ _root_.IsNilpotent.{u_3} (R := End K M)
    (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M)

Tactic:
refine Module.End.isNilpotent_iff_of_finite.mpr fun m ↦ ?_

Premises used: Iff.mpr, Module.End.isNilpotent_iff_of_finite
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
⊢ Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (χ : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑χ : (a : ↥H) → K)) m

Tactic:
simp [iSup_genWeightSpace_eq_top' K H M]

Premises used: LieModule.iSup_genWeightSpace_eq_top', Membership.mem, Subtype
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
⊢ Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (χ : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑χ : (a : ↥H) → K)) m

Tactic:
have hm : m ∈ ⨆ χ : LieModule.Weight K H M, genWeightSpace M χ := by
    simp [iSup_genWeightSpace_eq_top' K H M]
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          0 :
        M)
      (0 : M)

Tactic:
⟨0, map_zero _⟩

Premises used: map_zero, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          0 :
        M)
      (0 : M)

Tactic:
exact ⟨0, map_zero _⟩