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
inst_6 : LieModule R L M
inst_7 : IsNilpotent L M
x : L
h :
  ∀ (m : M),
    Membership.mem (γ := Submodule R M)
        (Module.End.maxGenEigenspace
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) 0)
        m ↔
      Membership.mem (γ := Submodule R M) ⊤ m
⊢ Eq.{w + 1} (α := Submodule R M)
    (Module.End.maxGenEigenspace (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x)
      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 : L
m : M
h :
  ∃ (k : ℕ),
    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 : M)
⊢ Membership.mem (γ := Submodule R M)
      (Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) 0)
      m ↔
    Membership.mem (γ := Submodule R M) ⊤ m

Tactic:
simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, Submodule.mem_top,
    iff_true]

Premises used: sub_zero, iff_true, zero_smul, Module.End.mem_maxGenEigenspace, Submodule.mem_top
-- 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
m : M
h :
  ∀ (k : ℕ)
    (hk :
      ∀ (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 : ℕ),
      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 : M)
⊢ ∃ (k : ℕ),
    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 : M)

Tactic:
obtain ⟨k, hk⟩ := exists_forall_pow_toEnd_eq_zero R L M

Premises used: LieModule.exists_forall_pow_toEnd_eq_zero
-- 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
m : M
k : ℕ
hk :
  ∀ (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
⊢ 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 : M)

Tactic:
simp [hk x]
-- 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
m : M
k : ℕ
hk :
  ∀ (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 : ℕ),
    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 : M)

Tactic:
exact ⟨k, by simp [hk x]⟩
-- 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
h₂ : IsNilpotent.{v, w} L (M ⧸ N)
rw :
  ∀ (h₂ : ∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥),
    ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ IsNilpotent L M

Tactic:
rw [isNilpotent_iff R L] at h₂ ⊢

Premises used: LieModule.isNilpotent_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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
h₂ : ∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
obtain :
  ∀ (k : ℕ) (hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥),
    ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
obtain ⟨k, hk⟩ := h₂
-- 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
use k + 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
inst_6 : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
h : Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) ⊥

Tactic:
simp only [lowerCentralSeries_succ]

Premises used: LieModule.lowerCentralSeries_succ
-- 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
this : lowerCentralSeries R L M k ≤ N
⊢ LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (maxTrivSubmodule R L M))

Tactic:
replace this := LieSubmodule.mono_lie_right ⊤ (le_trans this h₁)
-- 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
this :
  LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (maxTrivSubmodule R L M))
rwa :
  ∀
    (this :
      LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥),
    Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥),
    Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
⊢ Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥

Tactic:
rwa [ideal_oper_maxTrivSubmodule_eq_bot, le_bot_iff] at this

Premises used: le_bot_iff, LieModule.ideal_oper_maxTrivSubmodule_eq_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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
h : lowerCentralSeries R L M k ≤ N
⊢ Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥

Tactic:
suffices lowerCentralSeries R L M k ≤ N by
    replace this := LieSubmodule.mono_lie_right ⊤ (le_trans this h₁)
    rwa [ideal_oper_maxTrivSubmodule_eq_bot, le_bot_iff] at this
-- 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
h :
  LE.le (α := LieSubmodule R L (M ⧸ N)) (LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k))
    (lowerCentralSeries R L (M ⧸ N) k)
⊢ lowerCentralSeries R L M k ≤ N

Tactic:
rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, ← le_bot_iff, ← hk]

Premises used: le_bot_iff, LieSubmodule.Quotient.map_mk'_eq_bot_le
-- 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
⊢ LE.le (α := LieSubmodule R L (M ⧸ N)) (LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k))
    (lowerCentralSeries R L (M ⧸ N) k)

Tactic:
map_lowerCentralSeries_le k (LieSubmodule.Quotient.mk' N)

Premises used: LieSubmodule.Quotient.mk', LieModule.map_lowerCentralSeries_le
-- 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
⊢ LE.le (α := LieSubmodule R L (M ⧸ N)) (LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k))
    (lowerCentralSeries R L (M ⧸ N) k)

Tactic:
exact map_lowerCentralSeries_le k (LieSubmodule.Quotient.mk' N)

Premises used: LieSubmodule.Quotient.mk', LieModule.map_lowerCentralSeries_le
-- 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
rw :
  (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥) ↔
    ∃ (k : ℕ), lowerCentralSeries R L M k ≤ N
⊢ IsNilpotent.{v, w} L (M ⧸ N) ↔ ∃ (k : ℕ), lowerCentralSeries R L M k ≤ N

Tactic:
rw [isNilpotent_iff R L]

Premises used: LieModule.isNilpotent_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
N : LieSubmodule R L M
inst_6 : LieModule R L M
⊢ (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥) ↔
    ∃ (k : ℕ), lowerCentralSeries R L M k ≤ N

Tactic:
exists_congr fun k ↦ ?_

Premises used: exists_congr
-- 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
refine :
  ∀ (k : ℕ),
    Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔ lowerCentralSeries R L M k ≤ N
⊢ (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥) ↔
    ∃ (k : ℕ), lowerCentralSeries R L M k ≤ N

Tactic:
refine exists_congr fun k ↦ ?_

Premises used: exists_congr
-- 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
rw :
  Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔
    Eq (α := LieSubmodule R L (M ⧸ N)) (LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k)) ⊥
