awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i j : ι
y : L i
x : L j
inl :
  ∀ (x : L i),
    Eq.{w₁ + 1} (α := L')
      ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
          (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
        L')
inr :
  ∀ (hij : i ≠ j),
    Eq.{w₁ + 1} (α := L')
      ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
          (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
        L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i : ι
y x : L i
inl :
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        ((of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, y⁆ : ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inl₁ :
  Eq.{w₁ + 1} (α := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') ⁅x, y⁆ : L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inl₂ :
  Eq.{w₁ + 1} (α := L') (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') ⁅x, y⁆ : L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') y) :
      L')
inl₃ :
  Eq.{w₁ + 1} (α := L') ((f i : (a : L i) → L') ⁅x, y⁆ : L')
    (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f i : (a : L i) → L') y) : L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')

Tactic:
simp_rw [lie_of_same, toAddMonoid_of, LinearMap.toAddMonoidHom_coe, LieHom.coe_toLinearMap,
          LieHom.map_lie]

Premises used: LinearMap.toAddMonoidHom_coe, LieHom.map_lie, DirectSum.lie_of_same, LieHom.coe_toLinearMap, DirectSum.toAddMonoid_of
-- Module: Mathlib.Algebra.Lie.DirectSum
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i j : ι
y : L i
x : L j
hij : i ≠ j
inr :
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L') 0 : L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inr₁ :
  Eq.{w₁ + 1} (α := L') (0 : L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inr₂ :
  Eq.{w₁ + 1} (α := L') (0 : L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L') : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') y) :
      L')
inr₃ :
  Eq.{w₁ + 1} (α := L') (0 : L')
    (Bracket.bracket (L := L') ((f j : (a : L j) → L') x : L') ((f i : (a : L i) → L') y) : L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')

Tactic:
simp_rw [lie_of_of_ne _ hij.symm, map_zero, LinearMap.toAddMonoidHom_coe,
          LieHom.coe_toLinearMap, hf hij.symm x y]

Premises used: LinearMap.toAddMonoidHom_coe, DirectSum.lie_of_of_ne, map_zero, Ne.symm, LieHom.coe_toLinearMap
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
⊢ Membership.mem (γ := Submodule R L) ⊤ y

Tactic:
have hy : y ∈ (⊤ : Submodule R L) := Submodule.mem_top
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
hy : Membership.mem (γ := Submodule R L) ⊤ y
⊢ ∃ (y_1 : L), (∃ (a : R), a • x = y_1) ∧ ∃ z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule, y_1 + z = y

Tactic:
simp only [← hxI, Submodule.mem_sup, Submodule.mem_span_singleton] at hy

Premises used: Submodule.mem_span_singleton, Submodule.mem_sup
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
hy : ∃ (y_1 : L), (∃ (a : R), a • x = y_1) ∧ ∃ z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule, y_1 + z = y
obtain :
  ∀ (t : R) (z : L) (hz : z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule),
    ∃ (t_1 : R), ∃ z_1 ∈ I, t • x + z = t_1 • x + z_1
⊢ ∃ (t : R), ∃ z ∈ I, y = t • x + z

Tactic:
obtain ⟨-, ⟨t, rfl⟩, z, hz, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
t : R
z : L
hz : z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule
⊢ ∃ (t_1 : R), ∃ z_1 ∈ I, t • x + z = t_1 • x + z_1

Tactic:
⟨t, z, hz, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Lie.Engel
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
t : R
z : L
hz : z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule
⊢ ∃ (t_1 : R), ∃ z_1 ∈ I, t • x + z = t_1 • x + z_1

Tactic:
exact ⟨t, z, hz, rfl⟩
-- 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 : LieSubmodule R L M
simp :
  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}))
⊢ (↑(Bracket.bracket.{u₂, u₄} (L := LieIdeal R L) ⊤ N) : 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) (↑N : Submodule R M) ⊔
      (↑⁅I, N⁆ : Submodule R M)

Tactic:
simp only [lieIdeal_oper_eq_linear_span', Submodule.sup_span, mem_top, true_and,
    Submodule.map_coe, toEnd_apply_apply]

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieModule.toEnd_apply_apply, LieSubmodule.mem_top, Submodule.map_coe, Submodule.sup_span, true_and
-- 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 : LieSubmodule R L 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}))

Tactic:
le_antisymm (Submodule.span_le.mpr ?_) (Submodule.span_mono fun z hz => ?_)

Premises used: Iff.mpr, le_antisymm, Submodule.span_mono, Submodule.span_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 : 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)
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
⊢ 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}))

