awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 ≤ chainTopCoeff α β
hα : ¬α = 0
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
have neg : ∀ (hn : n < (chainTopCoeff α β).succ) (hα : ¬α = 0),
  Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
Tactic: classical
  rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, chainTopCoeff_add_one _ _ hα] at hn
  exact Nat.find_min (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists hn
Cleared hypotheses: hn, hα
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 ≤ chainTopCoeff α β
hα : ¬α = 0
neg :
  ∀ (hn : n < (chainTopCoeff α β).succ) (hα : ¬α = 0),
    Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
neg₁ :
  ∀ (hn : n < chainTopCoeff α β + 1) (hα : ¬α = 0),
    Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
have neg₂ : ∀ (hα : ¬α = 0)
  (hn :
    n < Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) sorry),
  Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
Tactic: classical
  rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, chainTopCoeff_add_one _ _ hα] at hn
  exact Nat.find_min (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists hn
Cleared hypotheses: hn, hα
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 α β) : ℤ) ≤ n
hn' : n ≤ (↑(chainTopCoeff α β) : ℤ)
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
have ofNat : ∀ (n : ℕ) (hn : -(↑(chainBotCoeff α β) : ℤ) ≤ Int.ofNat n) (hn' : Int.ofNat n ≤ (↑(chainTopCoeff α β) : ℤ)),
  Ne (α := LieSubmodule R L M) (genWeightSpace M (Int.ofNat n • α + (⇑β : (a : L) → R))) ⊥
Tactic: rcases n with (n | n)
Cleared hypotheses: n, hn, hn'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 α β) : ℤ) ≤ n
hn' : n ≤ (↑(chainTopCoeff α β) : ℤ)
ofNat :
  ∀ (n : ℕ) (hn : -(↑(chainBotCoeff α β) : ℤ) ≤ Int.ofNat n) (hn' : Int.ofNat n ≤ (↑(chainTopCoeff α β) : ℤ)),
    Ne (α := LieSubmodule R L M) (genWeightSpace M (Int.ofNat n • α + (⇑β : (a : L) → R))) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
have negSucc : ∀ (n : ℕ) (hn : -(↑(chainBotCoeff α β) : ℤ) ≤ Int.negSucc n) (hn' : Int.negSucc n ≤ (↑(chainTopCoeff α β) : ℤ)),
  Ne (α := LieSubmodule R L M) (genWeightSpace M (Int.negSucc n • α + (⇑β : (a : L) → R))) ⊥
Tactic: rcases n with (n | n)
Cleared hypotheses: n, hn, hn'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 α β) : ℤ)
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (Int.ofNat n • α + (⇑β : (a : L) → R))) ⊥
have ofNat : ∀ (hn' : n ≤ chainTopCoeff α β), Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
Tactic: simp only [Int.ofNat_eq_natCast, Nat.cast_le, Nat.cast_smul_eq_nsmul] at hn' ⊢
Cleared hypotheses: hn'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 α β) : ℤ)
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (Int.negSucc n • α + (⇑β : (a : L) → R))) ⊥
have negSucc : ∀ (hn : n.succ ≤ chainBotCoeff α β),
  Ne (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (-(↑n.succ : ℤ)) α + (⇑β : (a : L) → R))) ⊥
Tactic: simp only [Int.negSucc_eq, ← Nat.cast_succ, neg_le_neg_iff, Nat.cast_le] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 (HSMul.hSMul (α := ℤ) (-(↑n.succ : ℤ)) α + (⇑β : (a : L) → R))) ⊥
have negSucc : Ne (α := LieSubmodule R L M) (genWeightSpace M (n.succ • -α + (⇑β : (a : L) → R))) ⊥
Tactic: rw [neg_smul, ← smul_neg, Nat.cast_smul_eq_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 α β
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) α + (⇑β : (a : L) → R))) ⊥
have hn₁ : LE.le (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) (-(↑n : ℤ))
Tactic: apply genWeightSpace_zsmul_add_ne_bot α β
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 : ℤ))
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) α + (⇑β : (a : L) → R))) ⊥
have hn' : LE.le (α := ℤ) (-(↑n : ℤ)) (↑(chainTopCoeff α β) : ℤ)
Tactic: apply genWeightSpace_zsmul_add_ne_bot α β
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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) = HSMul.hSMul (α := ℤ) (↑(chainTopCoeff α β) : ℤ) α + (⇑β : (a : L) → R)
have rw : (⇑(chainTop α β) : (a : L) → R) = chainTopCoeff α β • α + (⇑β : (a : L) → R)
Tactic: rw [Nat.cast_smul_eq_nsmul ℤ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 (-α) β = chainBot α β
have h : ∀ (x : L), Eq.{u_1 + 1} (α := R) ((chainTop (-α) β : (a : L) → R) x : R) ((chainBot α β : (a : L) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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 (-α) β = chainTop α β
have h : ∀ (x : L), Eq.{u_1 + 1} (α := R) ((chainBot (-α) β : (a : L) → R) x : R) ((chainTop α β : (a : L) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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
⊢ chainTop 0 β = β
have h : ∀ (x : L), Eq.{u_1 + 1} (α := R) ((chainTop 0 β : (a : L) → R) x : R) ((β : (a : L) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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
⊢ chainBot 0 β = β
have h : ∀ (x : L), Eq.{u_1 + 1} (α := R) ((chainBot 0 β : (a : L) → R) x : R) ((β : (a : L) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (α + (⇑(chainTop α β) : (a : L) → R))) ⊥
have rw : Eq (α := LieSubmodule R L M) (genWeightSpace M (α + (chainTopCoeff α β • α + (⇑β : (a : L) → R)))) ⊥
Tactic: rw [coe_chainTop', ← add_assoc, ← succ_nsmul',
    genWeightSpace_chainTopCoeff_add_one_nsmul_add _ _ hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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)))) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (α + (⇑(chainTop α β) : (a : L) → R))) ⊥
have rw₁ : Eq (α := LieSubmodule R L M) (genWeightSpace M (α + chainTopCoeff α β • α + (⇑β : (a : L) → R))) ⊥
Tactic: rw [coe_chainTop', ← add_assoc, ← succ_nsmul',
    genWeightSpace_chainTopCoeff_add_one_nsmul_add _ _ hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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))) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (α + (⇑(chainTop α β) : (a : L) → R))) ⊥
have rw₂ : Eq (α := LieSubmodule R L M) (genWeightSpace M ((chainTopCoeff α β + 1) • α + (⇑β : (a : L) → R))) ⊥
Tactic: rw [coe_chainTop', ← add_assoc, ← succ_nsmul',
    genWeightSpace_chainTopCoeff_add_one_nsmul_add _ _ hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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))) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (α + (⇑(chainTop α β) : (a : L) → R))) ⊥
