awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule.{u₂, u₄} (↥K') M
_i4 : LieModule.{u₁, u₂, u₄} R (↥K') M
h :
  ∀ (x : ↥K'),
    IsNilpotent.{u₄} (R := Module.End R M) ((toEnd R (↥K') M : (a : ↥K') → Module.End R M) x : Module.End R M)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
hI₂ : R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (↑I : Submodule R ↥K') = ⊤
e : ↥K ≃ₗ⁅R⁆ ↥I
⊢ IsEngelian.{u₁, u₂, u₄} R ↥I

Tactic:
have hI₃ : LieAlgebra.IsEngelian R I := e.isEngelian_iff.mp hK₁
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule.{u₂, u₄} (↥K') M
_i4 : LieModule.{u₁, u₂, u₄} R (↥K') M
h :
  ∀ (x : ↥K'),
    IsNilpotent.{u₄} (R := Module.End R M) ((toEnd R (↥K') M : (a : ↥K') → Module.End R M) x : Module.End R M)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
hI₂ : R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (↑I : Submodule R ↥K') = ⊤
e : ↥K ≃ₗ⁅R⁆ ↥I
hI₃ : IsEngelian.{u₁, u₂, u₄} R ↥I
⊢ LieModule.IsNilpotent.{u₂, u₄} (↥K') M

Tactic:
LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop hI₂ (h _) (hI₃ _ fun x => h x)

Premises used: LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop, Subtype.val
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule.{u₂, u₄} (↥K') M
_i4 : LieModule.{u₁, u₂, u₄} R (↥K') M
h :
  ∀ (x : ↥K'),
    IsNilpotent.{u₄} (R := Module.End R M) ((toEnd R (↥K') M : (a : ↥K') → Module.End R M) x : Module.End R M)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
hI₂ : R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (↑I : Submodule R ↥K') = ⊤
e : ↥K ≃ₗ⁅R⁆ ↥I
hI₃ : IsEngelian.{u₁, u₂, u₄} R ↥I
⊢ LieModule.IsNilpotent.{u₂, u₄} (↥K') M

Tactic:
exact LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop hI₂ (h _) (hI₃ _ fun x => h x)

Premises used: LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop, Subtype.val
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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.{u_1} (R := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u_1} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
rw : LieModule.IsNilpotent (↥(LieHom.range (toEnd R L M))) M
⊢ LieModule.IsNilpotent L M

Tactic:
rw [← isNilpotent_range_toEnd_iff R]

Premises used: LieModule.isNilpotent_range_toEnd_iff
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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.{u_1} (R := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u_1} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
y : L
⊢ IsNilpotent.{u_1} (R := Module.End R M)
    ((↑(Subtype.mk (p := fun (x : Module.End R M) ↦ x ∈ L')
            ((((↑(toEnd R L M) : LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) L (Module.End R M)) :
                  LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) L (Module.End R M)) :
                (a : L) → Module.End R M)
              y)
            ⋯) :
        Module.End R M) :
      Module.End R M)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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.{u_1} (R := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u_1} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
⊢ ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)

Tactic:
replace h : ∀ y : L', IsNilpotent (y : Module.End R M) := by
    rintro ⟨-, ⟨y, rfl⟩⟩
    simp [h]
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
change : LieModule.IsNilpotent (↥L') M
⊢ LieModule.IsNilpotent (↥(LieHom.range (toEnd R L M))) M

Tactic:
change LieModule.IsNilpotent L' M

Premises used: Membership.mem, Subtype, LieModule.IsNilpotent
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
⊢ s.Nonempty

Tactic:
have hs : s.Nonempty := ⟨⊥, LieAlgebra.isEngelian_of_subsingleton⟩
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ⊤ ∈ s
rw : LieModule.IsNilpotent (↥⊤) M
⊢ LieModule.IsNilpotent (↥L') M

Tactic:
rw [← isNilpotent_of_top_iff (R := R)]

Premises used: LieModule.isNilpotent_of_top_iff
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ⊤ ∈ s
apply : ∀ (x : ↥⊤), IsNilpotent (R := Module.End R M) ((toEnd R (↥⊤) M : (a : ↥⊤) → Module.End R M) x : Module.End R M)
⊢ LieModule.IsNilpotent (↥⊤) M

Tactic:
apply this M
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ⊤ ∈ s
⊢ ∀ (x : ↥⊤), IsNilpotent (R := Module.End R M) ((toEnd R (↥⊤) M : (a : ↥⊤) → Module.End R M) x : Module.End R M)

Tactic:
simp [LieSubalgebra.toEnd_eq, h]

Premises used: LieSubalgebra.toEnd_eq
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
suffices : ⊤ ∈ s
⊢ LieModule.IsNilpotent (↥L') M

Tactic:
suffices ⊤ ∈ s by
    rw [← isNilpotent_of_top_iff (R := R)]
    apply this M
    simp [LieSubalgebra.toEnd_eq, h]
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
apply : K < K.normalizer
⊢ ∃ K' ∈ s, K < K'

Tactic:
apply LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer hK₁

Premises used: LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
apply : K ≠ K.normalizer
⊢ K < K.normalizer

Tactic:
apply lt_of_le_of_ne K.le_normalizer

Premises used: LieSubalgebra.le_normalizer, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
rw : Nontrivial.{u_1} ↥(maxTrivSubmodule R (↥K) (↥L' ⧸ K.toLieSubmodule))
⊢ K ≠ K.normalizer

Tactic:
rw [Ne, eq_comm, K.normalizer_eq_self_iff, ← Ne, ←
      LieSubmodule.nontrivial_iff_ne_bot R K]

Premises used: Membership.mem, Subtype, Ne, eq_comm, LieSubalgebra.normalizer_eq_self_iff, LieSubmodule.nontrivial_iff_ne_bot
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
⊢ (↑K.toLieSubmodule : Submodule R ↥L') ≠ ⊤

Tactic:
simpa
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
⊢ Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)

Tactic:
have : Nontrivial (L' ⧸ K.toLieSubmodule) := Submodule.Quotient.nontrivial_iff.2 <| by simpa
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
⊢ LieModule.IsNilpotent.{u_1, u_1} (↥K) (↥L' ⧸ K.toLieSubmodule)

Tactic:
hK₁ _ fun x => ?_
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
refine :
  ∀ (x : ↥K),
    IsNilpotent (R := Module.End R (↥L' ⧸ K.toLieSubmodule))
      ((toEnd R (↥K) (↥L' ⧸ K.toLieSubmodule) : (a : ↥K) → Module.End R (↥L' ⧸ K.toLieSubmodule)) x :
        Module.End R (↥L' ⧸ K.toLieSubmodule))
⊢ LieModule.IsNilpotent.{u_1, u_1} (↥K) (↥L' ⧸ K.toLieSubmodule)

Tactic:
refine hK₁ _ fun x => ?_
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
x : ↥K
⊢ IsNilpotent (R := Module.End R ↥L') ((ad R ↥L' : (a : ↥L') → Module.End R ↥L') (↑x : ↥L') : Module.End R ↥L')

Tactic:
have hx := LieAlgebra.isNilpotent_ad_of_isNilpotent (h x)
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent (R := Module.End R ↥L') ((ad R ↥L' : (a : ↥L') → Module.End R ↥L') (↑x : ↥L') : Module.End R ↥L')
apply :
  (↑K.toLieSubmodule : Submodule R ↥L') ≤
    Submodule.comap (σ₁₂ := RingHom.id R) ((ad R ↥L' : (a : ↥L') → Module.End R ↥L') (↑x : ↥L'))
      (↑K.toLieSubmodule : Submodule R ↥L')
⊢ IsNilpotent (R := Module.End R (↥L' ⧸ K.toLieSubmodule))
    ((toEnd R (↥K) (↥L' ⧸ K.toLieSubmodule) : (a : ↥K) → Module.End R (↥L' ⧸ K.toLieSubmodule)) x :
      Module.End R (↥L' ⧸ K.toLieSubmodule))

Tactic:
apply Module.End.IsNilpotent.mapQ ?_ hx

Premises used: Module.End.IsNilpotent.mapQ
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent (R := Module.End R ↥L') ((ad R ↥L' : (a : ↥L') → Module.End R ↥L') (↑x : ↥L') : Module.End R ↥L')
X : ↥L'
HX : X ∈ (↑K.toLieSubmodule : Submodule R ↥L')
⊢ X ∈ K

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

Premises used: LieSubalgebra.mem_toSubmodule, LieSubalgebra.coe_toLieSubmodule
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent (R := Module.End R ↥L') ((ad R ↥L' : (a : ↥L') → Module.End R ↥L') (↑x : ↥L') : Module.End R ↥L')
X : ↥L'
HX : X ∈ K
simp : ⁅(↑x : ↥L'), X⁆ ∈ K
⊢ Membership.mem (γ := Submodule R ↥L')
    (Submodule.comap (σ₁₂ := RingHom.id R) ((ad R ↥L' : (a : ↥L') → Module.End R ↥L') (↑x : ↥L'))
      (↑K.toLieSubmodule : Submodule R ↥L'))
    X

Tactic:
simp only [LieSubalgebra.coe_toLieSubmodule, Submodule.mem_comap, ad_apply,
        LieSubalgebra.mem_toSubmodule]

Premises used: LieSubalgebra.mem_toSubmodule, Submodule.mem_comap, LieAlgebra.ad_apply, LieSubalgebra.coe_toLieSubmodule
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent (R := Module.End R ↥L') ((ad R ↥L' : (a : ↥L') → Module.End R ↥L') (↑x : ↥L') : Module.End R ↥L')
X : ↥L'
HX : X ∈ K
⊢ ⁅(↑x : ↥L'), X⁆ ∈ K

Tactic:
LieSubalgebra.lie_mem K x.prop HX

Premises used: Subtype.prop, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent (R := Module.End R ↥L') ((ad R ↥L' : (a : ↥L') → Module.End R ↥L') (↑x : ↥L') : Module.End R ↥L')
X : ↥L'
HX : X ∈ K
⊢ ⁅(↑x : ↥L'), X⁆ ∈ K

Tactic:
exact LieSubalgebra.lie_mem K x.prop HX

Premises used: Subtype.prop, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
⊢ LieModule.IsNilpotent.{u_1, u_1} (↥K) (↥L' ⧸ K.toLieSubmodule)

Tactic:
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
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this_1 : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
this : LieModule.IsNilpotent.{u_1, u_1} (↥K) (↥L' ⧸ K.toLieSubmodule)
⊢ Nontrivial.{u_1} ↥(maxTrivSubmodule R (↥K) (↥L' ⧸ K.toLieSubmodule))

Tactic:
nontrivial_max_triv_of_isNilpotent R K (L' ⧸ K.toLieSubmodule)

Premises used: LieModule.nontrivial_max_triv_of_isNilpotent, Membership.mem, Subtype, HasQuotient.Quotient, LieSubalgebra.toLieSubmodule
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : 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) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian.{u₁, u_1, u_1} R ↥K
hK₂ : K ≠ ⊤
this_1 : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
this : LieModule.IsNilpotent.{u_1, u_1} (↥K) (↥L' ⧸ K.toLieSubmodule)
⊢ Nontrivial.{u_1} ↥(maxTrivSubmodule R (↥K) (↥L' ⧸ K.toLieSubmodule))

Tactic:
exact nontrivial_max_triv_of_isNilpotent R K (L' ⧸ K.toLieSubmodule)

Premises used: LieModule.nontrivial_max_triv_of_isNilpotent, Membership.mem, Subtype, HasQuotient.Quotient, LieSubalgebra.toLieSubmodule