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
x y : L
m : M
k : ℕ
ih :
  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)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ Membership.mem (γ := LieSubmodule R L M)
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M (2 * k)))
    ⁅y,
      (Function.comp (β := 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) :
              (a : M) → M)
            (⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M) :
              (a : M) → M))^[k]
        m⁆

Tactic:
LieSubmodule.lie_mem_lie (LieSubmodule.mem_top y) ih

Premises used: LieSubmodule.lie_mem_lie, LieSubmodule.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
x y : L
m : M
k : ℕ
ih :
  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)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ Membership.mem (γ := LieSubmodule R L M)
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M (2 * k)))
    ⁅y,
      (Function.comp (β := 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) :
              (a : M) → M)
            (⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M) :
              (a : M) → M))^[k]
        m⁆

Tactic:
exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top y) ih

Premises used: LieSubmodule.lie_mem_lie, LieSubmodule.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
x y : L
m : M
k : ℕ
zero :
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (HMul.hMul (α := ℕ) 2 0))
    ((⇑(((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)^[0]
      m)
succ :
  ∀ (k : ℕ)
    (ih :
      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)),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * (k + 1)))
      ((⇑(((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 + 1]
        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:
induction k with
  | zero => simp
  | succ k ih =>
    have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
    simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
      toEnd_apply_apply, LinearMap.coe_comp, toEnd_apply_apply]
    refine LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_
    exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top y) ih

Premises used: Function.iterate_succ', LieModule.lowerCentralSeries_succ, LieModule.toEnd_apply_apply, LieSubmodule.lie_mem_lie, LinearMap.coe_comp, LieSubmodule.mem_top, Function.comp_apply
-- 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 : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map f (lowerCentralSeries R L M 0) ≤ lowerCentralSeries R L M₂ 0

Tactic:
simp only [lowerCentralSeries_zero, le_top]

Premises used: LieModule.lowerCentralSeries_zero, le_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
k_1 : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
succ :
  Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (LieSubmodule.map f (lowerCentralSeries R L M k)) ≤
    Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M₂ k)
⊢ LieSubmodule.map f (lowerCentralSeries R L M (k + 1)) ≤ lowerCentralSeries R L M₂ (k + 1)

Tactic:
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]

Premises used: LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_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
k_1 : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
⊢ Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (LieSubmodule.map f (lowerCentralSeries R L M k)) ≤
    Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M₂ k)

Tactic:
LieSubmodule.mono_lie_right ⊤ ih

Premises used: LieSubmodule.mono_lie_right, Top.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
k_1 : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
⊢ Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (LieSubmodule.map f (lowerCentralSeries R L M k)) ≤
    Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M₂ k)

Tactic:
exact LieSubmodule.mono_lie_right ⊤ ih

Premises used: LieSubmodule.mono_lie_right, Top.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
k : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
zero : LieSubmodule.map f (lowerCentralSeries R L M 0) ≤ lowerCentralSeries R L M₂ 0
succ :
  ∀ (k : ℕ) (ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k),
    LieSubmodule.map f (lowerCentralSeries R L M (k + 1)) ≤ lowerCentralSeries R L M₂ (k + 1)
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k

Tactic:
induction k with
  | zero => simp only [lowerCentralSeries_zero, le_top]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    exact LieSubmodule.mono_lie_right ⊤ ih

Premises used: LieModule.lowerCentralSeries_zero, LieModule.lowerCentralSeries_succ, le_top, LieSubmodule.map_bracket_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
k : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
apply : lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) = lowerCentralSeries R L M₂ k

Tactic:
apply le_antisymm (map_lowerCentralSeries_le k f)

Premises used: le_antisymm, 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
k : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
zero : ⊤ ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
zero₁ : ⊤ ≤ LieSubmodule.map f ⊤
zero₂ : LieSubmodule.map f ⊤ = ⊤
zero₃ : f.range = ⊤
zero₄ zero₅ zero₆ zero₇ : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ lowerCentralSeries R L M₂ 0 ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)

