awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
⊢ ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'

Tactic:
have : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K' := by
    rintro K (hK₁ : LieAlgebra.IsEngelian R K) hK₂
    apply LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer hK₁
    apply lt_of_le_of_ne K.le_normalizer
    rw [Ne, eq_comm, K.normalizer_eq_self_iff, ← Ne, ←
      LieSubmodule.nontrivial_iff_ne_bot R K]
    have : Nontrivial (L' ⧸ K.toLieSubmodule) := Submodule.Quotient.nontrivial_iff.2 <| by simpa
    have : LieModule.IsNilpotent K (L' ⧸ K.toLieSubmodule) := by
      refine hK₁ _ fun x => ?_
      have hx := LieAlgebra.isNilpotent_ad_of_isNilpotent (h x)
      apply Module.End.IsNilpotent.mapQ ?_ hx
      intro X HX
      simp only [LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.mem_toSubmodule] at HX
      simp only [LieSubalgebra.coe_toLieSubmodule, Submodule.mem_comap, ad_apply,
        LieSubalgebra.mem_toSubmodule]
      exact LieSubalgebra.lie_mem K x.prop HX
    exact nontrivial_max_triv_of_isNilpotent R K (L' ⧸ K.toLieSubmodule)
-- 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 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ IsNoetherian.{u₁, u_1} R ↥L'

Tactic:
isNoetherian_of_surjective (LieHom.rangeRestrict (toEnd R L M)).toLinearMap ?_

Premises used: LieHom.rangeRestrict, isNoetherian_of_surjective, LieModule.toEnd, LieHom.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
inst_3 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
refine :
  Eq (α := Submodule R ↥L') (LinearMap.range (↑(LieHom.rangeRestrict (toEnd R L M)) : L →ₗ[R] ↥(toEnd R L M).range)) ⊤
⊢ IsNoetherian.{u₁, u_1} R ↥L'

Tactic:
refine isNoetherian_of_surjective (LieHom.rangeRestrict (toEnd R L M)).toLinearMap ?_

Premises used: LieHom.rangeRestrict, isNoetherian_of_surjective, LieModule.toEnd, LieHom.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
inst_3 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
simp :
  Function.Surjective.{u₂ + 1, u_1 + 1} (α := L) (β := ↥L')
    (⇑(↑(LieHom.rangeRestrict (toEnd R L M)) : L →ₗ[R] ↥(toEnd R L M).range) : (a : L) → ↥L')
⊢ Eq (α := Submodule R ↥L') (LinearMap.range (↑(LieHom.rangeRestrict (toEnd R L M)) : L →ₗ[R] ↥(toEnd R L M).range)) ⊤

Tactic:
simp only [LinearMap.range_eq_top]

Premises used: LinearMap.range_eq_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
inst_3 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ Function.Surjective.{u₂ + 1, u_1 + 1} (α := L) (β := ↥L')
    (⇑(↑(LieHom.rangeRestrict (toEnd R L M)) : L →ₗ[R] ↥(toEnd R L M).range) : (a : L) → ↥L')

Tactic:
LieHom.surjective_rangeRestrict (toEnd R L M)

Premises used: LieHom.surjective_rangeRestrict, Set.Mem, LieModule.toEnd
-- 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 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ Function.Surjective.{u₂ + 1, u_1 + 1} (α := L) (β := ↥L')
    (⇑(↑(LieHom.rangeRestrict (toEnd R L M)) : L →ₗ[R] ↥(toEnd R L M).range) : (a : L) → ↥L')

Tactic:
exact LieHom.surjective_rangeRestrict (toEnd R L M)

Premises used: LieHom.surjective_rangeRestrict, LieModule.toEnd
-- 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 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ IsNoetherian.{u₁, u_1} R ↥L'

Tactic:
haveI _i5 : IsNoetherian R L' := by
    refine isNoetherian_of_surjective (LieHom.rangeRestrict (toEnd R L M)).toLinearMap ?_
    simp only [LinearMap.range_eq_top]
    exact LieHom.surjective_rangeRestrict (toEnd R L M)
-- 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 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian.{u₁, u_1} R ↥L'
obtain : ∀ (K : LieSubalgebra R ↥L') (hK₁ : K ∈ s) (hK₂ : ∀ x ∈ s, ¬K < x), ⊤ ∈ s
⊢ ⊤ ∈ s

Tactic:
obtain ⟨K, hK₁, hK₂⟩ := (LieSubalgebra.wellFoundedGT_of_noetherian R L').wf.has_min s hs

Premises used: IsWellFounded.wf, WellFounded.has_min
-- 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 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian.{u₁, u_1} R ↥L'
K : LieSubalgebra R ↥L'
hK₁ : K ∈ s
hK₂ : ∀ x ∈ s, ¬K < x
⊢ K = ⊤

Tactic:
grind
-- 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 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian.{u₁, u_1} R ↥L'
K : LieSubalgebra R ↥L'
hK₁ : K ∈ s
hK₂ : ∀ x ∈ s, ¬K < x
⊢ ⊤ ∈ s

Tactic:
obtain rfl : K = ⊤ := by grind

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
inst_3 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian.{u₁, u_1} R ↥L'
K : LieSubalgebra R ↥L'
hK₁ : K ∈ s
hK₂ : ∀ x ∈ s, ¬K < x
hK₃ : ⊤ ∈ s
⊢ ∀ x ∈ s, ¬⊤ < x

Tactic:
obtain rfl : K = ⊤ := by grind

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
inst_3 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian.{u₁, u_1} R ↥L'
hK₁ : ⊤ ∈ s
hK₂ : ∀ x ∈ s, ¬⊤ < x
⊢ ⊤ ∈ s

Tactic:
hK₁
-- 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 : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEnd R L M)
h : ∀ (y : ↥L'), IsNilpotent (↑y : Module.End R M)
s : Set (LieSubalgebra R ↥L') := {K : LieSubalgebra R ↥L' | IsEngelian.{u₁, u_1, u_1} R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian.{u₁, u_1} R ↥L'
hK₁ : ⊤ ∈ s
hK₂ : ∀ x ∈ s, ¬⊤ < x
⊢ ⊤ ∈ s

Tactic:
exact hK₁
-- 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
inst_7 : IsNoetherian R L
⊢ IsNilpotent L M ↔
    ∀ (x : L),
      _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)

Tactic:
⟨fun _ ↦ isNilpotent_toEnd_of_isNilpotent R L M,
   fun h => LieAlgebra.isEngelian_of_isNoetherian M h⟩

Premises used: LieModule.isNilpotent_toEnd_of_isNilpotent, LieAlgebra.isEngelian_of_isNoetherian, Iff.intro
-- 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
inst_7 : IsNoetherian R M
rw :
  (∀ (x : ↥(LieHom.range (toEnd R L M))),
      _root_.IsNilpotent (R := Module.End R M)
        ((toEnd R (↥(LieHom.range (toEnd R L M))) M : (a : ↥(toEnd R L M).range) → Module.End R M) x :
          Module.End R M)) ↔
    ∀ (x : L),
      _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)
⊢ IsNilpotent L M ↔
    ∀ (x : L),
      _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)

Tactic:
rw [← isNilpotent_range_toEnd_iff (R := R), LieModule.isNilpotent_iff_forall (R := R)]

Premises used: LieModule.isNilpotent_range_toEnd_iff, LieModule.isNilpotent_iff_forall
-- 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
inst_7 : IsNoetherian R M
⊢ (∀ (x : ↥(LieHom.range (toEnd R L M))),
      _root_.IsNilpotent (R := Module.End R M)
        ((toEnd R (↥(LieHom.range (toEnd R L M))) M : (a : ↥(toEnd R L M).range) → Module.End R M) x :
          Module.End R M)) ↔
    ∀ (x : L),
      _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)

Tactic:
simp
-- 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 : IsNoetherian R L
⊢ LieRing.IsNilpotent L ↔
    ∀ (x : L), IsNilpotent (R := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L)

Tactic:
LieModule.isNilpotent_iff_forall

Premises used: LieModule.isNilpotent_iff_forall
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x : L
simp :
  ∀ {x_1 y : L} (x_2 : ℕ)
    (h :
      Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_2 : (a : L) → L)
            x_1 :
          L)
        (0 : L))
    (x_3 : ℕ)
    (h :
      Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_3 : (a : L) → L)
            y :
          L)
        (0 : L)),
    ∃ (k : ℕ),
      Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) k : (a : L) → L)
            ⁅x_1, y⁆ :
          L)
        (0 : L)
⊢ ∀ {x_1 y : L},
    Membership.mem (γ := Set L)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_1, u_2} (R := R)
              (Module.End.maxGenEigenspace ((ad R L : (a : L) → Module.End R L) x) 0))))
        x_1 →
      Membership.mem (γ := Set L)
          (AddSubsemigroup.carrier
            (AddSubmonoid.toAddSubsemigroup
              (Submodule.toAddSubmonoid.{u_1, u_2} (R := R)
                (Module.End.maxGenEigenspace ((ad R L : (a : L) → Module.End R L) x) 0))))
          y →
        Membership.mem (γ := Set L)
          (AddSubsemigroup.carrier
            (AddSubmonoid.toAddSubsemigroup
              (Submodule.toAddSubmonoid.{u_1, u_2} (R := R)
                (Module.End.maxGenEigenspace ((ad R L : (a : L) → Module.End R L) x) 0))))
          ⁅x_1, y⁆

