-- Mathlib/Algebra/Lie/Weights/Basic.lean
/-- This lemma exists only to simplify the proof of
`LieModule.isCompl_genWeightSpace_zero_posFittingComp`. -/
private lemma isCompl_genWeightSpace_zero_posFittingComp_aux
    (h : ∀ N < (⊤ : LieSubmodule R L M), IsCompl (genWeightSpace N 0) (posFittingComp R L N)) :
    IsCompl (genWeightSpace M 0) (posFittingComp R L M)

Proof state:
case inl
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
h✝ : ∀ N < ⊤, IsCompl (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), genWeightSpaceOf M 0 a = ⊤
⊢ IsNilpotent L M

Tactic:
replace h : M₀ = ⊤ := by simpa [M₀, genWeightSpace]

Result:
case inl
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
h✝ : ∀ N < ⊤, IsCompl (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

Proof state:
case inl
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
h✝ : ∀ N < ⊤, IsCompl (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

Tactic:
rw [← LieModule.isNilpotent_of_top_iff' (R := R), ← h]

Result:
case inl
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
h✝ : ∀ N < ⊤, IsCompl (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₀

Proof state:
case inr.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
h : ∀ N < ⊤, IsCompl (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₀ₓ ≠ ⊤
⊢ IsCompl M₀ M₁

Tactic:
set M₁ₓ := posFittingCompOf R M x

Result:
case inr.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
h : ∀ N < ⊤, IsCompl (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
⊢ IsCompl M₀ M₁

Proof state:
case inr.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
h : ∀ N < ⊤, IsCompl (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₁

Tactic:
have h₂ : IsCompl M₀ₓ₀ M₀ₓ₁ := h M₀ₓ hx.lt_top

Result:
case inr.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
h : ∀ N < ⊤, IsCompl (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₁

Proof state:
case inr.intro.hcomp
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
h : ∀ N < ⊤, IsCompl (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₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
⊢ IsCompl (LieSubmodule.map M₀ₓ.incl M₀ₓ₀ ⊔ LieSubmodule.map M₀ₓ.incl M₀ₓ₁) M₁ₓ

Tactic:
rwa [← LieSubmodule.map_sup, h₂.sup_eq_top, LieModuleHom.map_top, LieSubmodule.range_incl]

Result:
no goals