-- Mathlib/Algebra/Lie/Engel.lean
theorem LieAlgebra.isEngelian_of_isNoetherian [IsNoetherian R L] : LieAlgebra.IsEngelian R L

Proof state:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
⊢ ⊤ ∈ s

Tactic:
have : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K' := by
  rintro K (hK₁ : LieAlgebra.IsEngelian R K) hK₂
  apply LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer hK₁
  apply lt_of_le_of_ne K.le_normalizer
  rw [Ne, eq_comm, K.normalizer_eq_self_iff, ← Ne, ←
    LieSubmodule.nontrivial_iff_ne_bot R K]
  have : Nontrivial (L' ⧸ K.toLieSubmodule) := by
    replace hK₂ : K.toLieSubmodule ≠ ⊤ := by
      rwa [Ne, ← LieSubmodule.toSubmodule_inj, K.coe_toLieSubmodule,
        LieSubmodule.top_toSubmodule, ← LieSubalgebra.top_toSubmodule,
        K.toSubmodule_inj]
    exact Submodule.Quotient.nontrivial_of_lt_top _ hK₂.lt_top
  have : LieModule.IsNilpotent K (L' ⧸ K.toLieSubmodule) := by
    refine hK₁ _ fun x => ?_
    have hx := LieAlgebra.isNilpotent_ad_of_isNilpotent (h x)
    apply Module.End.IsNilpotent.mapQ ?_ hx
    intro X HX
    simp only [LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.mem_toSubmodule] at HX
    simp only [LieSubalgebra.coe_toLieSubmodule, Submodule.mem_comap, ad_apply,
      LieSubalgebra.mem_toSubmodule]
    exact LieSubalgebra.lie_mem K x.prop HX
  exact nontrivial_max_triv_of_isNilpotent R K (L' ⧸ K.toLieSubmodule)

Result:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ ⊤ ∈ s

Proof state:
case intro.intro
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian R ↥L'
K : LieSubalgebra R ↥L'
hK₁ : K ∈ s
hK₂ : ∀ x ∈ s, ¬x > K
hK₃ : K = ⊤
⊢ ⊤ ∈ s

Tactic:
exact hK₃ ▸ hK₁

Result:
no goals

Proof state:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent ((ad R ↥L') ↑x)
X : ↥L'
HX : X ∈ ↑K.toLieSubmodule
⊢ X ∈ Submodule.comap ((ad R ↥L') ↑x) ↑K.toLieSubmodule

Tactic:
simp only [LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.mem_toSubmodule] at HX

Result:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent ((ad R ↥L') ↑x)
X : ↥L'
HX : X ∈ K
⊢ X ∈ Submodule.comap ((ad R ↥L') ↑x) ↑K.toLieSubmodule

Proof state:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
h : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
⊢ LieModule.IsNilpotent (↥(toEnd R L M).range) M

Tactic:
replace h : ∀ y : L', _root_.IsNilpotent (y : Module.End R M) := by
  rintro ⟨-, ⟨y, rfl⟩⟩
  simp [h]

Result:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
⊢ LieModule.IsNilpotent (↥(toEnd R L M).range) M

Proof state:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
⊢ K.toLieSubmodule ≠ ⊤

Tactic:
rwa [Ne, ← LieSubmodule.toSubmodule_inj, K.coe_toLieSubmodule,
  LieSubmodule.top_toSubmodule, ← LieSubalgebra.top_toSubmodule,
  K.toSubmodule_inj]

Result:
no goals

Proof state:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
⊢ LieModule.IsNilpotent (↥L') M

Tactic:
suffices ⊤ ∈ s by
  rw [← isNilpotent_of_top_iff (R := R)]
  apply this M
  simp [LieSubalgebra.toEnd_eq, h]

Result:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
⊢ ⊤ ∈ s

Proof state:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent ((ad R ↥L') ↑x)
⊢ ↑K.toLieSubmodule ≤ Submodule.comap ((ad R ↥L') ↑x) ↑K.toLieSubmodule

Tactic:
intro X HX

Result:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent ((ad R ↥L') ↑x)
X : ↥L'
HX : X ∈ ↑K.toLieSubmodule
⊢ X ∈ Submodule.comap ((ad R ↥L') ↑x) ↑K.toLieSubmodule