Tactic:
refine le_antisymm (Submodule.span_le.mpr ?_) (Submodule.span_mono fun z hz => ?_)

Premises used: Iff.mpr, le_antisymm, Submodule.span_mono, Submodule.span_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 : LieSubmodule R L M
y : L
n : M
hn : n ∈ N
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)
⊢ ⁅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)

Tactic:
obtain ⟨t, z, hz, rfl⟩ := exists_smul_add_of_span_sup_eq_top hxI y

Premises used: LieSubmodule.exists_smul_add_of_span_sup_eq_top, rfl
-- 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 : LieSubmodule R L M
n : M
hn : n ∈ N
t : R
z : L
hz : z ∈ I
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⁆
⊢ ⁅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:
simp only [SetLike.mem_coe, Submodule.span_union, Submodule.mem_sup]

Premises used: Submodule.span_union, SetLike.mem_coe, Submodule.mem_sup
-- 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 : LieSubmodule R L M
n : M
hn : n ∈ N
t : R
z : L
hz : z ∈ I
⊢ t • ⁅x, n⁆ + ⁅z, n⁆ = ⁅t • x + z, n⁆

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 = ⊤
N : LieSubmodule R L M
n : M
hn : n ∈ N
t : R
z : L
hz : z ∈ I
⊢ ∃ (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:
exact
      ⟨t • ⁅x, n⁆, Submodule.subset_span ⟨t • n, N.smul_mem' t hn, lie_smul t x n⟩, ⁅z, n⁆,
        Submodule.subset_span ⟨z, hz, n, hn, rfl⟩, by 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 = ⊤
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)
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⁆
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x} z

Tactic:
rcases hz with (⟨m, hm, rfl⟩ | ⟨y, -, m, hm, rfl⟩)

Premises used: rfl
-- 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 : LieSubmodule R L M
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:
⟨x, m, hm, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- 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 : LieSubmodule R L M
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:
⟨y, m, hm, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- 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 : LieSubmodule R L M
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:
exacts [⟨x, m, hm, rfl⟩, ⟨y, m, hm, rfl⟩]
-- 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)
this :
  ∀ (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)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (i + n)) (I.lcs M (j + 1))

Tactic:
simpa only [bot_sup_eq, LieIdeal.incl_coe, Submodule.map_zero, hxn] using this n

Premises used: LieIdeal.incl_coe, bot_sup_eq, Submodule.map_zero
-- 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 : _root_.LieIdeal R L
x : L
hxI : R ∙ x ⊔ (_root_.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 :
  ∀ (l : ℕ),
    (↑(_root_.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) (lowerCentralSeries R L M (i + n)) (I.lcs M (j + 1))

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
-- 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)
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))
⊢ (↑(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:
simp only [add_zero, LieIdeal.lcs_succ, pow_zero, Module.End.one_eq_id,
      Submodule.map_id]

Premises used: Module.End.one_eq_id, Submodule.map_id, LieIdeal.lcs_succ, pow_zero, add_zero
-- 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)
⊢ 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:
le_sup_of_le_left hIM

Premises used: le_sup_of_le_left
-- 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)
⊢ 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:
exact le_sup_of_le_left hIM

Premises used: le_sup_of_le_left