awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
u : L
⊢ Membership.mem (γ := Set L) ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s) u ↔
    Membership.mem (γ := Set L) {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x} u
have h : (∃ (x : u ∈ H),
    Membership.mem (γ := Set ↥H.toSubmodule) {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
      (Subtype.mk (p := fun (a : L) ↦ a ∈ H.toSubmodule) u sorry)) ↔
  ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
Tactic: simp only [Submodule.coe_subtype, mem_image, Subtype.exists, LieSubalgebra.mem_toSubmodule,
    exists_and_right, exists_eq_right, mem_setOf_eq, s]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
u : L
⊢ (∃ (x : u ∈ H),
      Membership.mem (γ := Set ↥H.toSubmodule) {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
        (Subtype.mk (p := fun (a : L) ↦ a ∈ H.toSubmodule) u ⋯)) ↔
    ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
have h : (∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u) →
  ∀ (y : L) (hy : y ∈ rootSpace H α) (z : L) (hz : z ∈ rootSpace H (-α)) (hyz : ⁅y, z⁆ = u), u ∈ H
Tactic: refine ⟨fun ⟨_, y, hy, z, hz, hyz⟩ ↦ ⟨y, hy, z, hz, hyz⟩,
    fun ⟨y, hy, z, hz, hyz⟩ ↦ ⟨?_, y, hy, z, hz, hyz⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
u : L
h : ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = u
⊢ u ∈ H
have a : u ∈ H ↔
  (↑((rootSpaceProduct R L H α (-α) 0 sorry : (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥(rootSpace H 0))
          (Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H α) y hy ⊗ₜ[R]
            Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (-α)) z hz)) :
      L) ∈
    rootSpace H 0
Tactic: convert!
    (rootSpaceProduct R L H α (-α) 0 (add_neg_cancel α) (⟨y, hy⟩ ⊗ₜ[R] ⟨z, hz⟩)).property using 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
⊢ LieSubmodule.restr I H =
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)
have 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)
Tactic: refine le_antisymm ?_ (sup_le inf_le_left (iSup₂_le fun _ _ ↦ inf_le_left))
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
| LieSubmodule.restr I H
have rw : ⨆ (χ : Weight K (↥H) L), LieSubmodule.restr I H ⊓ genWeightSpace L (⇑χ : (a : ↥H) → K)
Tactic: rw [lieIdeal_eq_iSup_inf_genWeightSpace]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
⊢ LieSubmodule.restr I H ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)
have 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)
Tactic: conv_lhs => rw [lieIdeal_eq_iSup_inf_genWeightSpace]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
have 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)
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) = H.toLieSubmodule
have h : ∀ (m : L), Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) m ↔ m ∈ H.toLieSubmodule
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
have 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)
Tactic: rw [show genWeightSpace L (α : H → K) = H.toLieSubmodule from by ext; simp [hα.eq]]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
⊢ H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K) = ⊤
have rw : ∀ (i : Weight K (↥H) L),
  genWeightSpace L (⇑i : (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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)
have pos : ∀ (hα : α.IsZero),
  genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)
have neg : ∀ (hα : ¬α.IsZero),
  genWeightSpace L (⇑α : (a : ↥H) → K) ≤
    H.toLieSubmodule ⊔ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), rootSpace H (⇑α : (a : ↥H) → K)
Tactic: by_cases hα : α.IsZero
-- 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
χ₁ χ₂ : 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
⊢ ∀ᶠ (k : ℕ) in Filter.atTop, Eq (α := LieSubmodule R L M) (genWeightSpace M (k • χ₁ + χ₂)) ⊥
have rw : (f '' {x : ℕ | ¬Eq (α := LieSubmodule R L M) (genWeightSpace M (x • χ₁ + χ₂)) ⊥}).Finite
Tactic: rw [← Nat.cofinite_eq_atTop, Filter.eventually_cofinite, ← finite_image_iff this.injOn]
-- 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
χ₁ χ₂ : 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 • χ₁ + χ₂)) ⊥}).Finite
have apply : f '' {x : ℕ | ¬Eq (α := LieSubmodule R L M) (genWeightSpace M (x • χ₁ + χ₂)) ⊥} ⊆
  {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥}
Tactic: apply (finite_genWeightSpace_ne_bot R L M).subset
-- 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
χ₁ χ₂ : 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 : ℕ) in Filter.atTop, Eq (α := LieSubmodule R L M) (genWeightSpace M (k • χ₁ + χ₂)) ⊥
have suffices : Injective f
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]
-- 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
χ₁ χ₂ : 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
⊢ k = l
have hkl₁ : HSMul.hSMul (α := ℤ) (↑k : ℤ) χ₁ = HSMul.hSMul (α := ℤ) (↑l : ℤ) χ₁
Tactic: replace hkl : (k : ℤ) • χ₁ = (l : ℤ) • χ₁ := by
    simpa only [f, add_left_inj, natCast_zsmul] using hkl