Tactic:
rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
      f.range_eq_top]

Premises used: LieModule.lowerCentralSeries_zero, LieModuleHom.range_eq_top, top_le_iff, LieModuleHom.map_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
k : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
n : ℕ
h : lowerCentralSeries R L M₂ n ≤ LieSubmodule.map f (lowerCentralSeries R L M n)
succ :
  Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M₂ n) ≤
    Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (LieSubmodule.map f (lowerCentralSeries R L M n))
⊢ lowerCentralSeries R L M₂ (n + 1) ≤ LieSubmodule.map f (lowerCentralSeries R L M (n + 1))

Tactic:
simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]

Premises used: LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_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
k : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
n : ℕ
h succ : lowerCentralSeries R L M₂ n ≤ LieSubmodule.map f (lowerCentralSeries R L M n)
⊢ Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M₂ n) ≤
    Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (LieSubmodule.map f (lowerCentralSeries R L M n))

Tactic:
apply LieSubmodule.mono_lie_right

Premises used: LieSubmodule.mono_lie_right
-- 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 : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
n : ℕ
h : lowerCentralSeries R L M₂ n ≤ LieSubmodule.map f (lowerCentralSeries R L M n)
⊢ lowerCentralSeries R L M₂ n ≤ LieSubmodule.map f (lowerCentralSeries R L M n)

Tactic:
assumption
-- 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 : ℕ
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
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
zero : lowerCentralSeries R L M₂ 0 ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
succ :
  ∀ (n : ℕ),
    lowerCentralSeries R L M₂ n ≤ LieSubmodule.map f (lowerCentralSeries R L M n) →
      lowerCentralSeries R L M₂ (n + 1) ≤ LieSubmodule.map f (lowerCentralSeries R L M (n + 1))
⊢ lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)

Tactic:
induction k with
  | zero =>
    rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
      f.range_eq_top]
  | succ =>
    simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    apply LieSubmodule.mono_lie_right
    assumption

Premises used: LieModule.lowerCentralSeries_zero, LieModule.lowerCentralSeries_succ, LieSubmodule.mono_lie_right, LieModuleHom.range_eq_top, top_le_iff, LieSubmodule.map_bracket_eq, LieModuleHom.map_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
zero : LE.le (α := LieIdeal R L) (derivedSeriesOfIdeal R L 0 ⊤) (lowerCentralSeries R L L 0)
zero₁ : LE.le (α := LieIdeal R L) ⊤ (lowerCentralSeries R L L 0)
zero₂ zero₃ : LE.le.{v} (α := LieIdeal R L) ⊤ ⊤
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L 0) (lowerCentralSeries R L L 0)

Tactic:
rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]

Premises used: LieModule.lowerCentralSeries_zero, LieAlgebra.derivedSeries_def, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
h : LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L k) ⊤

Tactic:
simp only [le_top]

Premises used: le_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
h : LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L k) ⊤

Tactic:
have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
h : LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)
h' : LE.le (α := LieIdeal R L) (derivedSeries R L k) ⊤
succ :
  LE.le (α := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) (derivedSeriesOfIdeal R L k ⊤))
    (Bracket.bracket (L := LieIdeal R L) ⊤ (lowerCentralSeries R L L k))
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L (k + 1)) (lowerCentralSeries R L L (k + 1))

Tactic:
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]

Premises used: LieModule.lowerCentralSeries_succ, LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeries_def
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
h : LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)
h' : LE.le (α := LieIdeal R L) (derivedSeries R L k) ⊤
⊢ LE.le (α := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) (derivedSeriesOfIdeal R L k ⊤))
    (Bracket.bracket (L := LieIdeal R L) ⊤ (lowerCentralSeries R L L k))

Tactic:
LieSubmodule.mono_lie h' h

