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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hg_inj : Injective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : Eq (α := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) ⊥
rw : ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ LieModule.IsNilpotent L M

Tactic:
rw [isNilpotent_iff R]

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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hg_inj : Injective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : Eq (α := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) ⊥
h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hg_inj : Injective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : Eq (α := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) ⊥
h :
  ∀ (hk : Eq (α := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) (↑⊥ : Submodule R M₂)),
    Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
rw [← LieSubmodule.toSubmodule_inj] at hk ⊢

Premises used: LieSubmodule.toSubmodule_inj
-- 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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hg_inj : Injective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : Eq (α := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) (↑⊥ : Submodule R M₂)
h : Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) = Submodule.map g (↑⊥ : Submodule R M)
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)

Tactic:
apply Submodule.map_injective_of_injective hg_inj

Premises used: Submodule.map_injective_of_injective
-- 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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hg_inj : Injective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : Eq (α := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) (↑⊥ : Submodule R M₂)
⊢ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) = Submodule.map g (↑⊥ : Submodule R M)

Tactic:
simpa [hk] using lieModule_lcs_map_le hfg k

Premises used: lieModule_lcs_map_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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
⊢ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) = (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)

Tactic:
le_antisymm (lieModule_lcs_map_le hfg k) ?_

Premises used: le_antisymm, lieModule_lcs_map_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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
refine :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
⊢ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) = (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)

Tactic:
refine le_antisymm (lieModule_lcs_map_le hfg k) ?_

Premises used: le_antisymm, lieModule_lcs_map_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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
⊢ (↑(lowerCentralSeries R L₂ M₂ 0) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M 0) : Submodule R M)

Tactic:
simpa [LinearMap.range_eq_top]

Premises used: LinearMap.range_eq_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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
this :
  Subset.{u_2} (α := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M | ∃ (x : L) (n : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x, n⁆ = m})
⊢ Subset.{u_2} (α := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M |
        ∃ (x : L) (n : M),
          Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x, n⁆ = m})

Tactic:
simp only [← LieSubmodule.mem_toSubmodule] at this

Premises used: LieSubmodule.mem_toSubmodule
-- 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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
this :
  Subset.{u_2} (α := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M |
        ∃ (x : L) (n : M),
          Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x, n⁆ = m})
simp_rw :
  LE.le.{u_2} (α := Submodule R M₂)
    (Submodule.span R
      {x : M₂ |
        ∃ (x_1 : L₂) (n : M₂),
          Membership.mem (γ := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) n ∧ ⁅x_1, n⁆ = x})
    (Submodule.span R
      (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x_1, n⁆ = x}))
⊢ (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) ≤
    Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)

Tactic:
simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span',
        Submodule.map_span, LieSubmodule.mem_top, true_and, ← LieSubmodule.mem_toSubmodule]

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, LieModule.lowerCentralSeries_succ, LieSubmodule.mem_top, Submodule.map_span, 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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
this :
  Subset.{u_2} (α := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M |
        ∃ (x : L) (n : M),
          Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x, n⁆ = m})
⊢ LE.le.{u_2} (α := Submodule R M₂)
    (Submodule.span R
      {x : M₂ |
        ∃ (x_1 : L₂) (n : M₂),
          Membership.mem (γ := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) n ∧ ⁅x_1, n⁆ = x})
    (Submodule.span R
      (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x_1, n⁆ = x}))

Tactic:
Submodule.span_mono (Set.Subset.trans ?_ this)

Premises used: Set.Subset.trans, Submodule.span_mono
-- 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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
this :
  Subset.{u_2} (α := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M |
        ∃ (x : L) (n : M),
          Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x, n⁆ = m})
refine :
  Subset.{u_2} (α := Set M₂)
    {x : M₂ |
      ∃ (x_1 : L₂) (n : M₂),
        Membership.mem (γ := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) n ∧ ⁅x_1, n⁆ = x}
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
⊢ LE.le.{u_2} (α := Submodule R M₂)
    (Submodule.span R
      {x : M₂ |
        ∃ (x_1 : L₂) (n : M₂),
          Membership.mem (γ := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) n ∧ ⁅x_1, n⁆ = x})
    (Submodule.span R
      (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x_1, n⁆ = x}))

Tactic:
refine Submodule.span_mono (Set.Subset.trans ?_ this)

Premises used: Set.Subset.trans, Submodule.span_mono
-- 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
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
this :
  Subset.{u_2} (α := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M |
        ∃ (x : L) (n : M),
          Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x, n⁆ = m})
x : L₂
n : M₂
hn : Membership.mem (γ := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) n
obtain :
  ∀ (n' : M) (hn' : n' ∈ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M))
    (hn :
      Membership.mem (α := M₂) (γ := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
        ((g : (a : M) → M₂) n' : M₂)),
    Membership.mem.{u_2, u_2} (α := M₂) (γ := Set M₂)
      {m : M₂ |
        ∃ (x : L₂) (n : M),
          Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
            ⁅x, (g : (a : M) → M₂) n⁆ = m}
      (⁅x, (g : (a : M) → M₂) n'⁆ : M₂)
⊢ Membership.mem (γ := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    ⁅x, n⁆

Tactic:
obtain ⟨n', hn', rfl⟩ := ih hn

Premises used: 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
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
this :
  Subset.{u_2} (α := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M |
        ∃ (x : L) (n : M),
          Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x, n⁆ = m})
x : L₂
n' : M
hn' : n' ∈ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M)
hn :
  Membership.mem (α := M₂) (γ := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
    ((g : (a : M) → M₂) n' : M₂)
⊢ Membership.mem.{u_2, u_2} (α := M₂) (γ := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (⁅x, (g : (a : M) → M₂) n'⁆ : M₂)

Tactic:
⟨x, n', hn', rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, 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
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
this :
  Subset.{u_2} (α := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M |
        ∃ (x : L) (n : M),
          Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x, n⁆ = m})
x : L₂
n' : M
hn' : n' ∈ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M)
hn :
  Membership.mem (α := M₂) (γ := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
    ((g : (a : M) → M₂) n' : M₂)
⊢ Membership.mem.{u_2, u_2} (α := M₂) (γ := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧
          ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (⁅x, (g : (a : M) → M₂) n'⁆ : M₂)

Tactic:
exact ⟨x, n', hn', rfl⟩