awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
hl₁ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
hl₂ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have hl₃ : Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
Tactic: obtain ⟨hl₁, hl₂, hl₃⟩ := hl l (le_refl _)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
hl₁ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
hl₂ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)
hl₃ : Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have simp_rw : LieSubmodule.map N₁.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) ⊔
    LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
  ⨅ (k : ℕ), lowerCentralSeries R L M k
Tactic: simp_rw [← iInf_lowerCentralSeries_eq_posFittingComp, hl₁, hl₂, hl₃,
    LieSubmodule.lowerCentralSeries_map_eq_lcs, ← LieSubmodule.lcs_sup, lowerCentralSeries,
    h.eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
hl₁ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
hl₂ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)
hl₃ : Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
simp_rw :
  LieSubmodule.map N₁.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have simp_rw₁ : LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
    LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
  ⨅ (k : ℕ), lowerCentralSeries R L M k
Tactic: simp_rw [← iInf_lowerCentralSeries_eq_posFittingComp, hl₁, hl₂, hl₃,
    LieSubmodule.lowerCentralSeries_map_eq_lcs, ← LieSubmodule.lcs_sup, lowerCentralSeries,
    h.eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
hl₁ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
hl₂ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)
hl₃ : Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
simp_rw :
  LieSubmodule.map N₁.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₁ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have simp_rw₂ : LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔ LieSubmodule.map N₂.incl (lowerCentralSeries R L (↥N₂) l) =
  ⨅ (k : ℕ), lowerCentralSeries R L M k
Tactic: simp_rw [← iInf_lowerCentralSeries_eq_posFittingComp, hl₁, hl₂, hl₃,
    LieSubmodule.lowerCentralSeries_map_eq_lcs, ← LieSubmodule.lcs_sup, lowerCentralSeries,
    h.eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
hl₁ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
hl₂ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)
hl₃ : Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
simp_rw :
  LieSubmodule.map N₁.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₁ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₂ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (lowerCentralSeries R L (↥N₂) l) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have simp_rw₃ : LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔ LieSubmodule.map N₂.incl (lowerCentralSeries R L (↥N₂) l) =
  lowerCentralSeries R L M l
Tactic: simp_rw [← iInf_lowerCentralSeries_eq_posFittingComp, hl₁, hl₂, hl₃,
    LieSubmodule.lowerCentralSeries_map_eq_lcs, ← LieSubmodule.lcs_sup, lowerCentralSeries,
    h.eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
hl₁ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
hl₂ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)
hl₃ : Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
simp_rw :
  LieSubmodule.map N₁.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₁ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₂ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (lowerCentralSeries R L (↥N₂) l) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₃ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (lowerCentralSeries R L (↥N₂) l) =
    lowerCentralSeries R L M l
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have simp_rw₄ : LieSubmodule.lcs l N₁ ⊔ LieSubmodule.lcs l N₂ = lowerCentralSeries R L M l
Tactic: simp_rw [← iInf_lowerCentralSeries_eq_posFittingComp, hl₁, hl₂, hl₃,
    LieSubmodule.lowerCentralSeries_map_eq_lcs, ← LieSubmodule.lcs_sup, lowerCentralSeries,
    h.eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
hl₁ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
hl₂ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)
hl₃ : Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
simp_rw :
  LieSubmodule.map N₁.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₁ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₂ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (lowerCentralSeries R L (↥N₂) l) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₃ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (lowerCentralSeries R L (↥N₂) l) =
    lowerCentralSeries R L M l
simp_rw₄ : LieSubmodule.lcs l N₁ ⊔ LieSubmodule.lcs l N₂ = lowerCentralSeries R L M l
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have simp_rw₅ : LieSubmodule.lcs l (N₁ ⊔ N₂) = lowerCentralSeries R L M l
Tactic: simp_rw [← iInf_lowerCentralSeries_eq_posFittingComp, hl₁, hl₂, hl₃,
    LieSubmodule.lowerCentralSeries_map_eq_lcs, ← LieSubmodule.lcs_sup, lowerCentralSeries,
    h.eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k)
        (lowerCentralSeries R L (↥N₁) b) ∧
      Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k)
          (lowerCentralSeries R L (↥N₂) b) ∧
        Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M b)
hl₁ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)
hl₂ :
  Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)
