awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
refine :
  LieSubmodule.restr I H ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)
⊢ LieSubmodule.restr I H =
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
refine le_antisymm ?_ (sup_le inf_le_left (iSup₂_le fun _ _ ↦ inf_le_left))

Premises used: iSup₂_le, le_antisymm, sup_le
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
rw : ⨆ (χ : Weight K (↥H) L), LieSubmodule.restr I H ⊓ genWeightSpace L (⇑χ : (a : ↥H) → K)
| LieSubmodule.restr I H

Tactic:
rw [lieIdeal_eq_iSup_inf_genWeightSpace]

Premises used: LieAlgebra.lieIdeal_eq_iSup_inf_genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
conv_lhs :
  ⨆ (χ : Weight K (↥H) L), LieSubmodule.restr I H ⊓ genWeightSpace L (⇑χ : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)
⊢ LieSubmodule.restr I H ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
conv_lhs => rw [lieIdeal_eq_iSup_inf_genWeightSpace]

Premises used: LieAlgebra.lieIdeal_eq_iSup_inf_genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
pos :
  ∀ (hα : α.IsZero),
    LieSubmodule.restr I H ⊓ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
      LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
        ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)
neg :
  ∀ (hα : ¬α.IsZero),
    LieSubmodule.restr I H ⊓ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
      LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
        ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)
⊢ LieSubmodule.restr I H ⊓ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsZero
h :
  ∀ (m : L), Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) m ↔ m ∈ H.toLieSubmodule
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) = H.toLieSubmodule

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsZero
m : L
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) m ↔ m ∈ H.toLieSubmodule

Tactic:
simp [hα.eq]

Premises used: LieModule.Weight.IsZero.eq
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsZero
pos :
  LieSubmodule.restr I H ⊓ H.toLieSubmodule ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)
⊢ LieSubmodule.restr I H ⊓ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
rw [show genWeightSpace L (α : H → K) = H.toLieSubmodule from by ext; simp [hα.eq]]
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsZero
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
le_sup_left

Premises used: le_sup_left, Set.Mem
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsZero
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ LieSubmodule.restr I H ⊓ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
le_sup_of_le_right (le_iSup₂_of_le α hα le_rfl)

Premises used: le_rfl, Set.Mem, le_sup_of_le_right, le_iSup₂_of_le
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ LieSubmodule.restr I H ⊓ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
exact le_sup_of_le_right (le_iSup₂_of_le α hα le_rfl)

Premises used: le_rfl, le_sup_of_le_right, le_iSup₂_of_le
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ ⨆ (χ : Weight K (↥H) L), LieSubmodule.restr I H ⊓ genWeightSpace L (⇑χ : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
exact iSup_le fun α ↦ by
    by_cases hα : α.IsZero
    · rw [show genWeightSpace L (α : H → K) = H.toLieSubmodule from by ext; simp [hα.eq]]
      exact le_sup_left
    · exact le_sup_of_le_right (le_iSup₂_of_le α hα le_rfl)

Premises used: iSup_le
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
rw :
  ∀ (i : Weight K (↥H) L),
    genWeightSpace L (⇑i : (a : ↥H) → K) ≤
      H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)
⊢ H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K) = ⊤

Tactic:
rw [eq_top_iff, ← LieModule.iSup_genWeightSpace_eq_top', iSup_le_iff]

Premises used: eq_top_iff, LieModule.iSup_genWeightSpace_eq_top', iSup_le_iff
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
pos :
  ∀ (hα : α.IsZero),
    genWeightSpace L (⇑α : (a : ↥H) → K) ≤
      H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)
neg :
  ∀ (hα : ¬α.IsZero),
    genWeightSpace L (⇑α : (a : ↥H) → K) ≤
      H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : α.IsZero
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
simp [hα]
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
le_sup_of_le_right <| le_iSup₂_of_le α hα (le_refl _)

Premises used: le_refl, Set.Mem, le_sup_of_le_right, le_iSup₂_of_le
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
exact le_sup_of_le_right <| le_iSup₂_of_le α hα (le_refl _)

Premises used: le_refl, le_sup_of_le_right, le_iSup₂_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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun (k : ℕ) ↦ k • χ₁ + χ₂
this : Injective f
rw : (f '' {x : ℕ | ¬Eq (α := LieSubmodule R L M) (genWeightSpace M (x • χ₁ + χ₂)) ⊥}).Finite
⊢ ∀ᶠ (k : ℕ) in Filter.atTop, Eq (α := LieSubmodule R L M) (genWeightSpace M (k • χ₁ + χ₂)) ⊥

Tactic:
rw [← Nat.cofinite_eq_atTop, Filter.eventually_cofinite, ← finite_image_iff this.injOn]

Premises used: Function.Injective.injOn, Filter.eventually_cofinite, Set.finite_image_iff, Nat.cofinite_eq_atTop
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun (k : ℕ) ↦ k • χ₁ + χ₂
this : Injective f
apply :
  f '' {x : ℕ | ¬Eq (α := LieSubmodule R L M) (genWeightSpace M (x • χ₁ + χ₂)) ⊥} ⊆
    {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥}
⊢ (f '' {x : ℕ | ¬Eq (α := LieSubmodule R L M) (genWeightSpace M (x • χ₁ + χ₂)) ⊥}).Finite

Tactic:
apply (finite_genWeightSpace_ne_bot R L M).subset

Premises used: Set.Finite.subset, LieModule.finite_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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun (k : ℕ) ↦ k • χ₁ + χ₂
this : Injective f
⊢ f '' {x : ℕ | ¬Eq (α := LieSubmodule R L M) (genWeightSpace M (x • χ₁ + χ₂)) ⊥} ⊆
    {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥}

