-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma posFittingComp_map_incl_sup_of_codisjoint [IsNoetherian R M] [IsArtinian R M]
    {N₁ N₂ : LieSubmodule R L M} (h : Codisjoint N₁ N₂) :
    (posFittingComp R L N₁).map N₁.incl ⊔ (posFittingComp R L N₂).map N₂.incl =
    posFittingComp R L M

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
⊢ 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)

Result:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) b ∧
      ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) b ∧
        ⨅ 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

Proof state:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) b ∧
      ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) b ∧
        ⨅ 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

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

Result:
case intro.intro.intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) b ∧
      ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) b ∧
        ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M b
hl₁ : ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) l
hl₂ : ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) l
hl₃ : ⨅ 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

Proof state:
case intro.intro.intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ b ≥ l,
    ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) b ∧
      ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) b ∧
        ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M b
hl₁ : ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) l
hl₂ : ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) l
hl₃ : ⨅ 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

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

Result:
no goals