have rw₃ : Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊥
Tactic: rw [coe_chainTop', ← add_assoc, ← succ_nsmul',
    genWeightSpace_chainTopCoeff_add_one_nsmul_add _ _ hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (-α + (⇑(chainBot α β) : (a : L) → R))) ⊥
have rw : Eq (α := LieSubmodule R L M) (genWeightSpace M (-α + (⇑(chainTop (-α) β) : (a : L) → R))) ⊥
Tactic: rw [← chainTop_neg, genWeightSpace_add_chainTop _ _ (by simpa using hα)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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))) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (-α + (⇑(chainBot α β) : (a : L) → R))) ⊥
have rw₁ : Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊥
Tactic: rw [← chainTop_neg, genWeightSpace_add_chainTop _ _ (by simpa using hα)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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
⊢ False
have apply : Eq (α := LieSubmodule R L M) (genWeightSpace M α) ⊥
Tactic: apply hα'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M α) ⊥
have rw : Eq (α := LieSubmodule R L M) (genWeightSpace M (α + 0)) ⊥
Tactic: rw [← add_zero (α : L → R), ← e, genWeightSpace_add_chainTop _ _ hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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)) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M α) ⊥
have rw₁ : Eq (α := LieSubmodule R L M) (genWeightSpace M (α + (⇑(chainTop α β) : (a : L) → R))) ⊥
Tactic: rw [← add_zero (α : L → R), ← e, genWeightSpace_add_chainTop _ _ hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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))) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M α) ⊥
have rw₂ : Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊥
Tactic: rw [← add_zero (α : L → R), ← e, genWeightSpace_add_chainTop _ _ hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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)
have 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)
Tactic: refine Module.End.isNilpotent_iff_of_finite.mpr fun m ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (hypothesis)
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)
          m :
        M)
      (0 : M)
have hm : 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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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
χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M
m₂ : M
hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) 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)
have mem : ∀ (n : ℕ) (hn : Eq (α := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K))) ⊥),
  ∃ (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)
Tactic: obtain ⟨n, -, hn⟩ := exists_genWeightSpace_smul_add_eq_bot M χ χ₂ hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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
χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M
m₂ : M
hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂
n : ℕ
hn : Eq (α := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (n • χ + (⇑χ₂ : (a : ↥H) → K))) ⊥
⊢ ∃ (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)
have h : 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)
Tactic: use n