Premises used: Set.Mem, LieSubmodule.mono_lie
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
h : LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)
h' : LE.le (α := LieIdeal R L) (derivedSeries R L k) ⊤
⊢ LE.le (α := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) (derivedSeriesOfIdeal R L k ⊤))
    (Bracket.bracket (L := LieIdeal R L) ⊤ (lowerCentralSeries R L L k))

Tactic:
exact LieSubmodule.mono_lie h' h

Premises used: LieSubmodule.mono_lie
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
zero : LE.le (α := LieIdeal R L) (derivedSeries R L 0) (lowerCentralSeries R L L 0)
succ :
  ∀ (k : ℕ) (h : LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)),
    LE.le (α := LieIdeal R L) (derivedSeries R L (k + 1)) (lowerCentralSeries R L L (k + 1))
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)

Tactic:
induction k with
  | zero => rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]
  | succ k h =>
    have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]
    rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]
    exact LieSubmodule.mono_lie h' h

Premises used: LieModule.lowerCentralSeries_zero, LieModule.lowerCentralSeries_succ, LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeries_def, LieAlgebra.derivedSeriesOfIdeal_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
⊢ IsNilpotent L M ↔ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

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

Premises used: LieModule.isNilpotent_iff_int, 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
inst_7 : IsNilpotent L M
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
(isNilpotent_iff R L M).mp ‹_›

Premises used: LieModule.isNilpotent_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
inst_6 : LieModule R L M
k : ℕ
h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ IsNilpotent L M

Tactic:
(isNilpotent_iff R L M).mpr ⟨k, h⟩

Premises used: Iff.mpr, LieModule.isNilpotent_iff, 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
inst_6 : LieModule R L M
inst_7 : IsNilpotent L M
obtain :
  ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥),
    Eq.{w + 1} (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) ⊥

Tactic:
obtain ⟨k, hk⟩ := 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 : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
rw : LE.le (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M k)
⊢ Eq.{w + 1} (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) ⊥

Tactic:
rw [eq_bot_iff, ← hk]

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
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ LE.le (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M k)

Tactic:
iInf_le _ _

Premises used: Set.Mem, iInf_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
inst_7 : IsNilpotent L M
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ LE.le (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M k)

Tactic:
exact iInf_le _ _

Premises used: iInf_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
rw :
  (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥) ↔
    ∃ (k : ℕ), LieSubmodule.lcs k N = ⊥
⊢ IsNilpotent.{v, w} L ↥N ↔ ∃ (k : ℕ), LieSubmodule.lcs k N = ⊥

Tactic:
rw [isNilpotent_iff R L N]

Premises used: LieModule.isNilpotent_iff, Membership.mem, 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
inst_6 : LieModule R L M
N : LieSubmodule R L M
⊢ (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥) ↔
    ∃ (k : ℕ), LieSubmodule.lcs 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
inst_6 : LieModule R L M
N : LieSubmodule R L M
refine : ∀ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ LieSubmodule.lcs k N = ⊥
⊢ (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥) ↔
    ∃ (k : ℕ), LieSubmodule.lcs 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
inst_6 : LieModule R L M
N : LieSubmodule R L M
k : ℕ
rw : LieSubmodule.comap N.incl (LieSubmodule.lcs k N) = ⊥ ↔ LieSubmodule.lcs k N = ⊥
rw₁ : N ⊓ LieSubmodule.lcs k N = ⊥ ↔ LieSubmodule.lcs k N = ⊥
rw₂ rw₃ : LieSubmodule.lcs k N = ⊥ ↔ LieSubmodule.lcs k N = ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ LieSubmodule.lcs k N = ⊥

Tactic:
rw [N.lowerCentralSeries_eq_lcs_comap k, LieSubmodule.comap_incl_eq_bot,
    inf_eq_right.mpr (N.lcs_le_self k)]

Premises used: Iff.mpr, LieSubmodule.comap_incl_eq_bot, LieSubmodule.lowerCentralSeries_eq_lcs_comap, inf_eq_right, LieSubmodule.lcs_le_self