awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm : Membership.mem (α := M₂) (↑(↑(genWeightSpace M₂ χ) : Submodule R M₂) : Set M₂) ((f : (a : M) → M₂) m : M₂)
⊢ ∃ (m_1 : M),
    Membership.mem (α := M₂) (γ := LieSubmodule R L M₂) (genWeightSpace M₂ χ) ((f : (a : M) → M₂) m_1 : M₂) ∧
      Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) m_1 : M₂) ((f : (a : M) → M₂) m : M₂)

Tactic:
⟨m, hm, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm : Membership.mem (α := M₂) (↑(↑(genWeightSpace M₂ χ) : Submodule R M₂) : Set M₂) ((f : (a : M) → M₂) m : M₂)
⊢ ∃ (m_1 : M),
    Membership.mem (α := M₂) (γ := LieSubmodule R L M₂) (genWeightSpace M₂ χ) ((f : (a : M) → M₂) m_1 : M₂) ∧
      Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) m_1 : M₂) ((f : (a : M) → M₂) m : M₂)

Tactic:
exact ⟨m, hm, rfl⟩
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
e : M ≃ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map e.toLieModuleHom (genWeightSpace M χ) = genWeightSpace M₂ χ

Tactic:
simp [map_genWeightSpace_eq_of_injective e.injective]

Premises used: LieModuleEquiv.injective, LieModule.map_genWeightSpace_eq_of_injective
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M) = posFittingComp R L M₂

Tactic:
le_antisymm (map_posFittingComp_le _) ?_

Premises used: le_antisymm, LieModule.map_posFittingComp_le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
refine : posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)
⊢ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M) = posFittingComp R L M₂

Tactic:
refine le_antisymm (map_posFittingComp_le _) ?_

Premises used: le_antisymm, LieModule.map_posFittingComp_le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
this :
  posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
rw :
  LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂)) ≤
    LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)
⊢ posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
this :
  posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
⊢ LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂)) ≤
    LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Tactic:
LieSubmodule.map_mono (map_posFittingComp_le _)

Premises used: LieModule.map_posFittingComp_le, LieSubmodule.map_mono
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
this :
  posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
⊢ LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂)) ≤
    LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Tactic:
exact LieSubmodule.map_mono (map_posFittingComp_le _)

Premises used: LieModule.map_posFittingComp_le, LieSubmodule.map_mono
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
suffices :
  posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
⊢ posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Tactic:
suffices posFittingComp R L M₂ = ((posFittingComp R L M₂).map (e.symm : M₂ →ₗ⁅R,L⁆ M)).map e by
    rw [this]
    exact LieSubmodule.map_mono (map_posFittingComp_le _)
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
rw : posFittingComp R L M₂ = LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)
⊢ posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))

Tactic:
rw [← LieSubmodule.map_comp]

Premises used: LieSubmodule.map_comp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)) =
    LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)

Tactic:
LieSubmodule.map_id

Premises used: LieSubmodule.map_id
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
h :
  posFittingComp R L M₂ =
    LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))
⊢ posFittingComp R L M₂ = LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)

Tactic:
convert! LieSubmodule.map_id

Premises used: LieSubmodule.map_id
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
h :
  ∀ (m : M₂),
    Membership.mem (γ := LieSubmodule R L M₂) (posFittingComp R L M₂) m ↔
      m ∈ LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))
⊢ posFittingComp R L M₂ =
    LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
m : M₂
⊢ Membership.mem (γ := LieSubmodule R L M₂) (posFittingComp R L M₂) m ↔
    m ∈ LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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₂
obtain :
  ∀ (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)),
    LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
      posFittingComp R L M
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M

Tactic:
obtain ⟨l, hl⟩ := Filter.eventually_atTop.mp <|
    (eventually_iInf_lowerCentralSeries_eq R L N₁).and <|
    (eventually_iInf_lowerCentralSeries_eq R L N₂).and
    (eventually_iInf_lowerCentralSeries_eq R L M)

Premises used: Membership.mem, Filter.Eventually.and, Subtype, Iff.mp, LieModule.eventually_iInf_lowerCentralSeries_eq, Filter.eventually_atTop
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
⊢ Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₁) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₁) k) (lowerCentralSeries R L (↥N₁) l)

Tactic:
obtain ⟨hl₁, hl₂, hl₃⟩ := hl l (le_refl _)

