awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn :
  HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n =
    0
hIM : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M i) (I.lcs M j)
l : ℕ
zero :
  (↑(LieIdeal.lcs ⊤ M (i + 0)) : Submodule R M) ≤
    Submodule.map
        (HPow.hPow (α := Module.End R M) (β := ℕ)
          (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) 0)
        (↑(I.lcs M j) : Submodule R M) ⊔
      (↑(I.lcs M (j + 1)) : Submodule R M)
⊢ (↑(LieIdeal.lcs ⊤ M (i + l)) : Submodule R M) ≤
    Submodule.map
        (HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) l)
        (↑(I.lcs M j) : Submodule R M) ⊔
      (↑(I.lcs M (j + 1)) : Submodule R M)
have succ : ∀ (l : ℕ)
  (ih :
    (↑(LieIdeal.lcs ⊤ M (i + l)) : Submodule R M) ≤
      Submodule.map
          (HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
            l)
          (↑(I.lcs M j) : Submodule R M) ⊔
        (↑(I.lcs M (j + 1)) : Submodule R M)),
  (↑(LieIdeal.lcs ⊤ M (i + (l + 1))) : Submodule R M) ≤
    Submodule.map
        (HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
          (l + 1))
        (↑(I.lcs M j) : Submodule R M) ⊔
      (↑(I.lcs M (j + 1)) : Submodule R M)
Tactic: induction l with
  | zero =>
    simp only [add_zero, LieIdeal.lcs_succ, pow_zero, Module.End.one_eq_id,
      Submodule.map_id]
    exact le_sup_of_le_left hIM
  | succ l ih =>
    simp only [LieIdeal.lcs_succ, i.add_succ l, lie_top_eq_of_span_sup_eq_top hxI, sup_le_iff]
    refine ⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩
    · rw [Submodule.map_sup, ← Submodule.map_comp, ← Module.End.mul_eq_comp, ← pow_succ', ←
        I.lcs_succ]
      grw [coe_map_toEnd_le]
    · norm_cast
      gcongr
      exact le_trans (antitone_lowerCentralSeries R L M le_self_add) hIM
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hnp :
  _root_.IsNilpotent.{u₄} (R := Module.End R M)
    (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
hIM : LieModule.IsNilpotent.{u₂, u₄} (↥I) M
⊢ LieModule.IsNilpotent L M
have obtain : ∀ (n : ℕ)
  (hn :
    HPow.hPow (α := Module.End R M)
        (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n =
      0),
  LieModule.IsNilpotent L M
Tactic: obtain ⟨n, hn⟩ := hnp
Cleared hypotheses: hnp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent.{u₂, u₄} (↥I) M
n : ℕ
hn :
  HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n =
    0
⊢ LieModule.IsNilpotent L M
have obtain : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule.{u₁, u₂, u₄} R (↥I) M) (lowerCentralSeries R (↥I) M k) ⊥),
  LieModule.IsNilpotent L M
Tactic: obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R I M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent.{u₂, u₄} (↥I) M
n : ℕ
hn :
  HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n =
    0
k : ℕ
hk : Eq (α := LieSubmodule.{u₁, u₂, u₄} R (↥I) M) (lowerCentralSeries R (↥I) M k) ⊥
⊢ LieModule.IsNilpotent L M
have hk' : Eq (α := LieSubmodule R L M) (I.lcs M k) ⊥
Tactic: have hk' : I.lcs M k = ⊥ := by
    simp only [← toSubmodule_inj, I.coe_lcs_eq, hk, bot_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent.{u₂, u₄} (↥I) M
n : ℕ
hn :
  HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n =
    0
k : ℕ
hk : Eq (α := LieSubmodule.{u₁, u₂, u₄} R (↥I) M) (lowerCentralSeries R (↥I) M k) ⊥
hk' : Eq (α := LieSubmodule R L M) (I.lcs M k) ⊥
this : ∀ (l : ℕ), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)
⊢ LieModule.IsNilpotent L M
have rw : ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
Tactic: rw [isNilpotent_iff R]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent.{u₂, u₄} (↥I) M
n : ℕ
hn :
  HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n =
    0
