awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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'
⊢ LieModule.IsNilpotent.{u₂, u₄} (↥K') M
have hI₂ : R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (↑I : Submodule R ↥K') = ⊤
Tactic: have hI₂ : R ∙ (⟨x, hxK'⟩ : K') ⊔ LieSubmodule.toSubmodule I = ⊤ := by
    rw [← LieIdeal.toLieSubalgebra_toSubmodule R K' I, hI₁]
    apply Submodule.map_injective_of_injective (K' : Submodule R L).injective_subtype
    simp only [LieSubalgebra.coe_ofLe, Submodule.map_sup, Submodule.map_subtype_range_inclusion,
      Submodule.map_top, Submodule.range_subtype]
    rw [Submodule.map_subtype_span_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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') = ⊤
⊢ LieModule.IsNilpotent.{u₂, u₄} (↥K') M
have have : ∀ (e : ↥K ≃ₗ⁅R⁆ ↥I), LieModule.IsNilpotent.{u₂, u₄} (↥K') M
Tactic: have e : K ≃ₗ⁅R⁆ I :=
    (LieSubalgebra.equivOfLe hKK').trans
      (LieEquiv.ofEq _ _ ((LieSubalgebra.coe_set_eq _ _).mpr hI₁.symm))
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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
⊢ LieModule.IsNilpotent.{u₂, u₄} (↥K') M
have hI₃ : IsEngelian.{u₁, u₂, u₄} R ↥I
Tactic: have hI₃ : LieAlgebra.IsEngelian R I := e.isEngelian_iff.mp hK₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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)
⊢ LieModule.IsNilpotent L M
have rw : LieModule.IsNilpotent (↥(LieHom.range (toEnd R L M))) M
Tactic: rw [← isNilpotent_range_toEnd_iff R]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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)
⊢ LieModule.IsNilpotent (↥(LieHom.range (toEnd R L M))) M
have h₁ : ∀ (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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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}
⊢ LieModule.IsNilpotent (↥L') M
have hs : s.Nonempty
Tactic: have hs : s.Nonempty := ⟨⊥, LieAlgebra.isEngelian_of_subsingleton⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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
⊢ LieModule.IsNilpotent (↥L') M
have rw : LieModule.IsNilpotent (↥⊤) M
Tactic: rw [← isNilpotent_of_top_iff (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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
⊢ LieModule.IsNilpotent (↥⊤) M
have apply : ∀ (x : ↥⊤), IsNilpotent (R := Module.End R M) ((toEnd R (↥⊤) M : (a : ↥⊤) → Module.End R M) x : Module.End R M)
Tactic: apply this M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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
⊢ LieModule.IsNilpotent (↥L') M
have suffices : ⊤ ∈ s
Tactic: suffices ⊤ ∈ s by
    rw [← isNilpotent_of_top_iff (R := R)]
    apply this M
    simp [LieSubalgebra.toEnd_eq, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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' ∈ s, K < K'
have apply : K < K.normalizer
Tactic: apply LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer hK₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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 < K.normalizer
have apply : K ≠ K.normalizer
Tactic: apply lt_of_le_of_ne K.le_normalizer
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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 ≠ K.normalizer
have rw : Nontrivial.{u_1} ↥(maxTrivSubmodule R (↥K) (↥L' ⧸ K.toLieSubmodule))
Tactic: rw [Ne, eq_comm, K.normalizer_eq_self_iff, ← Ne, ←
      LieSubmodule.nontrivial_iff_ne_bot R K]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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} ↥(maxTrivSubmodule R (↥K) (↥L' ⧸ K.toLieSubmodule))
have this : Nontrivial.{u_1} (↥L' ⧸ K.toLieSubmodule)
Tactic: have : Nontrivial (L' ⧸ K.toLieSubmodule) := Submodule.Quotient.nontrivial_iff.2 <| by simpa
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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)
have 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))
Tactic: refine hK₁ _ fun x => ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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' ⧸ K.toLieSubmodule))
    ((toEnd R (↥K) (↥L' ⧸ K.toLieSubmodule) : (a : ↥K) → Module.End R (↥L' ⧸ K.toLieSubmodule)) x :
      Module.End R (↥L' ⧸ K.toLieSubmodule))
have hx : 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)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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')
⊢ 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))
have 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')
Tactic: apply Module.End.IsNilpotent.mapQ ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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')
⊢ 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
have HX₁ : X ∈ K
Tactic: simp only [LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.mem_toSubmodule] at HX
Cleared hypotheses: HX
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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
⊢ 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
have simp : ⁅(↑x : ↥L'), X⁆ ∈ K
Tactic: simp only [LieSubalgebra.coe_toLieSubmodule, Submodule.mem_comap, ad_apply,
        LieSubalgebra.mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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)
⊢ Nontrivial.{u_1} ↥(maxTrivSubmodule R (↥K) (↥L' ⧸ K.toLieSubmodule))
have this₁ : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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
⊢ ⊤ ∈ s
have this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
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) := Submodule.Quotient.nontrivial_iff.2 <| by simpa
    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)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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 : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ IsNoetherian.{u₁, u_1} R ↥L'
have refine : Eq (α := Submodule R ↥L') (LinearMap.range (↑(LieHom.rangeRestrict (toEnd R L M)) : L →ₗ[R] ↥(toEnd R L M).range)) ⊤
Tactic: refine isNoetherian_of_surjective (LieHom.rangeRestrict (toEnd R L M)).toLinearMap ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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 : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ Eq (α := Submodule R ↥L') (LinearMap.range (↑(LieHom.rangeRestrict (toEnd R L M)) : L →ₗ[R] ↥(toEnd R L M).range)) ⊤
have simp : Function.Surjective.{u₂ + 1, u_1 + 1} (α := L) (β := ↥L')
  (⇑(↑(LieHom.rangeRestrict (toEnd R L M)) : L →ₗ[R] ↥(toEnd R L M).range) : (a : L) → ↥L')
Tactic: simp only [LinearMap.range_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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 : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ ⊤ ∈ s
have _i5 : IsNoetherian.{u₁, u_1} R ↥L'
Tactic: haveI _i5 : IsNoetherian R L' := by
    refine isNoetherian_of_surjective (LieHom.rangeRestrict (toEnd R L M)).toLinearMap ?_
    simp only [LinearMap.range_eq_top]
    exact LieHom.surjective_rangeRestrict (toEnd R L M)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
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 : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian.{u₁, u_1} R ↥L'
⊢ ⊤ ∈ s
have obtain : ∀ (K : LieSubalgebra R ↥L') (hK₁ : K ∈ s) (hK₂ : ∀ x ∈ s, ¬K < x), ⊤ ∈ s
Tactic: obtain ⟨K, hK₁, hK₂⟩ := (LieSubalgebra.wellFoundedGT_of_noetherian R L').wf.has_min s hs
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
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 : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian.{u₁, u_1} R ↥L'
K : LieSubalgebra R ↥L'
hK₁ : K ∈ s
hK₂ : ∀ x ∈ s, ¬K < x
hK₃ : ⊤ ∈ s
⊢ ⊤ ∈ s
have hK₄ : ∀ x ∈ s, ¬⊤ < x
Tactic: obtain rfl : K = ⊤ := by grind
Cleared hypotheses: K, hK₁, hK₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
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 : IsNoetherian R M
⊢ IsNilpotent L M ↔
    ∀ (x : L),
      _root_.IsNilpotent.{u₄} (R := Module.End R M)
        (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
have rw : (∀ (x : ↥(LieHom.range (toEnd R L M))),
    _root_.IsNilpotent (R := Module.End R M)
      ((toEnd R (↥(LieHom.range (toEnd R L M))) M : (a : ↥(toEnd R L M).range) → Module.End R M) x : Module.End R M)) ↔
  ∀ (x : L),
    _root_.IsNilpotent.{u₄} (R := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
Tactic: rw [← isNilpotent_range_toEnd_iff (R := R), LieModule.isNilpotent_iff_forall (R := R)]