Cleared hypotheses: hkl
-- 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
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
⊢ ∃ p < 0,
    ∃ q > 0,
      Eq (α := LieSubmodule R L M) (genWeightSpace M (p • χ₁ + χ₂)) ⊥ ∧
        Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
have 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 • χ₁ + χ₂)) ⊥
Tactic: obtain ⟨q, hq₀, hq⟩ := exists_genWeightSpace_smul_add_eq_bot M χ₁ χ₂ 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
χ₁ χ₂ : 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 < 0,
    ∃ q > 0,
      Eq (α := LieSubmodule R L M) (genWeightSpace M (p • χ₁ + χ₂)) ⊥ ∧
        Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
have 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 • χ₁ + χ₂)) ⊥
Tactic: obtain ⟨p, hp₀, hp⟩ := exists_genWeightSpace_smul_add_eq_bot M (-χ₁) χ₂ (neg_ne_zero.mpr 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
χ₁ χ₂ : 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 • -χ₁ + χ₂)) ⊥
⊢ ∃ p < 0,
    ∃ q > 0,
      Eq (α := LieSubmodule R L M) (genWeightSpace M (p • χ₁ + χ₂)) ⊥ ∧
        Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
have refine_1 : Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (-(↑p : ℤ)) χ₁ + χ₂)) ⊥
Tactic: refine ⟨-(p : ℤ), by simpa, q, by simpa, ?_, ?_⟩
-- 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
χ₁ χ₂ : 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 : ℤ)) χ₁ + χ₂)) ⊥
⊢ ∃ p < 0,
    ∃ q > 0,
      Eq (α := LieSubmodule R L M) (genWeightSpace M (p • χ₁ + χ₂)) ⊥ ∧
        Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
have refine_2 : Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (↑q : ℤ) χ₁ + χ₂)) ⊥
Tactic: refine ⟨-(p : ℤ), by simpa, q, by simpa, ?_, ?_⟩
-- 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
χ₁ χ₂ : L → R
p q : ℤ
⊢ Eq (α := LieSubmodule R L M) (genWeightSpaceChain M χ₁ χ₂ p q) (⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • χ₁ + χ₂))
have this : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q
Tactic: have : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q := by simp
-- 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
χ₁ χ₂ : L → R
p q : ℤ
e : ℤ ≃ ℤ := Involutive.toPerm Neg.neg ⋯
⊢ Eq (α := LieSubmodule R L M) (genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p)) (genWeightSpaceChain M χ₁ χ₂ p q)
have simp_rw : Eq.{u_3 + 1} (α := LieSubmodule R L M) (⨆ k ∈ Ioo (-q) (-p), genWeightSpace M (k • -χ₁ + χ₂))
  (⨆ (i : ℤ),
    ⨆ (_ : Membership.mem (γ := Set ℤ) ((⇑e.symm : (a : ℤ) → ℤ) '' Ioo p q) i),
      genWeightSpace M (HSMul.hSMul (α := ℤ) ((e : (a : ℤ) → ℤ) i : ℤ) χ₁ + χ₂))
Tactic: simp_rw [genWeightSpaceChain, ← e.biSup_comp (Ioo p q)]
-- 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
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) y
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆
have hy₁ : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
  (⨆ (x : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑x : ℤ) • α + χ)) y
Tactic: rw [genWeightSpaceChain, iSup_subtype'] at hy
Cleared hypotheses: hy
-- 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
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y : M
k : Subtype (Membership.mem (Ioo p q))
z : M
hz : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((↑k : ℤ) • α + χ)) z
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆
have mem : ∀ (k : ℤ) (hk : k ∈ Ioo p q)
  (hz :
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
      (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p q)) k hk) : ℤ) • α + χ)) z),
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆
Tactic: obtain ⟨k, hk⟩ := k
Cleared hypotheses: k, hz
-- 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
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p q)) k hk) : ℤ) • α + χ)) z
this :
  LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (genWeightSpaceChain M α χ p q)
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆
have a : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ)) ⁅x, z⁆
Tactic: apply 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
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p q)) k hk) : ℤ) • α + χ)) z
this :
  LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (genWeightSpaceChain M α χ p q)
⊢ α + (k • α + χ) = (k + 1) • α + χ
have rw : α + (k • α + χ) = k • α + HSMul.hSMul (α := ℤ) 1 α + χ
Tactic: rw [add_smul]
-- 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
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p q)) k hk) : ℤ) • α + χ)) z
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆
have mem : LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ)) (genWeightSpaceChain M α χ p q)
Tactic: suffices genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q by
      apply this
      -- was `simpa using [...]` and very slow
      -- (https://github.com/leanprover-community/mathlib4/issues/19751)
      simpa only [zsmul_eq_mul, Int.cast_add, Pi.intCast_def, Int.cast_one] using
        (rootSpaceWeightSpaceProduct R L H M α (k • α + χ) ((k + 1) • α + χ)
            (by rw [add_smul]; abel) (⟨x, hx⟩ ⊗ₜ ⟨z, hz⟩)).property