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 : LieSubmodule R L M
refine_1 :
  {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x} ⊆
    (↑(Submodule.span R
          ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x})) :
      Set M)
⊢ Eq (α := Submodule R M) (Submodule.span R {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x})
    (Submodule.span R
      ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}))
have refine_2 : ∀ (z : M)
  (hz :
    Membership.mem (γ := Set M)
      ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}) z),
  Membership.mem (γ := Set M) {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x} z
Tactic: refine le_antisymm (Submodule.span_le.mpr ?_) (Submodule.span_mono fun z hz => ?_)
-- 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 : LieSubmodule R L M
y : L
n : M
hn : n ∈ N
⊢ ⁅y, n⁆ ∈
    (↑(Submodule.span R
          ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x})) :
      Set M)
have refine_1 : ∀ (t : R) (z : L) (hz : z ∈ I),
  ⁅t • x + z, n⁆ ∈
    (↑(Submodule.span R
          ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x})) :
      Set M)
Tactic: obtain ⟨t, z, hz, rfl⟩ := exists_smul_add_of_span_sup_eq_top hxI y
Cleared hypotheses: y
-- 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 : LieSubmodule R L M
n : M
hn : n ∈ N
t : R
z : L
hz : z ∈ I
⊢ ⁅t • x + z, n⁆ ∈
    (↑(Submodule.span R
          ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x})) :
      Set M)
have refine_1 : ∃ (y : M),
  Membership.mem (γ := Submodule R M) (Submodule.span R ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M))) y ∧
    ∃ (z_1 : M),
      Membership.mem (γ := Submodule R M) (Submodule.span R {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}) z_1 ∧
        y + z_1 = ⁅t • x + z, n⁆
Tactic: simp only [SetLike.mem_coe, Submodule.span_union, Submodule.mem_sup]
-- 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 : LieSubmodule R L M
z : M
hz :
  Membership.mem (γ := Set M)
    ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}) z
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x} z
have refine_2 : ∀ (m : M) (hm : m ∈ (↑(↑N : Submodule R M) : Set M)),
  Membership.mem (γ := Set M) {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x} ((fun (a : M) ↦ ⁅x, a⁆) m)
Tactic: rcases hz with (⟨m, hm, rfl⟩ | ⟨y, -, m, hm, rfl⟩)
Cleared hypotheses: z, hz
-- 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 : LieSubmodule R L M
z : M
hz :
  Membership.mem (γ := Set M)
    ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}) z
refine_2 :
  ∀ (m : M) (hm : m ∈ (↑(↑N : Submodule R M) : Set M)),
    Membership.mem (γ := Set M) {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x} ((fun (a : M) ↦ ⁅x, a⁆) m)
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x} z
have refine_2₁ : ∀ (y : L) (m : M) (hm : m ∈ N), Membership.mem (γ := Set M) {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x} ⁅y, m⁆
Tactic: rcases hz with (⟨m, hm, rfl⟩ | ⟨y, -, m, hm, rfl⟩)
Cleared hypotheses: z, hz
-- 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)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (i + n)) (I.lcs M (j + 1))
have LieIdeal : ∀ (l : ℕ),
  (↑(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: suffices
    ∀ l,
      ((⊤ : LieIdeal R L).lcs M (i + l) : Submodule R M) ≤
        (I.lcs M j : Submodule R M).map (toEnd R L M x ^ l) ⊔
          (I.lcs M (j + 1) : Submodule R M)
    by simpa only [bot_sup_eq, LieIdeal.incl_coe, Submodule.map_zero, hxn] using this 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 = ⊤
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)
⊢ (↑(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)
have zero : LE.le (α := Submodule R M) (↑(LieIdeal.lcs ⊤ M i) : Submodule R M)
  ((↑(I.lcs M j) : Submodule R M) ⊔ (↑⁅I, I.lcs M j⁆ : Submodule R M))
Tactic: simp only [add_zero, LieIdeal.lcs_succ, pow_zero, Module.End.one_eq_id,
      Submodule.map_id]
-- 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 : ℕ
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)
have 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)
Tactic: simp only [LieIdeal.lcs_succ, i.add_succ l, lie_top_eq_of_span_sup_eq_top hxI, sup_le_iff]
-- 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 : ℕ
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)
have 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)
Tactic: refine ⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩
-- 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 : ℕ
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)
⊢ 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)
have succ₁ : LE.le (α := Submodule R M) (↑⁅I, LieIdeal.lcs ⊤ M (i + l)⁆ : Submodule R M) (↑⁅I, I.lcs M j⁆ : Submodule R M)
Tactic: refine ⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩
-- 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 : ℕ
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 (σ₁₂ := 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)
have 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)
Tactic: rw [Submodule.map_sup, ← Submodule.map_comp, ← Module.End.mul_eq_comp, ← pow_succ', ←
        I.lcs_succ]
-- 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 : ℕ
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
        (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)
have 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)
Tactic: grw [coe_map_toEnd_le]
-- 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 : ℕ
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) ⁅I, LieIdeal.lcs ⊤ M (i + l)⁆ ⁅I, I.lcs M j⁆
have succ : LE.le (α := LieSubmodule R L M) (LieIdeal.lcs ⊤ M (i + l)) (I.lcs M j)
Tactic: gcongr
-- 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 : ℕ
⊢ (↑(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 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)
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