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
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))) ⊥) ⋯
⊢ chainTopCoeff α β + 1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
have rw₁ : (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) sorry).pred +
    1 =
  Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) sorry
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)
-- 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 :
  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))) ⊥) ⋯
⊢ chainTopCoeff α β + 1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
have a : 0 < Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) sorry
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)
-- 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 :
  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))) ⊥) ⋯
⊢ chainTopCoeff α β + 1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
have a₁ : Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) sorry ≠ 0
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)
-- 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 :
  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
⊢ chainTopCoeff α β + 1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
have a₃ : ∀
  (e :
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) sorry = 0)
  (this : Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 α + (⇑β : (a : L) → R))) ⊥), False
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)
-- 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 ((chainTopCoeff α β + 1) • α + (⇑β : (a : L) → R))) ⊥
have rw : Eq (α := LieSubmodule R L M)
  (genWeightSpace M
    (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) sorry •
        α +
      (⇑β : (a : L) → R)))
  ⊥
Tactic: rw [chainTopCoeff_add_one _ _ 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 ((chainTopCoeff α β + 1) • α + (⇑β : (a : L) → R))) ⊥
have rw : Eq (α := LieSubmodule R L M)
  (genWeightSpace M
    (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) sorry •
        α +
      (⇑β : (a : L) → R)))
  ⊥
Tactic: classical
  rw [chainTopCoeff_add_one _ _ hα]
  exact Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists
-- 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 (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw : Eq (α := LieSubmodule R L M)
  (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
  (genWeightSpace M ((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]
-- 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 (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
    (genWeightSpace M ((chainTopCoeff α β + 1) • α + (⇑β : (a : L) → R)))
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw₁ : Eq (α := LieSubmodule R L M)
  (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
  (genWeightSpace M (HSMul.hSMul (α := ℤ) (↑(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]
-- 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 (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)))
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw₂ : Eq (α := LieSubmodule R L M)
  (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
  (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]
-- 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 (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)))
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw₃ : Eq (α := LieSubmodule R L M)
  (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R)))
  (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]
-- 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 (HSub.hSub (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw : Eq (α := LieSubmodule R L M)
  (genWeightSpace M (HAdd.hAdd (α := ℤ) (-(↑(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α)]
-- 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 (HAdd.hAdd (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) (-1) • α + (⇑β : (a : L) → R))) ⊥
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HSub.hSub (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw₁ : Eq (α := LieSubmodule R L M)
  (genWeightSpace M (-HAdd.hAdd (α := ℤ) (↑(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α)]
-- 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 (HAdd.hAdd (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) (-1) • α + (⇑β : (a : L) → R))) ⊥
rw₁ :
  Eq (α := LieSubmodule R L M)
    (genWeightSpace M (-HAdd.hAdd (α := ℤ) (↑(chainBotCoeff α β) : ℤ) 1 • α + (⇑β : (a : L) → R))) ⊥
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HSub.hSub (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw₂ : Eq (α := LieSubmodule R L M)
  (genWeightSpace M (-(HAdd.hAdd (α := ℤ) (↑(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α)]
-- 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 (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))) ⊥
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HSub.hSub (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw₃ : Eq (α := LieSubmodule R L M)
  (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(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α)]
-- 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 (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))) ⊥
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HSub.hSub (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw₄ : Eq (α := LieSubmodule R L M)
  (genWeightSpace M (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (-α) β) : ℤ) 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α)]
-- 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 (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))) ⊥
⊢ Eq (α := LieSubmodule R L M)
    (genWeightSpace M (HSub.hSub (α := ℤ) (-(↑(chainBotCoeff α β) : ℤ)) 1 • α + (⇑β : (a : L) → R))) ⊥
have rw₅ : Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊥
Tactic: rw [sub_eq_add_neg, ← neg_add, neg_smul, ← smul_neg, chainBotCoeff,
    genWeightSpace_chainTopCoeff_add_one_zsmul_add _ _ (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
n : ℕ
hn : n ≤ chainTopCoeff α β
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
have pos : ∀ (hα : α = 0), Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
Tactic: by_cases hα : α = 0
-- 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 α β
pos : ∀ (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), Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
Tactic: by_cases hα : α = 0
-- 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 pos : Ne (α := LieSubmodule R L M) (genWeightSpace M (⇑β : (a : L) → R)) ⊥
Tactic: rw [hα, smul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (hypothesis)
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
⊢ Ne (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥
have hn₁ : n < Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) sorry
Tactic: rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, chainTopCoeff_add_one _ _ hα] at hn
Cleared hypotheses: hn, hα