awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
⊢ Submodule.map N.subtype (dx ^ (k + 1)).ker ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
have a : Submodule.map N.subtype (dx ^ (k + 1)).ker ≤ toSubmodule (engel R x)
Tactic: apply le_sup_of_le_left
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
⊢ Submodule.map N.subtype (dx ^ (k + 1)).ker ≤ toSubmodule (engel R x)
have a : (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype (toSubmodule (engel R x))
Tactic: rw [Submodule.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
hy : y ∈ (dx ^ (k + 1)).ker
⊢ y ∈ Submodule.comap N.subtype (toSubmodule (engel R x))
have a : ∃ (n : ℕ),
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L)
        ((N.subtype : (a : ↥N) → L) y : L) :
      L)
    (0 : L)
Tactic: simp only [Submodule.mem_comap, mem_engel_iff, mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
hy : y ∈ (dx ^ (k + 1)).ker
⊢ ∃ (n : ℕ),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L)
          ((N.subtype : (a : ↥N) → L) y : L) :
        L)
      (0 : L)
have h₁ : 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: use k + 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
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)
have h₁ : ∀ (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: revert hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
⊢ ∀ (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)
have 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)
Tactic: generalize k + 1 = k
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
⊢ ∀ (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)
have 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)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
    ((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)
have h₁ : Eq (α := L) ((N.subtype : (a : ↥N) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ N) val property) : L) (0 : L)
Tactic: simp only [pow_zero, Module.End.one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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 : ℕ
⊢ ∀ (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)
have 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)
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
Cleared hypotheses: y, k
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ ∀ (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)
have 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)
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
Cleared hypotheses: y, k
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
⊢ (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
have a : Submodule.map N.subtype (dx ^ (k + 1)).range ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
Tactic: rw [← Submodule.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
⊢ Submodule.map N.subtype (dx ^ (k + 1)).range ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
have a : Submodule.map N.subtype (dx ^ (k + 1)).range ≤ H.toSubmodule
Tactic: apply le_sup_of_le_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
⊢ Submodule.map N.subtype (dx ^ (k + 1)).range ≤ H.toSubmodule
have a : (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype H.toSubmodule
Tactic: rw [Submodule.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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 (α := ↥N) (Submodule.comap N.subtype H.toSubmodule) ((dx ^ (k + 1) : (a : ↥N) → ↥N) y : ↥N)
have a : Membership.mem (α := L) H ((N.subtype : (a : ↥N) → L) ((dx : (a : ↥N) → ↥N) ((dx ^ k : (a : ↥N) → ↥N) y) : ↥N) : L)
Tactic: simp only [pow_succ', Module.End.mul_apply, Submodule.mem_comap, mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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) H ((N.subtype : (a : ↥N) → L) ((dx : (a : ↥N) → ↥N) ((dx ^ k : (a : ↥N) → ↥N) y) : ↥N) : L)
have a : Membership.mem (α := L) N ((N.subtype : (a : ↥N.toSubmodule) → L) ((dx ^ k : (a : ↥N) → ↥N) y : ↥N) : L)
Tactic: apply aux₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
⊢ LieRing.IsNilpotent.{u_2} ↥H
have rw : ∀ (x : ↥H), _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)
Tactic: rw [LieAlgebra.isNilpotent_iff_forall (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)
have 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)
Tactic: let K : ℕ →o Submodule R H :=
    ⟨fun n ↦ LinearMap.ker ((ad R H x) ^ n), fun m n hmn ↦ ?mono⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (hypothesis)
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
⊢ 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))
      n)
    y
have 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)
Tactic: rw [LinearMap.mem_ker] at hy ⊢
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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' := ⋯ }
⊢ _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)
have 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)
Tactic: obtain ⟨n, hn⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance K
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ _root_.IsNilpotent (R := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H)
have h₁ : HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n = 0
have 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)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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
⊢ 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)
have 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)
Tactic: rw [coe_ad_pow]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (hypothesis)
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
⊢ 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)
have h₁ : Membership.mem (γ := LieSubalgebra R L) (engel R (↑x : L)) (↑y : L)
Tactic: specialize h x x.2 y.2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (hypothesis)
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)
⊢ 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)
have 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)
Tactic: rw [mem_engel_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨m, hm⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ 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)
have h : ∀ (hmn : m ≤ 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 : (a : ↥H) → ↥H) y) : L) : L)
Tactic: obtain (hmn | hmn) : m ≤ n ∨ n ≤ m := le_total m n