Tactic:
simp [f]
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun (k : ℕ) ↦ k • χ₁ + χ₂
suffices : Injective f
⊢ ∀ᶠ (k : ℕ) in Filter.atTop, Eq (α := LieSubmodule R L M) (genWeightSpace M (k • χ₁ + χ₂)) ⊥

Tactic:
suffices Injective f by
    rw [← Nat.cofinite_eq_atTop, Filter.eventually_cofinite, ← finite_image_iff this.injOn]
    apply (finite_genWeightSpace_ne_bot R L M).subset
    simp [f]
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun (k : ℕ) ↦ k • χ₁ + χ₂
k l : ℕ
hkl : f k = f l
⊢ HSMul.hSMul (α := ℤ) (↑k : ℤ) χ₁ = HSMul.hSMul (α := ℤ) (↑l : ℤ) χ₁

Tactic:
simpa only [f, add_left_inj, natCast_zsmul] using hkl

Premises used: add_left_inj, natCast_zsmul
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun (k : ℕ) ↦ k • χ₁ + χ₂
k l : ℕ
hkl : f k = f l
⊢ HSMul.hSMul (α := ℤ) (↑k : ℤ) χ₁ = HSMul.hSMul (α := ℤ) (↑l : ℤ) χ₁

Tactic:
replace hkl : (k : ℤ) • χ₁ = (l : ℤ) • χ₁ := by
    simpa only [f, add_left_inj, natCast_zsmul] using hkl
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun (k : ℕ) ↦ k • χ₁ + χ₂
k l : ℕ
hkl : HSMul.hSMul (α := ℤ) (↑k : ℤ) χ₁ = HSMul.hSMul (α := ℤ) (↑l : ℤ) χ₁
⊢ k = l

Tactic:
Nat.cast_inj.mp <| smul_left_injective ℤ hχ₁ hkl

Premises used: smul_left_injective, Int, Nat.cast_inj, Iff.mp
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun (k : ℕ) ↦ k • χ₁ + χ₂
k l : ℕ
hkl : HSMul.hSMul (α := ℤ) (↑k : ℤ) χ₁ = HSMul.hSMul (α := ℤ) (↑l : ℤ) χ₁
⊢ k = l

Tactic:
exact Nat.cast_inj.mp <| smul_left_injective ℤ hχ₁ hkl

Premises used: smul_left_injective, Int, Nat.cast_inj, Iff.mp
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
⊢ ∃ k > 0, Eq (α := LieSubmodule R L M) (genWeightSpace M (k • χ₁ + χ₂)) ⊥

Tactic:
(Nat.eventually_pos.and <| eventually_genWeightSpace_smul_add_eq_bot M χ₁ χ₂ hχ₁).exists

Premises used: Filter.Eventually.and, Nat.eventually_pos, Filter.Eventually.exists, LieModule.eventually_genWeightSpace_smul_add_eq_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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
obtain :
  ∀ (q : ℕ) (hq₀ : q > 0) (hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥),
    ∃ p < 0,
      ∃ q > 0,
        Eq (α := LieSubmodule R L M) (genWeightSpace M (p • χ₁ + χ₂)) ⊥ ∧
          Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
⊢ ∃ p < 0,
    ∃ q > 0,
      Eq (α := LieSubmodule R L M) (genWeightSpace M (p • χ₁ + χ₂)) ⊥ ∧
        Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥

Tactic:
obtain ⟨q, hq₀, hq⟩ := exists_genWeightSpace_smul_add_eq_bot M χ₁ χ₂ hχ₁

Premises used: LieModule.exists_genWeightSpace_smul_add_eq_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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
obtain :
  ∀ (p : ℕ) (hp₀ : p > 0) (hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥),
    ∃ p < 0,
      ∃ q > 0,
        Eq (α := LieSubmodule R L M) (genWeightSpace M (p • χ₁ + χ₂)) ⊥ ∧
          Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
⊢ ∃ p < 0,
    ∃ q > 0,
      Eq (α := LieSubmodule R L M) (genWeightSpace M (p • χ₁ + χ₂)) ⊥ ∧
        Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥

Tactic:
obtain ⟨p, hp₀, hp⟩ := exists_genWeightSpace_smul_add_eq_bot M (-χ₁) χ₂ (neg_ne_zero.mpr hχ₁)

Premises used: Iff.mpr, LieModule.exists_genWeightSpace_smul_add_eq_bot, neg_ne_zero, 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
p : ℕ
hp₀ : p > 0
hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
⊢ LT.lt (α := ℤ) (-(↑p : ℤ)) 0

Tactic:
simpa
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
p : ℕ
hp₀ : p > 0
hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
⊢ GT.gt (α := ℤ) (↑q : ℤ) 0

Tactic:
simpa
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
p : ℕ
hp₀ : p > 0
hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
refine_1 : Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (-(↑p : ℤ)) χ₁ + χ₂)) ⊥
refine_2 : Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (↑q : ℤ) χ₁ + χ₂)) ⊥
⊢ ∃ p < 0,
    ∃ q > 0,
      Eq (α := LieSubmodule R L M) (genWeightSpace M (p • χ₁ + χ₂)) ⊥ ∧
        Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥

Tactic:
refine ⟨-(p : ℤ), by simpa, q, by simpa, ?_, ?_⟩
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
p : ℕ
hp₀ : p > 0
hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
refine_1 : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (-(↑p : ℤ)) χ₁ + χ₂)) ⊥

Tactic:
rw [neg_smul, ← smul_neg, natCast_zsmul]

Premises used: neg_smul, smul_neg, natCast_zsmul
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
p : ℕ
hp₀ : p > 0
hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥

Tactic:
hp