awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
y : ↥N
h₁ :
  ∀ (k : ℕ) (hy : y ∈ (dx ^ k).ker),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) k : (a : L) → L)
          ((N.subtype : (a : ↥N) → L) y : L) :
        L)
      (0 : L)
⊢ ∀ (hy : y ∈ (dx ^ (k + 1)).ker),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (k + 1) : (a : L) → L)
          ((N.subtype : (a : ↥N) → L) y : L) :
        L)
      (0 : L)

Tactic:
generalize k + 1 = k
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
y : ↥N
h₁ :
  ∀ (val : L) (property : val ∈ N)
    (hy : Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property ∈ (HPow.hPow (β := ℕ) dx 0).ker),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) (β := ℕ) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) 0 :
            (a : L) → L)
          ((N.subtype : (a : ↥N) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property) : L) :
        L)
      (0 : L)
⊢ ∀ (hy : y ∈ (HPow.hPow (β := ℕ) dx 0).ker),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) (β := ℕ) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) 0 :
            (a : L) → L)
          ((N.subtype : (a : ↥N) → L) y : L) :
        L)
      (0 : L)

Tactic:
cases y
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
val : L
property : val ∈ N
hy : Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property ∈ (HPow.hPow (β := ℕ) dx 0).ker
h₁ : Eq (α := L) ((N.subtype : (a : ↥N) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property) : L) (0 : L)
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) (β := ℕ) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) 0 : (a : L) → L)
        ((N.subtype : (a : ↥N) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property) : L) :
      L)
    (0 : L)

Tactic:
simp only [pow_zero, Module.End.one_apply]

Premises used: pow_zero, Module.End.one_apply
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
val : L
property : val ∈ N
hy : Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property ∈ (HPow.hPow (β := ℕ) dx 0).ker
⊢ Eq (α := L) ((N.subtype : (a : ↥N) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property) : L) (0 : L)

Tactic:
(AddSubmonoid.mk_eq_zero N.toAddSubmonoid).mp hy

Premises used: Submodule.toAddSubmonoid, Iff.mp, AddSubmonoid.mk_eq_zero, LieSubalgebra.toSubmodule
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
val : L
property : val ∈ N
hy : Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property ∈ (HPow.hPow (β := ℕ) dx 0).ker
⊢ Eq (α := L) ((N.subtype : (a : ↥N) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property) : L) (0 : L)

Tactic:
exact (AddSubmonoid.mk_eq_zero N.toAddSubmonoid).mp hy

Premises used: Submodule.toAddSubmonoid, Iff.mp, AddSubmonoid.mk_eq_zero, LieSubalgebra.toSubmodule
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k_1 k : ℕ
ih :
  ∀ ⦃y : ↥N⦄ (hy : y ∈ (dx ^ k).ker),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) k : (a : L) → L)
          ((N.subtype : (a : ↥N) → L) y : L) :
        L)
      (0 : L)
y : ↥N
⊢ ∀ (hy : y ∈ (dx ^ (k + 1)).ker),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (k + 1) : (a : L) → L)
          ((N.subtype : (a : ↥N) → L) y : L) :
        L)
      (0 : L)

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k_1 : ℕ
y : ↥N
k : ℕ
h₁ :
  ∀ ⦃y : ↥N⦄ (hy : y ∈ (HPow.hPow (β := ℕ) dx 0).ker),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) (β := ℕ) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) 0 :
            (a : L) → L)
          ((N.subtype : (a : ↥N) → L) y : L) :
        L)
      (0 : L)
h₂ :
  ∀ (k : ℕ)
    (ih :
      ∀ ⦃y : ↥N⦄ (hy : y ∈ (dx ^ k).ker),
        Eq (α := L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) k : (a : L) → L)
              ((N.subtype : (a : ↥N) → L) y : L) :
            L)
          (0 : L))
    ⦃y : ↥N⦄ (hy : y ∈ (dx ^ (k + 1)).ker),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (k + 1) : (a : L) → L)
          ((N.subtype : (a : ↥N) → L) y : L) :
        L)
      (0 : L)
⊢ ∀ (hy : y ∈ (dx ^ k).ker),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) k : (a : L) → L)
          ((N.subtype : (a : ↥N) → L) y : L) :
        L)
      (0 : L)

Tactic:
induction k generalizing y with
    | zero =>
      cases y; intro hy; simp only [pow_zero, Module.End.one_apply]
      exact (AddSubmonoid.mk_eq_zero N.toAddSubmonoid).mp hy
    | succ k ih => solve_by_elim

Premises used: pow_zero, Module.End.one_apply
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
a : Submodule.map N.subtype (dx ^ (k + 1)).range ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
⊢ (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)

Tactic:
rw [← Submodule.map_le_iff_le_comap]

Premises used: Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
a : Submodule.map N.subtype (dx ^ (k + 1)).range ≤ H.toSubmodule
⊢ Submodule.map N.subtype (dx ^ (k + 1)).range ≤ toSubmodule (engel R x) ⊔ H.toSubmodule

Tactic:
apply le_sup_of_le_right