rw₁ rw₂ :
  Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔
    Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔ lowerCentralSeries R L M k ≤ N

Tactic:
rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, map_lowerCentralSeries_eq k
    (LieSubmodule.Quotient.surjective_mk' N)]

Premises used: LieSubmodule.Quotient.map_mk'_eq_bot_le, LieSubmodule.Quotient.surjective_mk', LieModule.map_lowerCentralSeries_eq
-- 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
h : IsNilpotent.{v, w} L (M ⧸ N)
obtain : ∀ (k : ℕ) (hk : lowerCentralSeries R L M k ≤ N), ⨅ (k : ℕ), lowerCentralSeries R L M k ≤ N
⊢ ⨅ (k : ℕ), lowerCentralSeries R L M k ≤ N

Tactic:
obtain ⟨k, hk⟩ := (isNilpotent_quotient_iff R L M N).mp h

Premises used: LieModule.isNilpotent_quotient_iff, Iff.mp
-- 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
h : IsNilpotent.{v, w} L (M ⧸ N)
k : ℕ
hk : lowerCentralSeries R L M k ≤ N
⊢ ⨅ (k : ℕ), lowerCentralSeries R L M k ≤ N

Tactic:
iInf_le_of_le k hk

Premises used: Set.Mem, iInf_le_of_le
-- 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
h : IsNilpotent.{v, w} L (M ⧸ N)
k : ℕ
hk : lowerCentralSeries R L M k ≤ N
⊢ ⨅ (k : ℕ), lowerCentralSeries R L M k ≤ N

Tactic:
exact iInf_le_of_le k hk

Premises used: iInf_le_of_le
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
obtain : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥), s.Nonempty
⊢ s.Nonempty

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

Premises used: LieModule.IsNilpotent.nilpotent, Int
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
k : ℕ
hk : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
⊢ s.Nonempty

Tactic:
⟨k, hk⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
k : ℕ
hk : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
⊢ s.Nonempty

Tactic:
exact ⟨k, hk⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
⊢ s.Nonempty

Tactic:
have hs : s.Nonempty := by
    obtain ⟨k, hk⟩ := IsNilpotent.nilpotent ℤ L M
    exact ⟨k, hk⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
change : sInf s = 0 ↔ Subsingleton M
⊢ nilpotencyLength L M = 0 ↔ Subsingleton M

Tactic:
change sInf s = 0 ↔ _

Premises used: InfSet.sInf
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
rw : sInf s = 0 ↔ Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥
⊢ sInf s = 0 ↔ Subsingleton M

Tactic:
rw [← LieSubmodule.subsingleton_iff ℤ L M, ← subsingleton_iff_bot_eq_top, ←
    lowerCentralSeries_zero, @eq_comm (LieSubmodule ℤ L M)]

Premises used: LieModule.lowerCentralSeries_zero, Int, eq_comm, subsingleton_iff_bot_eq_top, LieSubmodule.subsingleton_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥

Tactic:
⟨fun h => h ▸ Nat.sInf_mem hs, fun h => ?_⟩

Premises used: Nat.sInf_mem, Eq.rec, Iff.intro
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
refine : ∀ (h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥), sInf s = 0
⊢ sInf s = 0 ↔ Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥

Tactic:
refine ⟨fun h => h ▸ Nat.sInf_mem hs, fun h => ?_⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥
rw : 0 ∈ s ∨ s = ∅
⊢ sInf s = 0

Tactic:
rw [Nat.sInf_eq_zero]

Premises used: Nat.sInf_eq_zero
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥
⊢ 0 ∈ s ∨ s = ∅

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥
⊢ 0 ∈ s ∨ s = ∅

Tactic:
exact Or.inl h

Premises used: Or.inl
-- 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
k_1 k : ℕ
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
    Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥

Tactic:
simp [SetLike.ext'_iff, coe_lowerCentralSeries_eq_int R L M]

Premises used: LieModule.coe_lowerCentralSeries_eq_int, SetLike.ext'_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
k : ℕ
⊢ ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥

Tactic:
have aux (k : ℕ) : lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥ := by
    simp [SetLike.ext'_iff, coe_lowerCentralSeries_eq_int 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
k : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
rw :
  nilpotencyLength L M = k + 1 ↔
    Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M (k + 1)) ⊥ ∧
      ¬Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
⊢ nilpotencyLength L M = k + 1 ↔
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) ⊥ ∧
      Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
rw [aux, ne_eq, aux]

Premises used: ne_eq
-- 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
k : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
change : sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
⊢ nilpotencyLength L M = k + 1 ↔
    Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M (k + 1)) ⊥ ∧
      ¬Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥

Tactic:
change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Premises used: InfSet.sInf
-- 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
k : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k₁) ⊥
⊢ k₂ ∈ s

Tactic:
eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries ℤ L M h₁₂)

Premises used: Iff.mpr, Set.Mem, setOf, Eq.rec, Int, LieModule.antitone_lowerCentralSeries, eq_bot_iff