k : ℕ
hk : Eq (α := LieSubmodule.{u₁, u₂, u₄} R (↥I) M) (lowerCentralSeries R (↥I) M k) ⊥
hk' : Eq (α := LieSubmodule R L M) (I.lcs M k) ⊥
this : ∀ (l : ℕ), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k * n)) ⊥
Tactic: use k * n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent.{u₂, u₄} (↥I) M
n : ℕ
hn :
  HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n =
    0
k : ℕ
hk : Eq (α := LieSubmodule.{u₁, u₂, u₄} R (↥I) M) (lowerCentralSeries R (↥I) M k) ⊥
hk' : Eq (α := LieSubmodule R L M) (I.lcs M k) ⊥
⊢ LieModule.IsNilpotent L M
have suffices : ∀ (l : ℕ), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)
Tactic: suffices ∀ l, lowerCentralSeries R L M (l * n) ≤ I.lcs M l by
    rw [isNilpotent_iff R]
    use k * n
    simpa [hk'] using this k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent.{u₂, u₄} (↥I) M
n : ℕ
hn :
  HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n =
    0
k : ℕ
hk : Eq (α := LieSubmodule.{u₁, u₂, u₄} R (↥I) M) (lowerCentralSeries R (↥I) M k) ⊥
hk' : Eq (α := LieSubmodule R L M) (I.lcs M k) ⊥
l : ℕ
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)
have zero : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (0 * n)) (I.lcs M 0)
Tactic: induction l with
  | zero => simp
  | succ l ih => exact (l.succ_mul n).symm ▸ lcs_le_lcs_of_is_nilpotent_span_sup_eq_top hxI hn ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent.{u₂, u₄} (↥I) M
n : ℕ
hn :
  HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n =
    0
k : ℕ
hk : Eq (α := LieSubmodule.{u₁, u₂, u₄} R (↥I) M) (lowerCentralSeries R (↥I) M k) ⊥
hk' : Eq (α := LieSubmodule R L M) (I.lcs M k) ⊥
l : ℕ
zero : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (0 * n)) (I.lcs M 0)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)
have succ : ∀ (l : ℕ) (ih : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)),
  LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M ((l + 1) * n)) (I.lcs M (l + 1))
Tactic: induction l with
  | zero => simp
  | succ l ih => exact (l.succ_mul n).symm ▸ lcs_le_lcs_of_is_nilpotent_span_sup_eq_top hxI hn ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h :
  ∀ (x : L),
    IsNilpotent.{u_1} (R := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u_1} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
