awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) m : (a : L) → L) y : L)
    (0 : L)
n : ℕ
hn :
  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) z : L)
    (0 : L)
ij : ℕ × ℕ
hij : ij ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n)
h : m ≤ ij.1
⊢ HSMul.hSMul (β := L) ((m + n).choose ij.1)
      (Bracket.bracket (L := L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 : (a : L) → L)
              y :
            L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.2 : (a : L) → L)
            z) :
        L) =
    0

Tactic:
simp [Module.End.pow_map_zero_of_le h, hm, hn]

Premises used: Module.End.pow_map_zero_of_le
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) m : (a : L) → L) y : L)
    (0 : L)
n : ℕ
hn :
  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) z : L)
    (0 : L)
ij : ℕ × ℕ
hij : ij ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n)
h : n ≤ ij.2
⊢ HSMul.hSMul (β := L) ((m + n).choose ij.1)
      (Bracket.bracket (L := L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 : (a : L) → L)
              y :
            L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.2 : (a : L) → L)
            z) :
        L) =
    0

Tactic:
simp [Module.End.pow_map_zero_of_le h, hm, hn]

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
x y : L
⊢ (∃ (k : ℕ),
      Eq (α := L)
        ((HSub.hSub (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L)
                  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := Module.End R L) 0 1) ^
                k :
              (a : L) → L)
            y :
          L)
        (0 : L)) ↔
    ∃ (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) y :
          L)
        (0 : L)

Tactic:
simp only [zero_smul, sub_zero]

Premises used: sub_zero, zero_smul
-- 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
x : L
simp :
  ∃ (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) x : L)
      (0 : L)
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R x) x

Tactic:
simp only [mem_engel_iff]

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
x : L
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) (β := ℕ) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) 1 : (a : L) → L)
        x :
      L)
    (0 : L)

Tactic:
simp
-- 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
x : L
⊢ ∃ (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) x : L)
      (0 : L)

Tactic:
exact ⟨1, by simp⟩
-- 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
rw : LE.le.{u_2} (α := LieSubalgebra R L) ⊤ (engel R 0)
⊢ Eq.{u_2 + 1} (α := LieSubalgebra R L) (engel R 0) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_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
x : L
rw : ∃ (n : ℕ), Eq (α := L) ((HPow.hPow (α := Module.End R L) 0 n : (a : L) → L) x : L) (0 : L)
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R 0) x

Tactic:
rw [mem_engel_iff, map_zero]

Premises used: map_zero, 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
x : L
h : Eq (α := L) ((HPow.hPow (α := Module.End R L) (β := ℕ) 0 1 : (a : L) → L) x : L) (0 : L)
⊢ ∃ (n : ℕ), Eq (α := L) ((HPow.hPow (α := Module.End R L) 0 n : (a : L) → L) x : L) (0 : L)

Tactic:
use 1
-- 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
x : L
⊢ Eq (α := L) ((HPow.hPow (α := Module.End R L) (β := ℕ) 0 1 : (a : L) → L) x : L) (0 : L)

Tactic:
simp only [pow_one, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, pow_one
-- 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
x : L
apply : LE.le (α := LieSubalgebra R L) (normalizer (engel R x)) (engel R x)
⊢ Eq (α := LieSubalgebra R L) (normalizer (engel R x)) (engel R x)

Tactic:
apply le_antisymm _ (le_normalizer _)

Premises used: LieSubalgebra.le_normalizer, le_antisymm
-- 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
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (normalizer (engel R x)) y
⊢ ∀ (y_1 : L),
    Membership.mem (γ := LieSubalgebra R L) (engel R x) y_1 →
      Membership.mem (γ := LieSubalgebra R L) (engel R x) ⁅y, y_1⁆

Tactic:
rw [mem_normalizer_iff] at hy

Premises used: LieSubalgebra.mem_normalizer_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
x y : L
hy :
  ∀ (y_1 : L),
    Membership.mem (γ := LieSubalgebra R L) (engel R x) y_1 →
      Membership.mem (γ := LieSubalgebra R L) (engel R x) ⁅y, y_1⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R x) ⁅y, x⁆

Tactic:
specialize hy x (self_mem_engel R x)

Premises used: LieSubalgebra.self_mem_engel
-- 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
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (engel R x) ⁅y, x⁆
⊢ ∃ (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)
          ⁅x, y⁆ :
        L)
      (0 : L)

Tactic:
rw [← lie_skew, neg_mem_iff (G := L), mem_engel_iff] at hy

Premises used: neg_mem_iff, LieSubalgebra.mem_engel_iff, lie_skew
-- 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
x y : L
hy :
  ∃ (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)
          ⁅x, y⁆ :
        L)
      (0 : L)
rcases :
  ∀ (n : ℕ)
    (hn :
      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)
            ⁅x, y⁆ :
          L)
        (0 : L)),
    Membership.mem (γ := LieSubalgebra R L) (engel R x) y
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R x) y

Tactic:
rcases hy with ⟨n, hn⟩
-- 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
x y : L
n : ℕ
hn :
  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) ⁅x, y⁆ :
      L)
    (0 : L)
rw :
  ∃ (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) y : L)
      (0 : L)
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R x) y

Tactic:
rw [mem_engel_iff]

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
x y : L
n : ℕ
hn :
  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) ⁅x, y⁆ :
      L)
    (0 : L)
h :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (n + 1) : (a : L) → L)
        y :
      L)
    (0 : L)
⊢ ∃ (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) y : L)
      (0 : L)

Tactic:
use n + 1
-- 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
x y : L
n : ℕ
hn :
  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) ⁅x, y⁆ :
      L)
    (0 : L)
h :
  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)
        ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (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 : Module.End R L) (n + 1) : (a : L) → L)
        y :
      L)
    (0 : L)

