awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
inst_11 : IsTrivial L M
h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 1) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥

Tactic:
use 1
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
inst_11 : IsTrivial L M
⊢ Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 1) ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
obtain :
  ∀ (k : ℕ) (hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥),
    IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)
⊢ IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)

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

Premises used: Membership.mem, LieModule.IsNilpotent.nilpotent, Subtype
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
obtain :
  ∀ (l : ℕ) (hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥),
    IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)
⊢ IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)

Tactic:
obtain ⟨l, hl⟩ := IsNilpotent.nilpotent R L M₂

Premises used: Membership.mem, LieModule.IsNilpotent.nilpotent, Subtype
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k_1 : ℕ
N_1 : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
l : ℕ
hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥
m n : ℕ
N : LieSubmodule R L M
le : m ≤ n
hn : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) m) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) n) ⊥

Tactic:
simpa [hn] using antitone_lowerCentralSeries R L N le

Premises used: Membership.mem, Subtype, LieModule.antitone_lowerCentralSeries
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
l : ℕ
hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M) (le : m ≤ n)
  (hn : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) m) ⊥),
  Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) n) ⊥ :=
  ⋯
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) (max k l)) ⊥

Tactic:
have h₁ : lowerCentralSeries R L M₁ (k ⊔ l) = ⊥ := lcs_eq_bot M₁ (Nat.le_max_left k l) hk
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
l : ℕ
hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M) (le : m ≤ n)
  (hn : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) m) ⊥),
  Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) n) ⊥ :=
  ⋯
h₁ : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) (max k l)) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) (max k l)) ⊥

Tactic:
have h₂ : lowerCentralSeries R L M₂ (k ⊔ l) = ⊥ := lcs_eq_bot M₂ (Nat.le_max_right k l) hl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
l : ℕ
hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M) (le : m ≤ n)
  (hn : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) m) ⊥),
  Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) n) ⊥ :=
  ⋯
h₁ : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) (max k l)) ⊥
h₂ : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) (max k l)) ⊥
⊢ IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)

Tactic:
(isNilpotent_iff R L (M₁ + M₂)).mpr ⟨k ⊔ l, ?_⟩

Premises used: Iff.mpr, Set.Mem, LieModule.isNilpotent_iff, Membership.mem, Subtype, HAdd.hAdd, Max.max, Exists.intro
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
l : ℕ
hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M) (le : m ≤ n)
  (hn : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) m) ⊥),
  Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) n) ⊥ :=
  ⋯
h₁ : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) (max k l)) ⊥
h₂ : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) (max k l)) ⊥
refine : Eq.{w + 1} (α := LieSubmodule R L ↥(M₁ + M₂)) (lowerCentralSeries R L (↥(M₁ + M₂)) (max k l)) ⊥
⊢ IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)

Tactic:
refine (isNilpotent_iff R L (M₁ + M₂)).mpr ⟨k ⊔ l, ?_⟩

Premises used: Iff.mpr, LieModule.isNilpotent_iff, Membership.mem, Subtype, HAdd.hAdd, Max.max, Exists.intro
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
l : ℕ
hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M) (le : m ≤ n)
  (hn : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) m) ⊥),
  Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) n) ⊥ :=
  ⋯
h₁ : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) (max k l)) ⊥
h₂ : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) (max k l)) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥(M₁ + M₂)) (lowerCentralSeries R L (↥(M₁ + M₂)) (max k l)) ⊥

Tactic:
simp [LieSubmodule.add_eq_sup, (M₁ ⊔ M₂).lowerCentralSeries_eq_lcs_comap, LieSubmodule.lcs_sup,
    (M₁.lowerCentralSeries_eq_bot_iff_lcs_eq_bot (k ⊔ l)).1 h₁,
    (M₂.lowerCentralSeries_eq_bot_iff_lcs_eq_bot (k ⊔ l)).1 h₂, LieSubmodule.comap_incl_eq_bot]

Premises used: LieSubmodule.lcs_sup, LieSubmodule.lowerCentralSeries_eq_bot_iff_lcs_eq_bot, LieSubmodule.comap_incl_eq_bot, LieSubmodule.lowerCentralSeries_eq_lcs_comap, Max.max, Iff.mp, LieSubmodule.add_eq_sup
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
obtain :
  ∀ (k : ℕ) (hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥),
    ∃ (k : ℕ),
      ∀ (x : L),
        HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
          0