Premises used: le_refl
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
⊢ Eq.{u_4 + 1} (α := LieSubmodule R L ↥N₂) (⨅ (k : ℕ), lowerCentralSeries R L (↥N₂) k) (lowerCentralSeries R L (↥N₂) l)

Tactic:
obtain ⟨hl₁, hl₂, hl₃⟩ := hl l (le_refl _)

Premises used: le_refl
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
⊢ 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 _)

Premises used: le_refl
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
simp_rw₆ : LieSubmodule.lcs l (N₁ ⊔ N₂) = LieSubmodule.lcs l ⊤
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M

Tactic:
simp_rw [← iInf_lowerCentralSeries_eq_posFittingComp, hl₁, hl₂, hl₃,
    LieSubmodule.lowerCentralSeries_map_eq_lcs, ← LieSubmodule.lcs_sup, lowerCentralSeries,
    h.eq_top]

Premises used: LieModule.iInf_lowerCentralSeries_eq_posFittingComp, LieSubmodule.lcs_sup, LieSubmodule.lowerCentralSeries_map_eq_lcs, LieModule.lowerCentralSeries, Codisjoint.eq_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
x : L
χ : L → R
⊢ Eq (α := LieSubmodule R L M)
    (LieSubmodule.map (M := ↥(genWeightSpaceOf M (χ x) x)) (LieSubmodule.incl (genWeightSpaceOf M (χ x) x))
      (genWeightSpace (↥(genWeightSpaceOf M (χ x) x)) χ))
    (genWeightSpace M χ)

Tactic:
simpa [map_genWeightSpace_eq_of_injective (genWeightSpaceOf M (χ x) x).injective_incl]
    using genWeightSpace_le_genWeightSpaceOf M x χ

Premises used: LieModule.genWeightSpaceOf, LieModule.genWeightSpace_le_genWeightSpaceOf, LieModule.map_genWeightSpace_eq_of_injective, LieSubmodule.injective_incl
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
x : L
⊢ IsCompl (α := LieSubmodule R L M) (genWeightSpaceOf M 0 x) (posFittingCompOf R M x)

Tactic:
simpa only [isCompl_iff, codisjoint_iff, disjoint_iff, ← LieSubmodule.toSubmodule_inj,
    LieSubmodule.sup_toSubmodule, LieSubmodule.inf_toSubmodule,
    LieSubmodule.top_toSubmodule, LieSubmodule.bot_toSubmodule, coe_genWeightSpaceOf_zero] using
    (toEnd R L M x).isCompl_iSup_ker_pow_iInf_range_pow

Premises used: LieSubmodule.bot_toSubmodule, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, codisjoint_iff, LieModule.coe_genWeightSpaceOf_zero, disjoint_iff, LieSubmodule.top_toSubmodule, isCompl_iff, LieSubmodule.toSubmodule_inj, LieSubmodule.sup_toSubmodule, LieModule.toEnd, DFunLike.coe, LieSubmodule.inf_toSubmodule
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
set :
  let M₀ : LieSubmodule R L M := genWeightSpace M 0;
  IsCompl M₀ (posFittingComp R L M)
⊢ IsCompl (α := LieSubmodule R L M) (genWeightSpace M 0) (posFittingComp R L M)

Tactic:
set M₀ := genWeightSpace M (0 : L → R)

Premises used: LieModule.genWeightSpace, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
set :
  let M₁ : LieSubmodule R L M := posFittingComp R L M;
  IsCompl M₀ M₁
⊢ IsCompl M₀ (posFittingComp R L M)

Tactic:
set M₁ := posFittingComp R L M

Premises used: LieModule.posFittingComp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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₁
inr : ∀ (x : L) (hx : Ne (α := LieSubmodule R L M) (genWeightSpaceOf M 0 x) ⊤), IsCompl M₀ M₁
⊢ 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 ≠ ⊤⟩

Premises used: LieModule.genWeightSpaceOf, forall_or_exists_not, Top.top, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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) ⊤
this : IsNilpotent L M
⊢ IsCompl M₀ M₁

Tactic:
simp [M₀, M₁, isCompl_top_bot]

Premises used: isCompl_top_bot
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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) ⊤
inl : IsNilpotent L M
⊢ IsCompl M₀ M₁

Tactic:
suffices IsNilpotent L M by simp [M₀, M₁, isCompl_top_bot]
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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) ⊤
⊢ M₀ = ⊤

Tactic:
simpa [M₀, genWeightSpace]

Premises used: LieModule.genWeightSpace