awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Engel
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) ⊥
suffices : ∀ (l : ℕ), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)
⊢ LieModule.IsNilpotent L M

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
-- Module: Mathlib.Algebra.Lie.Engel
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) ⊥
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (0 * n)) (I.lcs M 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Engel
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 : ℕ
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:
(l.succ_mul n).symm ▸ lcs_le_lcs_of_is_nilpotent_span_sup_eq_top hxI hn ih

Premises used: Set.Mem, Eq.rec, LieSubmodule.lcs_le_lcs_of_is_nilpotent_span_sup_eq_top, Nat.succ_mul, Eq.symm
-- Module: Mathlib.Algebra.Lie.Engel
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 : ℕ
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:
exact (l.succ_mul n).symm ▸ lcs_le_lcs_of_is_nilpotent_span_sup_eq_top hxI hn ih
-- Module: Mathlib.Algebra.Lie.Engel
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)
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))
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)

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
-- Module: Mathlib.Algebra.Lie.Engel
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)
h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 1) ⊥
⊢ LieModule.IsNilpotent L M

Tactic:
use 1
-- Module: Mathlib.Algebra.Lie.Engel
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)
⊢ Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 1) ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Engel
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 := ⋯
⊢ ∀ (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)
-- Module: Mathlib.Algebra.Lie.Engel
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)
⊢ 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
-- Module: Mathlib.Algebra.Lie.Engel
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

Tactic:
haveI : LieModule.IsNilpotent L M := h M hnp
-- Module: Mathlib.Algebra.Lie.Engel
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
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)
⊢ LieModule.IsNilpotent L₂ M

Tactic:
apply hf.lieModuleIsNilpotent _ surj_id

