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
k : ℕ
ih :
  (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
⊢ ∀ (x : M),
    x ∈ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) ↔
      x ∈ (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)

Tactic:
rw [Set.ext_iff] at ih

Premises used: Set.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 : ℕ
ih :
  ∀ (x : M),
    x ∈ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) ↔
      x ∈ (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
⊢ ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x

Tactic:
simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih

Premises used: LieSubmodule.mem_toSubmodule, SetLike.mem_coe
-- 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 : ℕ
ih :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
succ :
  (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) =
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
⊢ (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal R L) ⊤ x_1 ∧
                ∃ (n : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) =
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) ⊤ x_1 ∧
                ∃ (n : M), Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)

Tactic:
simp only [LieSubmodule.mem_top, ih, true_and]

Premises used: LieSubmodule.mem_top, true_and
-- 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 : ℕ
ih :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
succ :
  (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
succ₁ :
  (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
⊢ (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) =
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 : ℕ
ih :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
⊢ (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)

Tactic:
coe_lowerCentralSeries_eq_int_aux _ _ L M k

Premises used: _private.0.LieModule.coe_lowerCentralSeries_eq_int_aux
-- 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 : ℕ
ih :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
⊢ (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)

Tactic:
exact coe_lowerCentralSeries_eq_int_aux _ _ L M k

Premises used: _private.0.LieModule.coe_lowerCentralSeries_eq_int_aux
-- 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 : ℕ
ih :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
succ :
  (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
⊢ (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)

Tactic:
simp only [← ih]
-- 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 : ℕ
ih :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
⊢ (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)

Tactic:
coe_lowerCentralSeries_eq_int_aux _ _ L M k

Premises used: _private.0.LieModule.coe_lowerCentralSeries_eq_int_aux
-- 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 : ℕ
ih :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
⊢ (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)

Tactic:
exact coe_lowerCentralSeries_eq_int_aux _ _ L M k

Premises used: _private.0.LieModule.coe_lowerCentralSeries_eq_int_aux
-- 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 : ℕ
zero :
  (↑(↑(lowerCentralSeries R L M 0) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M 0) : Submodule ℤ M) : Set M)
succ :
  ∀ (k : ℕ)
    (ih :
      (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
        (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)),
    (↑(↑(lowerCentralSeries R L M (k + 1)) : Submodule R M) : Set M) =
      (↑(↑(lowerCentralSeries ℤ L M (k + 1)) : Submodule ℤ M) : Set M)
⊢ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)

Tactic:
induction k with
  | zero => rfl
  | succ k ih =>
    rw [lowerCentralSeries_succ, lowerCentralSeries_succ]
    rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
    rw [Set.ext_iff] at ih
    simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
    simp only [LieSubmodule.mem_top, ih, true_and]
    apply le_antisymm
    · exact coe_lowerCentralSeries_eq_int_aux _ _ L M k
    · simp only [← ih]
      exact coe_lowerCentralSeries_eq_int_aux _ _ L M k

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, LieModule.lowerCentralSeries_succ, le_antisymm, _private.0.LieModule.coe_lowerCentralSeries_eq_int_aux, SetLike.mem_coe, LieSubmodule.mem_top, Set.ext_iff, true_and
-- 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
⊢ lcs 0 N ≤ N

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_1 : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
succ : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N) ≤ N
⊢ lcs (k + 1) N ≤ N

Tactic:
simp only [lcs_succ]

Premises used: LieSubmodule.lcs_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
k_1 : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N) ≤ N

Tactic:
(LieSubmodule.mono_lie_right ⊤ ih).trans (N.lie_le_right ⊤)

Premises used: LieSubmodule.mono_lie_right, LieSubmodule.lie_le_right, LE.le.trans, 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 : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N) ≤ N

Tactic:
exact (LieSubmodule.mono_lie_right ⊤ ih).trans (N.lie_le_right ⊤)

Premises used: LieSubmodule.mono_lie_right, LieSubmodule.lie_le_right, LE.le.trans, 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 : ℕ
N : LieSubmodule R L M
zero : lcs 0 N ≤ N
succ : ∀ (k : ℕ) (ih : lcs k N ≤ N), lcs (k + 1) N ≤ N
⊢ lcs k N ≤ N

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    simp only [lcs_succ]
    exact (LieSubmodule.mono_lie_right ⊤ ih).trans (N.lie_le_right ⊤)

Premises used: LieSubmodule.lcs_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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
⊢ lowerCentralSeries R L (↥N) 0 = comap N.incl (lcs 0 N)

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_1 : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
succ :
  Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L (↥N) k) =
    comap N.incl (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N))
⊢ lowerCentralSeries R L (↥N) (k + 1) = comap N.incl (lcs (k + 1) N)

Tactic:
simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢

Premises used: LieModule.lowerCentralSeries_succ, LieSubmodule.lcs_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
k_1 : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
rw : lcs k N ≤ N
⊢ lcs k N ≤ N.incl.range

