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
hα : α ≠ 0
a : Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ ≠ 0
⊢ 0 < Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯

Tactic:
rw [zero_lt_iff]

Premises used: zero_lt_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
hα : α ≠ 0
e : Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ = 0
rw :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M
      (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ •
          α +
        (⇑β : (a : L) → R)))
    ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 α + (⇑β : (a : L) → R))) ⊥

Tactic:
rw [← 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
e : Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ = 0
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M
      (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ •
          α +
        (⇑β : (a : L) → R)))
    ⊥

Tactic:
Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists

Premises used: Filter.Eventually.exists, LieModule.eventually_genWeightSpace_smul_add_eq_bot, DFunLike.coe, Nat.find_spec
-- 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
e : Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ = 0
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M
      (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ •
          α +
        (⇑β : (a : L) → R)))
    ⊥

Tactic:
exact Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists

Premises used: Filter.Eventually.exists, LieModule.eventually_genWeightSpace_smul_add_eq_bot, DFunLike.coe, Nat.find_spec
-- 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
e : Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ = 0
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 α + (⇑β : (a : L) → R))) ⊥

Tactic:
have : genWeightSpace M (0 • α + β : L → R) = ⊥ := by
    rw [← e]
    exact Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists
-- 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
e : Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ = 0
this : Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 α + (⇑β : (a : L) → R))) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (⇑β : (a : L) → R)) ⊥

Tactic:
simpa only [zero_smul, zero_add] using this

Premises used: zero_add, zero_smul
-- 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
e : Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ = 0
this : Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 α + (⇑β : (a : L) → R))) ⊥
⊢ False

Tactic:
exact β.genWeightSpace_ne_bot _ (by simpa only [zero_smul, zero_add] using this)

Premises used: LieModule.Weight.genWeightSpace_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
hα : α ≠ 0
rw :
  HAdd.hAdd (α := ℕ)
      (if hα : α = 0 then 0
      else
        (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥)
            ⋯).pred)
      1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
rw₁ rw₂ rw₃ :
  (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥)
          ⋯).pred +
      1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
a : 0 < Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
a₁ : Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ ≠ 0
a₂ :
  ∀
    (e :
      Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ =
        0),
    False
a₃ :
  ∀
    (e :
      Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ =
        0)
    (this : Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 α + (⇑β : (a : L) → R))) ⊥), False
⊢ chainTopCoeff α β + 1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯

Tactic:
classical
  rw [chainTopCoeff, dif_neg hα]
  apply Nat.succ_pred_eq_of_pos
  rw [zero_lt_iff]
  intro e
  have : genWeightSpace M (0 • α + β : L → R) = ⊥ := by
    rw [← e]
    exact Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists
  exact β.genWeightSpace_ne_bot _ (by simpa only [zero_smul, zero_add] using this)

Premises used: Nat.succ_pred_eq_of_pos, dif_neg, zero_lt_iff, LieModule.Weight.genWeightSpace_ne_bot, LieModule.chainTopCoeff
-- 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
      (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ •
          α +
        (⇑β : (a : L) → R)))
    ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M ((chainTopCoeff α β + 1) • α + (⇑β : (a : L) → R))) ⊥

Tactic:
rw [chainTopCoeff_add_one _ _ hα]

Premises used: LieModule.chainTopCoeff_add_one
-- 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
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M
      (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ •
          α +
        (⇑β : (a : L) → R)))
    ⊥

Tactic:
Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists

Premises used: Filter.Eventually.exists, LieModule.eventually_genWeightSpace_smul_add_eq_bot, DFunLike.coe, Nat.find_spec
-- 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
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M
      (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ •
          α +
        (⇑β : (a : L) → R)))
    ⊥

Tactic:
exact Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists

Premises used: Filter.Eventually.exists, LieModule.eventually_genWeightSpace_smul_add_eq_bot, DFunLike.coe, Nat.find_spec
-- 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 rw₁ rw₂ :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M
      (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯ •
          α +
        (⇑β : (a : L) → R)))
    ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M ((chainTopCoeff α β + 1) • α + (⇑β : (a : L) → R))) ⊥

Tactic:
classical
  rw [chainTopCoeff_add_one _ _ hα]
  exact Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists

