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
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 : L
⊢ ∀ {x_1 y : L},
    Membership.mem (γ := Set L)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_1, u_2} (R := R)
              (Module.End.maxGenEigenspace ((ad R L : (a : L) → Module.End R L) x) 0))))
        x_1 →
      Membership.mem (γ := Set L)
          (AddSubsemigroup.carrier
            (AddSubmonoid.toAddSubsemigroup
              (Submodule.toAddSubmonoid.{u_1, u_2} (R := R)
                (Module.End.maxGenEigenspace ((ad R L : (a : L) → Module.End R L) x) 0))))
          y →
        Membership.mem (γ := Set L)
          (AddSubsemigroup.carrier
            (AddSubmonoid.toAddSubsemigroup
              (Submodule.toAddSubmonoid.{u_1, u_2} (R := R)
                (Module.End.maxGenEigenspace ((ad R L : (a : L) → Module.End R L) x) 0))))
          ⁅x_1, y⁆
have simp : ∀ {x_1 y : L} (x_2 : ℕ)
  (h :
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_2 : (a : L) → L)
          x_1 :
        L)
      (0 : L))
  (x_3 : ℕ)
  (h :
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_3 : (a : L) → L) y :
        L)
      (0 : L)),
  ∃ (k : ℕ),
    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)
          ⁅x_1, y⁆ :
        L)
      (0 : L)
Tactic: simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid, Module.End.mem_maxGenEigenspace, zero_smul,
        sub_zero, forall_exists_index]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ ∃ (k : ℕ),
    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)
          ⁅y, z⁆ :
        L)
      (0 : L)
have refine : Eq (α := L)
  ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (m + n) : (a : L) → L)
      ⁅y, z⁆ :
    L)
  (0 : L)
Tactic: refine ⟨m + n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (m + n) : (a : L) → L)
        ⁅y, z⁆ :
      L)
    (0 : L)
have rw : Eq.{u_2 + 1} (α := L)
  (∑ ij ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n),
    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: rw [ad_pow_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ Eq.{u_2 + 1} (α := L)
    (∑ ij ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n),
      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
have h : ∀ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n),
  HSMul.hSMul (β := L) ((m + n).choose x_1.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) x_1.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) x_1.2 :
              (a : L) → L)
            z) :
        L) =
    0
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (hypothesis)
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)
⊢ m ≤ ij.1 ∨ n ≤ ij.2
have hij₁ : ij.1 + ij.2 = m + n
Tactic: rw [Finset.mem_antidiagonal] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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)
⊢ 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
have h : ∀ (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: obtain (h | h) : m ≤ ij.1 ∨ n ≤ ij.2 := by rw [Finset.mem_antidiagonal] at hij; lia
-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
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 :
  ∀ (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
⊢ 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
have h₁ : ∀ (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: obtain (h | h) : m ≤ ij.1 ∨ n ≤ ij.2 := by rw [Finset.mem_antidiagonal] at hij; lia
-- 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
x : L
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R x) x
have 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)
Tactic: simp only [mem_engel_iff]
-- 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
⊢ Eq.{u_2 + 1} (α := LieSubalgebra R L) (engel R 0) ⊤
have rw : LE.le.{u_2} (α := LieSubalgebra R L) ⊤ (engel R 0)
Tactic: rw [eq_top_iff]
-- 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
x : L
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R 0) x
have rw : ∃ (n : ℕ), Eq (α := L) ((HPow.hPow (α := Module.End R L) 0 n : (a : L) → L) x : L) (0 : L)
Tactic: rw [mem_engel_iff, map_zero]
-- 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
x : L
⊢ ∃ (n : ℕ), Eq (α := L) ((HPow.hPow (α := Module.End R L) 0 n : (a : L) → L) x : L) (0 : L)
have h : Eq (α := L) ((HPow.hPow (α := Module.End R L) (β := ℕ) 0 1 : (a : L) → L) x : L) (0 : L)
Tactic: use 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
x : L
⊢ Eq (α := LieSubalgebra R L) (normalizer (engel R x)) (engel R x)
have apply : LE.le (α := LieSubalgebra R L) (normalizer (engel R x)) (engel R x)
Tactic: apply le_antisymm _ (le_normalizer _)
-- 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
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (normalizer (engel R x)) y
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R x) y
have 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⁆
Tactic: rw [mem_normalizer_iff] at hy
Cleared hypotheses: hy
-- 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
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
have hy₁ : Membership.mem (γ := LieSubalgebra R L) (engel R x) ⁅y, x⁆
Tactic: specialize hy x (self_mem_engel R x)
Cleared hypotheses: hy
-- 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
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (engel R x) ⁅y, x⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R x) y
have 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)
Tactic: rw [← lie_skew, neg_mem_iff (G := L), mem_engel_iff] 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
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)
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R x) y
have 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
Tactic: rcases hy with ⟨n, hn⟩
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
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)
⊢ Membership.mem (γ := LieSubalgebra R L) (engel R x) y
have 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)
Tactic: rw [mem_engel_iff]
-- 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
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)
⊢ ∃ (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)
have 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)
Tactic: use n + 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
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 + 1) : (a : L) → L)
        y :
      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) 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: rw [pow_succ, Module.End.mul_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
⊢ N = H
have apply : H.normalizer ≤ H
Tactic: apply le_antisymm _ (le_normalizer 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 : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
⊢ toSubmodule (engel R x) ⊔ H.toSubmodule = H.toSubmodule
have rwa : toSubmodule (engel R x) ≤ H.toSubmodule
Tactic: rwa [sup_eq_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
⊢ H.normalizer ≤ H
have calc : N.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
Tactic: calc N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule := ?_
       _ = H := by rwa [sup_eq_right]
-- 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 : 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
⊢ ⁅x, n⁆ ∈ H
have hn₁ : ∀ y ∈ H, ⁅n, y⁆ ∈ H
Tactic: rw [mem_normalizer_iff] at hn
Cleared hypotheses: hn
-- 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 : 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
⊢ ⁅x, n⁆ ∈ H
have hn₁ : ⁅n, x⁆ ∈ H
Tactic: specialize hn x (h (self_mem_engel R x))
Cleared hypotheses: hn
-- 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
n : L
hn : ⁅n, x⁆ ∈ H
⊢ ⁅x, n⁆ ∈ H
have rwa : -⁅n, x⁆ ∈ H
Tactic: rwa [← lie_skew, neg_mem_iff (G := L)]
-- 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 : 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
have aux₁ : ∀ 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)]
-- 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 : 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.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
have aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
Tactic: have aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N := fun n hn ↦ le_normalizer H (aux₁ _ hn)
-- 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₂
⊢ N.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
have obtain : ∀ (k : ℕ) (hk : ∀ b ≥ k, Codisjoint (dx ^ b).ker (dx ^ b).range),
  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
-- 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 : 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
⊢ N.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
have hk₁ : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
Tactic: specialize hk (k + 1) (Nat.le_add_right k 1)
Cleared hypotheses: hk
-- 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
⊢ N.toSubmodule ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
have rw : ⊤ ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
Tactic: rw [← Submodule.map_subtype_top N.toSubmodule, 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.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
have a : (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
Tactic: apply hk
-- 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
a : (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
⊢ ⊤ ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
have a₁ : (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
Tactic: apply hk
-- 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)).ker ≤ Submodule.comap N.subtype (toSubmodule (engel R x) ⊔ H.toSubmodule)
have a : Submodule.map N.subtype (dx ^ (k + 1)).ker ≤ toSubmodule (engel R x) ⊔ H.toSubmodule
Tactic: rw [← Submodule.map_le_iff_le_comap]