hl₃ : Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
simp_rw :
  LieSubmodule.map N₁.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₁ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₂ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (lowerCentralSeries R L (↥N₂) l) =
    ⨅ (k : ℕ), lowerCentralSeries R L M k
simp_rw₃ :
  LieSubmodule.map N₁.incl (lowerCentralSeries R L (↥N₁) l) ⊔
      LieSubmodule.map N₂.incl (lowerCentralSeries R L (↥N₂) l) =
    lowerCentralSeries R L M l
simp_rw₄ : LieSubmodule.lcs l N₁ ⊔ LieSubmodule.lcs l N₂ = lowerCentralSeries R L M l
simp_rw₅ : LieSubmodule.lcs l (N₁ ⊔ N₂) = lowerCentralSeries R L M l
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M
have simp_rw₆ : LieSubmodule.lcs l (N₁ ⊔ N₂) = LieSubmodule.lcs l ⊤
Tactic: simp_rw [← iInf_lowerCentralSeries_eq_posFittingComp, hl₁, hl₂, hl₃,
    LieSubmodule.lowerCentralSeries_map_eq_lcs, ← LieSubmodule.lcs_sup, lowerCentralSeries,
    h.eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
⊢ IsCompl M₀ M₁
have inl : ∀ (h : ∀ (a : L), Eq (α := LieSubmodule R L M) (genWeightSpaceOf M 0 a) ⊤), IsCompl M₀ M₁
Tactic: rcases forall_or_exists_not (fun (x : L) ↦ genWeightSpaceOf M (0 : R) x = ⊤)
    with h | ⟨x, hx : genWeightSpaceOf M (0 : R) x ≠ ⊤⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
inl : ∀ (h : ∀ (a : L), Eq (α := LieSubmodule R L M) (genWeightSpaceOf M 0 a) ⊤), IsCompl M₀ M₁
⊢ IsCompl M₀ M₁
have inr : ∀ (x : L) (hx : Ne (α := LieSubmodule R L M) (genWeightSpaceOf M 0 x) ⊤), IsCompl M₀ M₁
Tactic: rcases forall_or_exists_not (fun (x : L) ↦ genWeightSpaceOf M (0 : R) x = ⊤)
    with h | ⟨x, hx : genWeightSpaceOf M (0 : R) x ≠ ⊤⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
h_1 : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
h : ∀ (a : L), Eq (α := LieSubmodule R L M) (genWeightSpaceOf M 0 a) ⊤
⊢ IsCompl M₀ M₁
have inl : IsNilpotent L M
Tactic: suffices IsNilpotent L M by simp [M₀, M₁, isCompl_top_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
h_1 : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
h : ∀ (a : L), Eq (α := LieSubmodule R L M) (genWeightSpaceOf M 0 a) ⊤
⊢ IsNilpotent L M
have h₁ : M₀ = ⊤
Tactic: replace h : M₀ = ⊤ := by simpa [M₀, genWeightSpace]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
h_1 : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
h : M₀ = ⊤
⊢ IsNilpotent L M
have inl : IsNilpotent.{u_3, u_4} L ↥M₀
Tactic: rw [← LieModule.isNilpotent_of_top_iff' (R := R), ← h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
⊢ IsCompl M₀ M₁
have h₁ : IsCompl M₀ₓ M₁ₓ
Tactic: have h₁ : IsCompl M₀ₓ M₁ₓ := isCompl_genWeightSpaceOf_zero_posFittingCompOf R L M x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
⊢ IsCompl M₀ M₁
have h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
Tactic: have h₂ : IsCompl M₀ₓ₀ M₀ₓ₁ := h M₀ₓ hx.lt_top
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
⊢ LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
have rw : genWeightSpace M 0 ≤ M₀ₓ
Tactic: rw [map_genWeightSpace_eq_of_injective M₀ₓ.injective_incl, inf_eq_left,
        LieSubmodule.range_incl]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 : IsNoetherian R M
inst_9 : IsArtinian R M
h : ∀ N < ⊤, IsCompl.{u_4} (α := LieSubmodule R L ↥N) (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
⊢ IsCompl M₀ M₁
have h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
Tactic: have h₃ : M₀ₓ₀.map M₀ₓ.incl = M₀ := by
      rw [map_genWeightSpace_eq_of_injective M₀ₓ.injective_incl, inf_eq_left,
        LieSubmodule.range_incl]
      exact iInf_le _ x