Premises used: LieModule.chainTopCoeff_add_one
-- 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 (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
    (genWeightSpace M ((chainTopCoeff α β + 1) • α + (⇑β : (a : L) → R)))
rw₁ :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
    (genWeightSpace M (HSMul.hSMul (α := ℤ) (↑(chainTopCoeff α β + 1) : ℤ) α + (⇑β : (a : L) → R)))
rw₂ :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) (↑1 : ℤ) • α + (⇑β : (a : L) → R)))
rw₃ rw₄ :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R))) ⊥

Tactic:
rw [← genWeightSpace_chainTopCoeff_add_one_nsmul_add α β hα, ← Nat.cast_smul_eq_nsmul ℤ,
    Nat.cast_add, Nat.cast_one]

Premises used: Int, Nat.cast_add, Nat.cast_smul_eq_nsmul, LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, Nat.cast_one
-- 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
⊢ -α ≠ 0

Tactic:
simpa using 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
rw :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) (-1) • α + (⇑β : (a : L) → R))) ⊥
rw₁ :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M (-HAdd.hAdd (α := ℤ) (↑(chainBotCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R))) ⊥
rw₂ :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M (-(HAdd.hAdd (α := ℤ) (↑(chainBotCoeff α β) : ℤ) 1 • α) + (⇑β : (a : L) → R))) ⊥
rw₃ :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainBotCoeff α β) : ℤ) 1 • -α + (⇑β : (a : L) → R))) ⊥
rw₄ :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (-α) β) : ℤ) 1 • -α + (⇑β : (a : L) → R))) ⊥
rw₅ rw₆ : Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊥
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HSub.hSub (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) 1 • α + (⇑β : (a : L) → R))) ⊥

Tactic:
rw [sub_eq_add_neg, ← neg_add, neg_smul, ← smul_neg, chainBotCoeff,
    genWeightSpace_chainTopCoeff_add_one_zsmul_add _ _ (by simpa using hα)]

Premises used: neg_smul, sub_eq_add_neg, neg_add, smul_neg, LieModule.chainBotCoeff, LieModule.genWeightSpace_chainTopCoeff_add_one_zsmul_add
-- 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 ≤ chainTopCoeff α β
pos : ∀ (hα : α = 0), Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
neg : ∀ (hα : ¬α = 0), Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥

Tactic:
by_cases hα : α = 0
-- 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 ≤ chainTopCoeff α β
hα : α = 0
pos : Ne (α := LieSubmodule R L M) (genWeightSpace M (⇑β : (a : L) → R)) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥

Tactic:
rw [hα, smul_zero, zero_add]

Premises used: smul_zero, zero_add
-- 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 ≤ chainTopCoeff α β
hα : α = 0
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (⇑β : (a : L) → R)) ⊥

Tactic:
β.genWeightSpace_ne_bot

Premises used: LieModule.Weight.genWeightSpace_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 ≤ chainTopCoeff α β
hα : α = 0
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (⇑β : (a : L) → R)) ⊥

Tactic:
exact β.genWeightSpace_ne_bot

Premises used: LieModule.Weight.genWeightSpace_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 ≤ chainTopCoeff α β
hα : ¬α = 0
⊢ ¬α = 0

Tactic:
rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, chainTopCoeff_add_one _ _ hα] at hn

Premises used: Nat.succ_eq_add_one, LieModule.chainTopCoeff_add_one, Nat.lt_succ_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 : n ≤ chainTopCoeff α β
hα hα₁ : ¬α = 0
⊢ n < Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯

Tactic:
rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, chainTopCoeff_add_one _ _ hα] at hn

Premises used: Nat.succ_eq_add_one, LieModule.chainTopCoeff_add_one, Nat.lt_succ_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 : ℕ
hα : ¬α = 0
hn : n < Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥

Tactic:
Nat.find_min (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists hn

Premises used: Filter.Eventually.exists, Nat.find_min, LieModule.eventually_genWeightSpace_smul_add_eq_bot, DFunLike.coe
-- 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 : ℕ
hα : ¬α = 0
hn : n < Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥

Tactic:
exact Nat.find_min (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists hn

Premises used: Filter.Eventually.exists, Nat.find_min, LieModule.eventually_genWeightSpace_smul_add_eq_bot, DFunLike.coe
-- 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 ≤ 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))) ⊥
neg₂ neg₃ neg₄ :
  ∀ (hα : ¬α = 0)
    (hn :
      n <
        Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯),
    Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
⊢ 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

Premises used: Nat.succ_eq_add_one, LieModule.chainTopCoeff_add_one, Nat.lt_succ_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 : -(↑(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))) ⊥
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))) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥

Tactic:
rcases n with (n | n)