Premises used: le_sup_of_le_right
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
a : (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype H.toSubmodule
⊢ Submodule.map N.subtype (dx ^ (k + 1)).range ≤ H.toSubmodule

Tactic:
rw [Submodule.map_le_iff_le_comap]

Premises used: Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
a : Membership.mem (α := L) H ((N.subtype : (a : ↥N) → L) ((dx : (a : ↥N) → ↥N) ((dx ^ k : (a : ↥N) → ↥N) y) : ↥N) : L)
⊢ Membership.mem (α := ↥N) (Submodule.comap N.subtype H.toSubmodule) ((dx ^ (k + 1) : (a : ↥N) → ↥N) y : ↥N)

Tactic:
simp only [pow_succ', Module.End.mul_apply, Submodule.mem_comap, mem_toSubmodule]

Premises used: LieSubalgebra.mem_toSubmodule, Submodule.mem_comap, Module.End.mul_apply, pow_succ'
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
a : Membership.mem (α := L) N ((N.subtype : (a : ↥N.toSubmodule) → L) ((dx ^ k : (a : ↥N) → ↥N) y : ↥N) : L)
⊢ Membership.mem (α := L) H ((N.subtype : (a : ↥N) → L) ((dx : (a : ↥N) → ↥N) ((dx ^ k : (a : ↥N) → ↥N) y) : ↥N) : L)

Tactic:
apply aux₁
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L : (a : L) → Module.End R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
⊢ Membership.mem (α := L) N ((N.subtype : (a : ↥N.toSubmodule) → L) ((dx ^ k : (a : ↥N) → ↥N) y : ↥N) : L)

Tactic:
simp only [Submodule.coe_subtype, SetLike.coe_mem]

Premises used: SetLike.coe_mem, Submodule.coe_subtype
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
rw : ∀ (x : ↥H), _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)
⊢ LieRing.IsNilpotent.{u_2} ↥H

Tactic:
rw [LieAlgebra.isNilpotent_iff_forall (R := R)]

Premises used: LieAlgebra.isNilpotent_iff_forall
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
let : _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)
let₁ :
  ∀ (m n : ℕ) (hmn : m ≤ n),
    LE.le.{u_2} (α := Submodule R ↥H)
      ((fun (n : ℕ) ↦
          LinearMap.ker
            (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n))
        m)
      ((fun (n : ℕ) ↦
          LinearMap.ker
            (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n))
        n)
⊢ _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)

Tactic:
let K : ℕ →o Submodule R H :=
    ⟨fun n ↦ LinearMap.ker ((ad R H x) ^ n), fun m n hmn ↦ ?mono⟩
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
y : ↥H
hy :
  Membership.mem (γ := Submodule R ↥H)
    ((fun (n : ℕ) ↦
        LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n))
      m)
    y
⊢ Eq (α := ↥H)
    ((HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) m : (a : ↥H) → ↥H)
        y :
      ↥H)
    (0 : ↥H)

Tactic:
rw [LinearMap.mem_ker] at hy ⊢

Premises used: LinearMap.mem_ker
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
y : ↥H
hy :
  Eq (α := ↥H)
    ((HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) m : (a : ↥H) → ↥H)
        y :
      ↥H)
    (0 : ↥H)
⊢ Eq (α := ↥H)
    ((HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n : (a : ↥H) → ↥H)
        y :
      ↥H)
    (0 : ↥H)

Tactic:
Module.End.pow_map_zero_of_le hmn hy

Premises used: Module.End.pow_map_zero_of_le
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
y : ↥H
hy :
  Eq (α := ↥H)
    ((HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) m : (a : ↥H) → ↥H)
        y :
      ↥H)
    (0 : ↥H)
⊢ Eq (α := ↥H)
    ((HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n : (a : ↥H) → ↥H)
        y :
      ↥H)
    (0 : ↥H)

Tactic:
exact Module.End.pow_map_zero_of_le hmn hy

Premises used: Module.End.pow_map_zero_of_le
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
⊢ LE.le.{u_2} (α := Submodule R ↥H)
    ((fun (n : ℕ) ↦
        LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n))
      m)
    ((fun (n : ℕ) ↦
        LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n))
      n)

Tactic:
case mono =>
    intro y hy
    rw [LinearMap.mem_ker] at hy ⊢
    exact Module.End.pow_map_zero_of_le hmn hy

Premises used: LinearMap.mem_ker
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
obtain :
  ∀ (n : ℕ)
    (hn :
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
            ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)),
    _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)
⊢ _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)

Tactic:
obtain ⟨n, hn⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance K

Premises used: Iff.mpr, inferInstance, monotone_stabilizes_iff_noetherian
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
h₁ : HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n = 0
⊢ _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)

Tactic:
use n
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
h₁ :
  ∀ (y : ↥H),
    Eq.{u_2 + 1} (α := L)
      (↑((HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n :
              (a : ↥H) → ↥H)
            y) :
        L)
      (↑((0 : (a : ↥H) → ↥H) y) : L)
⊢ HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n = 0

Tactic:
ext y
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
h₁ :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
⊢ Eq.{u_2 + 1} (α := L)
    (↑((HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n : (a : ↥H) → ↥H)
          y) :
      L)
    (↑((0 : (a : ↥H) → ↥H) y) : L)

Tactic:
rw [coe_ad_pow]

Premises used: LieSubalgebra.coe_ad_pow
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R (↑x : L)) (↑y : L)

Tactic:
specialize h x x.2 y.2

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
h : Membership.mem (γ := LieSubalgebra R L) (engel R (↑x : L)) (↑y : L)
⊢ ∃ (n : ℕ),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      (0 : L)

Tactic:
rw [mem_engel_iff] at h

Premises used: LieSubalgebra.mem_engel_iff
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
h :
  ∃ (n : ℕ),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      (0 : L)
h₁ :
  ∀ (m : ℕ)
    (hm :
      Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m :
              (a : L) → L)
            (↑y : L) :
          L)
        (0 : L)),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)

Tactic:
obtain ⟨m, hm⟩ := h
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
⊢ m ≤ n ∨ n ≤ m

Tactic:
le_total m n

Premises used: le_total