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 = ⊤
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 : ℕ
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)
succ :
  Submodule.map (R := R) (σ₁₂ := RingHom.id R)
        (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x)
        (↑(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 + 1))
          (↑(I.lcs M j) : Submodule R M) ⊔
        (↑⁅I, I.lcs M j⁆ : Submodule R M) ∧
    (↑⁅I, 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 + 1))
          (↑(I.lcs M j) : Submodule R M) ⊔
        (↑⁅I, I.lcs M j⁆ : 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:
simp only [LieIdeal.lcs_succ, i.add_succ l, lie_top_eq_of_span_sup_eq_top hxI, sup_le_iff]

Premises used: LieSubmodule.lie_top_eq_of_span_sup_eq_top, LieIdeal.lcs_succ, sup_le_iff, Nat.add_succ
-- 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 = ⊤
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 : ℕ
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)
⊢ Submodule.map (R := R) (σ₁₂ := RingHom.id R)
        (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x)
        (↑(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 + 1))
          (↑(I.lcs M j) : Submodule R M) ⊔
        (↑⁅I, I.lcs M j⁆ : Submodule R M) ∧
    (↑⁅I, 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 + 1))
          (↑(I.lcs M j) : Submodule R M) ⊔
        (↑⁅I, I.lcs M j⁆ : Submodule R M)

Tactic:
⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩

Premises used: le_sup_of_le_right, And.intro, Submodule.map_mono, LE.le.trans
-- 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 = ⊤
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 : ℕ
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)
succ :
  Submodule.map (σ₁₂ := RingHom.id R)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x)
      (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)) ≤
    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, I.lcs M j⁆ : Submodule R M)
succ₁ : LE.le (α := Submodule R M) (↑⁅I, LieIdeal.lcs ⊤ M (i + l)⁆ : Submodule R M) (↑⁅I, I.lcs M j⁆ : Submodule R M)
⊢ Submodule.map (R := R) (σ₁₂ := RingHom.id R)
        (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x)
        (↑(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 + 1))
          (↑(I.lcs M j) : Submodule R M) ⊔
        (↑⁅I, I.lcs M j⁆ : Submodule R M) ∧
    (↑⁅I, 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 + 1))
          (↑(I.lcs M j) : Submodule R M) ⊔
        (↑⁅I, I.lcs M j⁆ : Submodule R M)

Tactic:
refine ⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩
-- 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 = ⊤
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 : ℕ
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)
succ :
  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) ⊔
      Submodule.map (σ₁₂ := RingHom.id R)
        (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x)
        (↑(I.lcs M (j + 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)
⊢ Submodule.map (σ₁₂ := RingHom.id R)
      (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x)
      (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)) ≤
    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, I.lcs M j⁆ : Submodule R M)

Tactic:
rw [Submodule.map_sup, ← Submodule.map_comp, ← Module.End.mul_eq_comp, ← pow_succ', ←
        I.lcs_succ]

Premises used: Module.End.mul_eq_comp, Submodule.map_sup, LieIdeal.lcs_succ, Submodule.map_comp, pow_succ'
-- 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 = ⊤
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 : ℕ
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)
succ succ₁ :
  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) ≤
    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)
⊢ 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) ⊔
      Submodule.map (σ₁₂ := RingHom.id R)
        (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x)
        (↑(I.lcs M (j + 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:
grw [coe_map_toEnd_le]

Premises used: LieSubmodule.coe_map_toEnd_le
-- 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 = ⊤
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 : ℕ
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)
succ : LE.le (α := LieSubmodule R L M) (LieIdeal.lcs ⊤ M (i + l)) (I.lcs M j)
⊢ LE.le (α := LieSubmodule R L M) ⁅I, LieIdeal.lcs ⊤ M (i + l)⁆ ⁅I, I.lcs M j⁆

Tactic:
gcongr
-- 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 = ⊤
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 : ℕ
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)
⊢ LE.le (α := LieSubmodule R L M) (LieIdeal.lcs ⊤ M (i + l)) (I.lcs M j)

Tactic:
le_trans (antitone_lowerCentralSeries R L M le_self_add) hIM

Premises used: LieModule.antitone_lowerCentralSeries, le_self_add, le_trans
-- 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 = ⊤
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 : ℕ
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)
⊢ LE.le (α := LieSubmodule R L M) (LieIdeal.lcs ⊤ M (i + l)) (I.lcs M j)

Tactic:
exact le_trans (antitone_lowerCentralSeries R L M le_self_add) hIM

Premises used: LieModule.antitone_lowerCentralSeries, le_self_add, le_trans
-- 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 = ⊤
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)
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)
⊢ (↑(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)

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

Premises used: Module.End.mul_eq_comp, Module.End.one_eq_id, LieSubmodule.lie_top_eq_of_span_sup_eq_top, Submodule.map_id, LieSubmodule.coe_map_toEnd_le, Submodule.map_sup, le_sup_of_le_left, LieIdeal.lcs_succ, Submodule.map_comp, LieModule.antitone_lowerCentralSeries, pow_zero, sup_le_iff, Nat.add_succ, add_zero, le_self_add, pow_succ', le_trans
-- 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 = ⊤
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
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
⊢ LieModule.IsNilpotent L M

Tactic:
obtain ⟨n, hn⟩ := hnp
-- 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
obtain :
  ∀ (k : ℕ) (hk : Eq (α := LieSubmodule.{u₁, u₂, u₄} R (↥I) M) (lowerCentralSeries R (↥I) M k) ⊥),
    LieModule.IsNilpotent L M
⊢ LieModule.IsNilpotent L M

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R I M

Premises used: Membership.mem, LieModule.IsNilpotent.nilpotent, Subtype
-- 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) ⊥
⊢ Eq (α := LieSubmodule R L M) (I.lcs M k) ⊥

Tactic:
simp only [← toSubmodule_inj, I.coe_lcs_eq, hk, bot_toSubmodule]

Premises used: LieSubmodule.bot_toSubmodule, LieSubmodule.toSubmodule_inj, LieIdeal.coe_lcs_eq
-- 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) ⊥
⊢ 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]
-- 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) ⊥
this : ∀ (l : ℕ), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)
rw : ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ LieModule.IsNilpotent L M

Tactic:
rw [isNilpotent_iff R]

Premises used: LieModule.isNilpotent_iff
-- 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) ⊥
this : ∀ (l : ℕ), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)
h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k * n)) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
use k * n
-- 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) ⊥
this : ∀ (l : ℕ), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (l * n)) (I.lcs M l)
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k * n)) ⊥

Tactic:
simpa [hk'] using this k