Tactic:
rw [N.range_incl]

Premises used: LieSubmodule.range_incl
-- 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
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ lcs k N ≤ N

Tactic:
apply lcs_le_self

Premises used: LieSubmodule.lcs_le_self
-- 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
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ lcs k N ≤ N.incl.range

Tactic:
have : N.lcs k ≤ N.incl.range := by
      rw [N.range_incl]
      apply lcs_le_self
-- 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
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
this : lcs k N ≤ N.incl.range
succ :
  Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (comap N.incl (lcs k N)) =
    comap N.incl (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N))
succ₁ succ₂ :
  Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (comap N.incl (lcs k N)) =
    Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (comap N.incl (lcs k N))
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L (↥N) k) =
    comap N.incl (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N))

Tactic:
rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl this]

Premises used: LieSubmodule.comap_bracket_eq, LieSubmodule.ker_incl, LieSubmodule.incl
-- 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
inst_6 : LieModule R L M
zero : lowerCentralSeries R L (↥N) 0 = comap N.incl (lcs 0 N)
succ :
  ∀ (k : ℕ) (ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)),
    lowerCentralSeries R L (↥N) (k + 1) = comap N.incl (lcs (k + 1) N)
⊢ lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢
    have : N.lcs k ≤ N.incl.range := by
      rw [N.range_incl]
      apply lcs_le_self
    rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl this]

Premises used: LieModule.lowerCentralSeries_succ, LieSubmodule.lcs_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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
rw : lcs k N ≤ N
⊢ map N.incl (lowerCentralSeries R L (↥N) k) = lcs k N

Tactic:
rw [lowerCentralSeries_eq_lcs_comap, LieSubmodule.map_comap_incl, inf_eq_right]

Premises used: LieSubmodule.lowerCentralSeries_eq_lcs_comap, inf_eq_right, LieSubmodule.map_comap_incl
-- 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
inst_6 : LieModule R L M
⊢ lcs k N ≤ N

Tactic:
apply lcs_le_self

Premises used: LieSubmodule.lcs_le_self
-- 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
inst_6 : LieModule R L M
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ lcs k N = ⊥

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.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 : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
refine_1 : ∀ (h : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥), lcs k N = ⊥
refine_2 : ∀ (h : lcs k N = ⊥), Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ lcs k N = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
h : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥
refine_1 : lowerCentralSeries R L (↥N) k ≤ N.incl.ker
⊢ lcs k N = ⊥

Tactic:
rw [← N.lowerCentralSeries_map_eq_lcs, ← LieModuleHom.le_ker_iff_map]

Premises used: LieSubmodule.lowerCentralSeries_map_eq_lcs, LieModuleHom.le_ker_iff_map
-- 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
inst_6 : LieModule R L M
h : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥
⊢ lowerCentralSeries R L (↥N) k ≤ N.incl.ker

Tactic:
simpa
-- 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
inst_6 : LieModule R L M
h : lcs k N = ⊥
refine_2 : N ⊓ lcs k N = ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥

Tactic:
rw [N.lowerCentralSeries_eq_lcs_comap, comap_incl_eq_bot]

Premises used: LieSubmodule.comap_incl_eq_bot, LieSubmodule.lowerCentralSeries_eq_lcs_comap
-- 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
inst_6 : LieModule R L M
h : lcs k N = ⊥
⊢ N ⊓ lcs k N = ⊥

Tactic:
simp [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
l : ℕ
⊢ l ≤ 0 → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M 0) (lowerCentralSeries R L M l)

Tactic:
fun h ↦ (Nat.le_zero.mp h).symm ▸ le_rfl

Premises used: le_rfl, Nat.le_zero, Eq.rec, Iff.mp, Eq.symm
-- 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
l : ℕ
⊢ l ≤ 0 → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M 0) (lowerCentralSeries R L M l)

Tactic:
exact fun h ↦ (Nat.le_zero.mp h).symm ▸ le_rfl
-- 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 : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
l : ℕ
h : l ≤ k + 1
succ : ∀ (hk : l ≤ k), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)
succ₁ :
  ∀ (hk : l = k.succ), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)

Tactic:
rcases Nat.of_le_succ h with (hk | hk)

Premises used: Nat.of_le_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
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
l : ℕ
h : l ≤ k + 1
hk : l ≤ k
succ :
  LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
    (lowerCentralSeries R L M l)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)

Tactic:
rw [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
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
l : ℕ
h : l ≤ k + 1
hk : l ≤ k
⊢ LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
    (lowerCentralSeries R L M l)

Tactic:
(LieSubmodule.mono_lie_right ⊤ (ih hk)).trans (LieSubmodule.lie_le_right _ _)

Premises used: LieSubmodule.mono_lie_right, LieSubmodule.lie_le_right, LE.le.trans, Top.top