⊢ LieModule.IsNilpotent L M
have h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 1) ⊥
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
Goal:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective.{u₂ + 1, u₃ + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' :
  ∀ (x : L₂),
    IsNilpotent.{u₄} (R := Module.End R M)
      (((toEnd R L₂ M : LieHom.{u₁, u₃, u₄} R L₂ (Module.End R M)) : (a : L₂) → Module.End R M) x : Module.End R M)
this_1 : LieRingModule L M := LieRingModule.compLieHom M f
this : LieModule R L M := ⋯
⊢ LieModule.IsNilpotent L₂ M
have hnp : ∀ (x : L),
  IsNilpotent.{u₄} (R := Module.End R M)
    (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
Tactic: have hnp : ∀ x, IsNilpotent (toEnd R L M x) := fun x => h' (f x)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
Goal:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective.{u₂ + 1, u₃ + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' :
  ∀ (x : L₂),
    IsNilpotent.{u₄} (R := Module.End R M)
      (((toEnd R L₂ M : LieHom.{u₁, u₃, u₄} R L₂ (Module.End R M)) : (a : L₂) → Module.End R M) x : Module.End R M)
this_1 : LieRingModule L M := LieRingModule.compLieHom M f
this : LieModule R L M := ⋯
hnp :
  ∀ (x : L),
    IsNilpotent.{u₄} (R := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
⊢ LieModule.IsNilpotent L₂ M
have surj_id : Surjective.{u₄ + 1, u₄ + 1} (α := M) (β := M) (⇑LinearMap.id : (a : M) → M)
Tactic: have surj_id : Function.Surjective (LinearMap.id : M →ₗ[R] M) := Function.surjective_id
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
Goal:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective.{u₂ + 1, u₃ + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' :
  ∀ (x : L₂),
    IsNilpotent.{u₄} (R := Module.End R M)
      (((toEnd R L₂ M : LieHom.{u₁, u₃, u₄} R L₂ (Module.End R M)) : (a : L₂) → Module.End R M) x : Module.End R M)
this_1 : LieRingModule L M := LieRingModule.compLieHom M f
this : LieModule R L M := ⋯
hnp :
  ∀ (x : L),
    IsNilpotent.{u₄} (R := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
surj_id : Surjective.{u₄ + 1, u₄ + 1} (α := M) (β := M) (⇑LinearMap.id : (a : M) → M)
⊢ LieModule.IsNilpotent L₂ M
have this₁ : LieModule.IsNilpotent L M
Tactic: haveI : LieModule.IsNilpotent L M := h M hnp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective.{u₂ + 1, u₃ + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' :
  ∀ (x : L₂),
    IsNilpotent.{u₄} (R := Module.End R M)
      (((toEnd R L₂ M : LieHom.{u₁, u₃, u₄} R L₂ (Module.End R M)) : (a : L₂) → Module.End R M) x : Module.End R M)
this_1 : LieRingModule L M := LieRingModule.compLieHom M f
this_2 : LieModule R L M := ⋯
hnp :
  ∀ (x : L),
    IsNilpotent.{u₄} (R := Module.End R M)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
surj_id : Surjective.{u₄ + 1, u₄ + 1} (α := M) (β := M) (⇑LinearMap.id : (a : M) → M)
this : LieModule.IsNilpotent L M
⊢ LieModule.IsNilpotent L₂ M
have apply : ∀ (x : L) (m : M),
  Eq (α := M) (Bracket.bracket.{u₃, u₄} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((LinearMap.id : (a : M) → M) m) : M)
    ((LinearMap.id : (a : M) → M) ⁅x, m⁆ : M)
Tactic: apply hf.lieModuleIsNilpotent _ surj_id
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
⊢ ∃ (K' : LieSubalgebra R L), IsEngelian.{u₁, u₂, u₄} R ↥K' ∧ K < K'
have obtain : ∀ (x : L) (hx₁ : x ∈ K.normalizer) (hx₂ : x ∉ K), ∃ (K' : LieSubalgebra R L), IsEngelian.{u₁, u₂, u₄} R ↥K' ∧ K < K'
Tactic: obtain ⟨x, hx₁, hx₂⟩ := SetLike.exists_of_lt hK₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
⊢ ∃ (K' : LieSubalgebra R L), IsEngelian.{u₁, u₂, u₄} R ↥K' ∧ K < K'
have hxK' : x ∈ K'
Tactic: have hxK' : x ∈ K' := Submodule.mem_sup_left (Submodule.subset_span (Set.mem_singleton _))
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
⊢ ∃ (K' : LieSubalgebra R L), IsEngelian.{u₁, u₂, u₄} R ↥K' ∧ K < K'
have hKK' : K ≤ K'
Tactic: have hKK' : K ≤ K' := (LieSubalgebra.toSubmodule_le_toSubmodule K K').mp le_sup_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
⊢ ∃ (K' : LieSubalgebra R L), IsEngelian.{u₁, u₂, u₄} R ↥K' ∧ K < K'
have hK' : K' ≤ K.normalizer
Tactic: have hK' : K' ≤ K.normalizer := by
    rw [← LieSubalgebra.toSubmodule_le_toSubmodule]
    exact sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) hK₂.le
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
⊢ ∃ (K' : LieSubalgebra R L), IsEngelian.{u₁, u₂, u₄} R ↥K' ∧ K < K'
have refine : IsEngelian.{u₁, u₂, u₄} R ↥K'
Tactic: refine ⟨K', ?_, lt_iff_le_and_ne.mpr ⟨hKK', fun contra => hx₂ (contra.symm ▸ hxK')⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule.{u₂, u₄} (↥K') M
_i4 : LieModule.{u₁, u₂, u₄} R (↥K') M
h :
  ∀ (x : ↥K'),
    IsNilpotent.{u₄} (R := Module.End R M) ((toEnd R (↥K') M : (a : ↥K') → Module.End R M) x : Module.End R M)
⊢ LieModule.IsNilpotent.{u₂, u₄} (↥K') M
have obtain : ∀ (I : LieIdeal R ↥K') (hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'),
  LieModule.IsNilpotent.{u₂, u₄} (↥K') M
Tactic: obtain ⟨I, hI₁ : (I : LieSubalgebra R K') = LieSubalgebra.ofLe hKK'⟩ :=
    LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer hKK' hK'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule.{u₂, u₄} (↥K') M
_i4 : LieModule.{u₁, u₂, u₄} R (↥K') M
h :
  ∀ (x : ↥K'),
    IsNilpotent.{u₄} (R := Module.End R M) ((toEnd R (↥K') M : (a : ↥K') → Module.End R M) x : Module.End R M)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (↑I : Submodule R ↥K') = ⊤
have rw : R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (LieSubalgebra.ofLe hKK').toSubmodule = ⊤
Tactic: rw [← LieIdeal.toLieSubalgebra_toSubmodule R K' I, hI₁]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule.{u₂, u₄} (↥K') M
_i4 : LieModule.{u₁, u₂, u₄} R (↥K') M
h :
  ∀ (x : ↥K'),
    IsNilpotent.{u₄} (R := Module.End R M) ((toEnd R (↥K') M : (a : ↥K') → Module.End R M) x : Module.End R M)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (LieSubalgebra.ofLe hKK').toSubmodule = ⊤
have a : Submodule.map K'.subtype (R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (LieSubalgebra.ofLe hKK').toSubmodule) =
  Submodule.map K'.subtype ⊤
Tactic: apply Submodule.map_injective_of_injective (K' : Submodule R L).injective_subtype
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule.{u₂, u₄} (↥K') M
_i4 : LieModule.{u₁, u₂, u₄} R (↥K') M
h :
  ∀ (x : ↥K'),
    IsNilpotent.{u₄} (R := Module.End R M) ((toEnd R (↥K') M : (a : ↥K') → Module.End R M) x : Module.End R M)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ Submodule.map K'.subtype (R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (LieSubalgebra.ofLe hKK').toSubmodule) =
    Submodule.map K'.subtype ⊤
have a : Submodule.map K'.subtype (R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK') ⊔ K.toSubmodule = K'.toSubmodule
Tactic: simp only [LieSubalgebra.coe_ofLe, Submodule.map_sup, Submodule.map_subtype_range_inclusion,
      Submodule.map_top, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian.{u₁, u₂, u₄} R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule.{u₂, u₄} (↥K') M
_i4 : LieModule.{u₁, u₂, u₄} R (↥K') M
h :
  ∀ (x : ↥K'),
    IsNilpotent.{u₄} (R := Module.End R M) ((toEnd R (↥K') M : (a : ↥K') → Module.End R M) x : Module.End R M)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ Submodule.map K'.subtype (R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK') ⊔ K.toSubmodule = K'.toSubmodule
have a : R ∙ (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK') : L) ⊔ K.toSubmodule = K'.toSubmodule
Tactic: rw [Submodule.map_subtype_span_singleton]