Premises used: Function.Surjective.lieModuleIsNilpotent
-- Module: Mathlib.Algebra.Lie.Engel
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
⊢ ∀ (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:
aesop
-- Module: Mathlib.Algebra.Lie.Engel
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₂
e : L ≃ₗ⁅R⁆ L₂
⊢ LieAlgebra.IsEngelian R L ↔ LieAlgebra.IsEngelian R L₂

Tactic:
⟨e.surjective.isEngelian, e.symm.surjective.isEngelian⟩

Premises used: Function.Surjective.isEngelian, LieEquiv.surjective, Iff.intro, LieEquiv.symm
-- Module: Mathlib.Algebra.Lie.Engel
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
obtain :
  ∀ (x : L) (hx₁ : x ∈ K.normalizer) (hx₂ : x ∉ K), ∃ (K' : LieSubalgebra R L), IsEngelian.{u₁, u₂, u₄} R ↥K' ∧ K < K'
⊢ ∃ (K' : LieSubalgebra R L), IsEngelian.{u₁, u₂, u₄} R ↥K' ∧ K < K'

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := SetLike.exists_of_lt hK₂

Premises used: SetLike.exists_of_lt
-- Module: Mathlib.Algebra.Lie.Engel
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' := ⋯ }
⊢ x ∈ K'

Tactic:
have hxK' : x ∈ K' := Submodule.mem_sup_left (Submodule.subset_span (Set.mem_singleton _))
-- Module: Mathlib.Algebra.Lie.Engel
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 ≤ K'

Tactic:
have hKK' : K ≤ K' := (LieSubalgebra.toSubmodule_le_toSubmodule K K').mp le_sup_right
-- Module: Mathlib.Algebra.Lie.Engel
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'.toSubmodule ≤ K.normalizer.toSubmodule

Tactic:
sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) hK₂.le

Premises used: Iff.mpr, Set.Mem, LT.lt.le, sup_le, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.Algebra.Lie.Engel
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'.toSubmodule ≤ K.normalizer.toSubmodule

Tactic:
exact sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) hK₂.le

Premises used: Iff.mpr, LT.lt.le, sup_le, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.Algebra.Lie.Engel
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' ≤ 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
-- Module: Mathlib.Algebra.Lie.Engel
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'

Tactic:
⟨K', ?_, lt_iff_le_and_ne.mpr ⟨hKK', fun contra => hx₂ (contra.symm ▸ hxK')⟩⟩

Premises used: Iff.mpr, lt_iff_le_and_ne, Eq.rec, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Lie.Engel
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
refine : IsEngelian.{u₁, u₂, u₄} R ↥K'
⊢ ∃ (K' : LieSubalgebra R L), IsEngelian.{u₁, u₂, u₄} R ↥K' ∧ K < K'

Tactic:
refine ⟨K', ?_, lt_iff_le_and_ne.mpr ⟨hKK', fun contra => hx₂ (contra.symm ▸ hxK')⟩⟩
-- Module: Mathlib.Algebra.Lie.Engel
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)
obtain :
  ∀ (I : LieIdeal R ↥K') (hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'),
    LieModule.IsNilpotent.{u₂, u₄} (↥K') M
⊢ 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'

Premises used: LieSubalgebra.ofLe, LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer
-- Module: Mathlib.Algebra.Lie.Engel
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'
rw : R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (LieSubalgebra.ofLe hKK').toSubmodule = ⊤
⊢ R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (↑I : Submodule R ↥K') = ⊤

Tactic:
rw [← LieIdeal.toLieSubalgebra_toSubmodule R K' I, hI₁]

Premises used: Membership.mem, LieIdeal.toLieSubalgebra_toSubmodule, Subtype
-- Module: Mathlib.Algebra.Lie.Engel
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'
a :
  Submodule.map K'.subtype (R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (LieSubalgebra.ofLe hKK').toSubmodule) =
    Submodule.map K'.subtype ⊤
⊢ R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (LieSubalgebra.ofLe hKK').toSubmodule = ⊤

Tactic:
apply Submodule.map_injective_of_injective (K' : Submodule R L).injective_subtype

Premises used: Submodule.injective_subtype, LieSubalgebra.toSubmodule, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Lie.Engel
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'
a : Submodule.map K'.subtype (R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK') ⊔ K.toSubmodule = K'.toSubmodule
⊢ Submodule.map K'.subtype (R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (LieSubalgebra.ofLe hKK').toSubmodule) =
    Submodule.map K'.subtype ⊤

Tactic:
simp only [LieSubalgebra.coe_ofLe, Submodule.map_sup, Submodule.map_subtype_range_inclusion,
      Submodule.map_top, Submodule.range_subtype]

Premises used: Submodule.map_top, Submodule.map_sup, LieSubalgebra.coe_ofLe, Submodule.map_subtype_range_inclusion, Submodule.range_subtype
-- Module: Mathlib.Algebra.Lie.Engel
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'
a a₁ : R ∙ (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK') : L) ⊔ K.toSubmodule = K'.toSubmodule
⊢ Submodule.map K'.subtype (R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK') ⊔ K.toSubmodule = K'.toSubmodule

Tactic:
rw [Submodule.map_subtype_span_singleton]

Premises used: Submodule.map_subtype_span_singleton
-- Module: Mathlib.Algebra.Lie.Engel
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') = ⊤

Tactic:
have hI₂ : R ∙ (⟨x, hxK'⟩ : K') ⊔ LieSubmodule.toSubmodule I = ⊤ := by
    rw [← LieIdeal.toLieSubalgebra_toSubmodule R K' I, hI₁]
    apply Submodule.map_injective_of_injective (K' : Submodule R L).injective_subtype
    simp only [LieSubalgebra.coe_ofLe, Submodule.map_sup, Submodule.map_subtype_range_inclusion,
      Submodule.map_top, Submodule.range_subtype]
    rw [Submodule.map_subtype_span_singleton]
-- Module: Mathlib.Algebra.Lie.Engel
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'
hI₂ : R ∙ Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hxK' ⊔ (↑I : Submodule R ↥K') = ⊤
have : ∀ (e : ↥K ≃ₗ⁅R⁆ ↥I), LieModule.IsNilpotent.{u₂, u₄} (↥K') M
⊢ LieModule.IsNilpotent.{u₂, u₄} (↥K') M

Tactic:
have e : K ≃ₗ⁅R⁆ I :=
    (LieSubalgebra.equivOfLe hKK').trans
      (LieEquiv.ofEq _ _ ((LieSubalgebra.coe_set_eq _ _).mpr hI₁.symm))