Tactic:
rw [pow_succ, Module.End.mul_apply]

Premises used: pow_succ, Module.End.mul_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
x y : L
n : ℕ
hn :
  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) ⁅x, y⁆ :
      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) n : (a : L) → L)
        ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L) y : L) :
      L)
    (0 : L)

Tactic:
hn
-- 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
x y : L
n : ℕ
hn :
  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) ⁅x, y⁆ :
      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) n : (a : L) → L)
        ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L) y : L) :
      L)
    (0 : L)

Tactic:
exact hn
-- 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
set :
  let N := H.normalizer;
  N = H
⊢ H.normalizer = H

Tactic:
set N := normalizer H

Premises used: LieSubalgebra.normalizer
-- 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
apply : H.normalizer ≤ H
⊢ N = H

Tactic:
apply le_antisymm _ (le_normalizer H)

Premises used: LieSubalgebra.le_normalizer, le_antisymm
-- 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
⊢ N.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule

Tactic:
?_
-- 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
rwa rwa₁ rwa₂ rwa₃ : toSubmodule (engel R x) ≤ H.toSubmodule
⊢ toSubmodule (engel R x) ⊔ H.toSubmodule = H.toSubmodule

Tactic:
rwa [sup_eq_right]

Premises used: sup_eq_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
calc : N.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
⊢ H.normalizer ≤ H

Tactic:
calc N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule := ?_
       _ = H := by rwa [sup_eq_right]

Premises used: LieSubalgebra.engel, 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
n : L
hn : n ∈ N
⊢ ∀ y ∈ H, ⁅n, y⁆ ∈ H

Tactic:
rw [mem_normalizer_iff] at hn

Premises used: LieSubalgebra.mem_normalizer_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 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
n : L
hn : ∀ y ∈ H, ⁅n, y⁆ ∈ H
⊢ ⁅n, x⁆ ∈ H

Tactic:
specialize hn x (h (self_mem_engel R x))

Premises used: LieSubalgebra.self_mem_engel
-- 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
n : L
hn : ⁅n, x⁆ ∈ H
rwa : -⁅n, x⁆ ∈ H
rwa₁ rwa₂ rwa₃ rwa₄ : ⁅n, x⁆ ∈ H
⊢ ⁅x, n⁆ ∈ H

Tactic:
rwa [← lie_skew, neg_mem_iff (G := L)]

Premises used: neg_mem_iff, lie_skew
-- 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
⊢ ∀ n ∈ N, ⁅x, n⁆ ∈ H

Tactic:
have aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H := by
    intro n hn
    rw [mem_normalizer_iff] at hn
    specialize hn x (h (self_mem_engel R x))
    rwa [← lie_skew, neg_mem_iff (G := L)]
-- 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
⊢ ∀ n ∈ N, ⁅x, n⁆ ∈ N

Tactic:
have aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N := fun n hn ↦ le_normalizer H (aux₁ _ hn)
-- 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₂
⊢ ∃ (a : ℕ), ∀ b ≥ a, Codisjoint (dx ^ b).ker (dx ^ b).range

Tactic:
eventually_atTop.mp <| dx.eventually_codisjoint_ker_pow_range_pow

Premises used: Iff.mp, LinearMap.eventually_codisjoint_ker_pow_range_pow, Filter.eventually_atTop
-- 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₂
obtain :
  ∀ (k : ℕ) (hk : ∀ b ≥ k, Codisjoint (dx ^ b).ker (dx ^ b).range),
    N.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
⊢ N.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule

Tactic:
obtain ⟨k, hk⟩ : ∃ a, ∀ b ≥ a, Codisjoint (LinearMap.ker (dx ^ b)) (LinearMap.range (dx ^ b)) :=
    eventually_atTop.mp <| dx.eventually_codisjoint_ker_pow_range_pow

Premises used: Iff.mp, LinearMap.eventually_codisjoint_ker_pow_range_pow, Filter.eventually_atTop
-- 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 : ∀ b ≥ k, Codisjoint (dx ^ b).ker (dx ^ b).range
⊢ Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range

Tactic:
specialize hk (k + 1) (Nat.le_add_right k 1)

Premises used: Nat.le_add_right, HAdd.hAdd, OfNat.ofNat
-- 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
rw : ⊤ ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
⊢ N.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule

Tactic:
rw [← Submodule.map_subtype_top N.toSubmodule, Submodule.map_le_iff_le_comap]

Premises used: Submodule.map_subtype_top, Submodule.map_le_iff_le_comap, 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 : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
a : (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
a₁ : (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
⊢ ⊤ ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)

Tactic:
apply hk
-- 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)).ker ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
⊢ (dx ^ (k + 1)).ker ≤ 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)).ker ≤ toSubmodule (engel R x)
⊢ Submodule.map N.subtype (dx ^ (k + 1)).ker ≤ toSubmodule (engel R x) ⊔ H.toSubmodule

Tactic:
apply le_sup_of_le_left

Premises used: le_sup_of_le_left
-- 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)).ker ≤ Submodule.comap N.subtype (toSubmodule (engel R x))
⊢ Submodule.map N.subtype (dx ^ (k + 1)).ker ≤ toSubmodule (engel R x)

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
hy : y ∈ (dx ^ (k + 1)).ker
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)
⊢ y ∈ Submodule.comap N.subtype (toSubmodule (engel R x))

Tactic:
simp only [Submodule.mem_comap, mem_engel_iff, mem_toSubmodule]

Premises used: LieSubalgebra.mem_toSubmodule, Submodule.mem_comap, 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 : 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
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)
⊢ ∃ (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:
use k + 1
-- 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
hy : y ∈ (dx ^ (k + 1)).ker
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)
⊢ 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