⊢ ∃ (k : ℕ),
    ∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0

Tactic:
obtain ⟨k, hM⟩ := IsNilpotent.nilpotent R L M

Premises used: LieModule.IsNilpotent.nilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
h :
  ∀ (x : L),
    HPow.hPow (α := Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
      0
⊢ ∃ (k : ℕ),
    ∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0

Tactic:
use k
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
x : L
h :
  ∀ (m : M),
    Eq (α := M)
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
              k :
            (a : M) → M)
          m :
        M)
      ((0 : (a : M) → M) m : M)
⊢ HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
    0

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
x : L
m : M
h :
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k)
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[k]
      m)
⊢ Eq (α := M)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k :
          (a : M) → M)
        m :
      M)
    ((0 : (a : M) → M) m : M)

Tactic:
rw [Module.End.pow_apply, LinearMap.zero_apply, ← @LieSubmodule.mem_bot R L M, ← hM]

Premises used: LinearMap.zero_apply, Module.End.pow_apply, LieSubmodule.mem_bot
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
x : L
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k)
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[k]
      m)

Tactic:
iterate_toEnd_mem_lowerCentralSeries R L M x m k

Premises used: LieModule.iterate_toEnd_mem_lowerCentralSeries
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
x : L
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k)
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[k]
      m)

Tactic:
exact iterate_toEnd_mem_lowerCentralSeries R L M x m k

Premises used: LieModule.iterate_toEnd_mem_lowerCentralSeries
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x : L
⊢ ∃ (k : ℕ),
    ∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0

Tactic:
have := exists_forall_pow_toEnd_eq_zero R L M
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x : L
this :
  ∃ (k : ℕ),
    ∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : ℕ),
    (∀ (x : L),
        HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) w =
          0) →
      ∃ (k : ℕ),
        HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
          0
⊢ ∃ (k : ℕ),
    HPow.hPow (α := Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
      0

Tactic:
tauto
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
obtain :
  ∀ (k : ℕ) (hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥),
    _root_.IsNilpotent.{w} (R := M →ₗ[R] M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
        ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
⊢ _root_.IsNilpotent.{w} (R := M →ₗ[R] M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
      ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)

Tactic:
obtain ⟨k, hM⟩ := IsNilpotent.nilpotent R L M

Premises used: LieModule.IsNilpotent.nilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
rw : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) (lowerCentralSeries R L M k)
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥

Tactic:
rw [eq_bot_iff, ← hM]

Premises used: eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ k ≤ 2 * k

Tactic:
lia
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) (lowerCentralSeries R L M k)

Tactic:
exact antitone_lowerCentralSeries R L M (by lia)

Premises used: LieModule.antitone_lowerCentralSeries
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥

Tactic:
replace hM : lowerCentralSeries R L M (2 * k) = ⊥ := by
    rw [eq_bot_iff, ← hM]; exact antitone_lowerCentralSeries R L M (by lia)
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
h :
  HPow.hPow (α := M →ₗ[R] M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
        ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
      k =
    0
⊢ _root_.IsNilpotent.{w} (R := M →ₗ[R] M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
      ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)

Tactic:
use k
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
h :
  ∀ (m : M),
    Eq (α := M)
      ((HPow.hPow (α := M →ₗ[R] M)
              (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
                ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
              k :
            (a : M) → M)
          m :
        M)
      ((0 : (a : M) → M) m : M)
⊢ HPow.hPow (α := M →ₗ[R] M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
        ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
      k =
    0

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
m : M
h :
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k]
      m)
⊢ Eq (α := M)
    ((HPow.hPow (α := M →ₗ[R] M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
            k :
          (a : M) → M)
        m :
      M)
    ((0 : (a : M) → M) m : M)

Tactic:
rw [Module.End.pow_apply, LinearMap.zero_apply, ← LieSubmodule.mem_bot (R := R) (L := L), ← hM]

Premises used: LinearMap.zero_apply, Module.End.pow_apply, LieSubmodule.mem_bot
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k]
      m)

Tactic:
iterate_toEnd_mem_lowerCentralSeries₂ R L M x y m k

Premises used: Set.Mem, LieModule.iterate_toEnd_mem_lowerCentralSeries₂
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
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 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k]
      m)

Tactic:
exact iterate_toEnd_mem_lowerCentralSeries₂ R L M x y m k

Premises used: LieModule.iterate_toEnd_mem_lowerCentralSeries₂