Tactic:
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid, Module.End.mem_maxGenEigenspace, zero_smul,
        sub_zero, forall_exists_index]

Premises used: sub_zero, forall_exists_index, AddSubsemigroup.mem_carrier, zero_smul, Submodule.mem_toAddSubmonoid, Module.End.mem_maxGenEigenspace, AddSubmonoid.mem_toSubsemigroup
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) m : (a : L) → L) y : L)
    (0 : L)
n : ℕ
hn :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L) z : L)
    (0 : L)
⊢ ∃ (k : ℕ),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) k : (a : L) → L)
          ⁅y, z⁆ :
        L)
      (0 : L)

Tactic:
⟨m + n, ?_⟩

Premises used: HAdd.hAdd, Exists.intro
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) m : (a : L) → L) y : L)
    (0 : L)
n : ℕ
hn :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L) z : L)
    (0 : L)
refine :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (m + n) : (a : L) → L)
        ⁅y, z⁆ :
      L)
    (0 : L)
⊢ ∃ (k : ℕ),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) k : (a : L) → L)
          ⁅y, z⁆ :
        L)
      (0 : L)

Tactic:
refine ⟨m + n, ?_⟩
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) m : (a : L) → L) y : L)
    (0 : L)
n : ℕ
hn :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L) z : L)
    (0 : L)
rw :
  Eq.{u_2 + 1} (α := L)
    (∑ ij ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n),
      HSMul.hSMul (β := L) ((m + n).choose ij.1)
        (Bracket.bracket (L := L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                  (a : L) → L)
                y :
              L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.2 :
                (a : L) → L)
              z) :
          L))
    0
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (m + n) : (a : L) → L)
        ⁅y, z⁆ :
      L)
    (0 : L)

Tactic:
rw [ad_pow_lie]

Premises used: LieAlgebra.ad_pow_lie
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) m : (a : L) → L) y : L)
    (0 : L)
n : ℕ
hn :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L) z : L)
    (0 : L)
h :
  ∀ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n),
    HSMul.hSMul (β := L) ((m + n).choose x_1.1)
        (Bracket.bracket (L := L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_1.1 :
                  (a : L) → L)
                y :
              L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_1.2 :
                (a : L) → L)
              z) :
          L) =
      0
⊢ Eq.{u_2 + 1} (α := L)
    (∑ ij ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n),
      HSMul.hSMul (β := L) ((m + n).choose ij.1)
        (Bracket.bracket (L := L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                  (a : L) → L)
                y :
              L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.2 :
                (a : L) → L)
              z) :
          L))
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) m : (a : L) → L) y : L)
    (0 : L)
n : ℕ
hn :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L) z : L)
    (0 : L)
ij : ℕ × ℕ
hij : ij ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n)
⊢ ij.1 + ij.2 = m + n

Tactic:
rw [Finset.mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) m : (a : L) → L) y : L)
    (0 : L)
n : ℕ
hn :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L) z : L)
    (0 : L)
ij : ℕ × ℕ
hij : ij.1 + ij.2 = m + n
⊢ m ≤ ij.1 ∨ n ≤ ij.2

Tactic:
lia
-- Module: Mathlib.Algebra.Lie.EngelSubalgebra
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) m : (a : L) → L) y : L)
    (0 : L)
n : ℕ
hn :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) n : (a : L) → L) z : L)
    (0 : L)
ij : ℕ × ℕ
hij : ij ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (m + n)
h :
  ∀ (h : m ≤ ij.1),
    HSMul.hSMul (β := L) ((m + n).choose ij.1)
        (Bracket.bracket (L := L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                  (a : L) → L)
                y :
              L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.2 :
                (a : L) → L)
              z) :
          L) =
      0
h₁ :
  ∀ (h : n ≤ ij.2),
    HSMul.hSMul (β := L) ((m + n).choose ij.1)
        (Bracket.bracket (L := L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                  (a : L) → L)
                y :
              L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.2 :
                (a : L) → L)
              z) :
          L) =
      0
⊢ HSMul.hSMul (β := L) ((m + n).choose ij.1)
      (Bracket.bracket (L := L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 : (a : L) → L)
              y :
            L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.2 : (a : L) → L)
            z) :
        L) =
    0

Tactic:
obtain (h | h) : m ≤ ij.1 ∨ n ≤ ij.2 := by rw [Finset.mem_antidiagonal] at hij; lia

Premises used: Prod.fst, Prod.snd