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 : ℕ
⊢ GaloisConnection (fun (N : LieSubmodule R L M) ↦ lcs k N) fun (N : LieSubmodule R L M) ↦ ucs k N

Tactic:
fun _ _ => lcs_le_iff k

Premises used: Set.Mem, LieSubmodule.lcs_le_iff, GaloisConnection
-- 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 : lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M k ≤ N
⊢ ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N

Tactic:
rw [eq_top_iff, ← lcs_le_iff]

Premises used: eq_top_iff, LieSubmodule.lcs_le_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 : ℕ
⊢ lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M k ≤ N

Tactic:
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
rw :
  (∃ (k : ℕ), Eq (α := LieSubmodule R L M) (LieModule.lowerCentralSeries R L M k) ⊥) ↔
    ∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L M) (ucs k ⊥) ⊤
⊢ LieModule.IsNilpotent L M ↔ ∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L M) (ucs k ⊥) ⊤

Tactic:
rw [LieModule.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
k : ℕ
⊢ Eq (α := LieSubmodule R L M) (LieModule.lowerCentralSeries R L M k) ⊥ ↔
    Eq.{w + 1} (α := LieSubmodule R L M) (ucs k ⊥) ⊤

Tactic:
simp [ucs_eq_top_iff]

Premises used: LieSubmodule.ucs_eq_top_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 : ℕ), Eq (α := LieSubmodule R L M) (LieModule.lowerCentralSeries R L M k) ⊥) ↔
    ∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L M) (ucs k ⊥) ⊤

Tactic:
exact exists_congr fun k => by simp [ucs_eq_top_iff]

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
⊢ comap N.incl (ucs 0 ⊥) = ucs 0 ⊥

Tactic:
N.ker_incl

Premises used: LieSubmodule.ker_incl, Nat.iterate, LieModuleHom.ker, LieSubmodule.ucs
-- 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
⊢ comap N.incl (ucs 0 ⊥) = ucs 0 ⊥

Tactic:
exact N.ker_incl

Premises used: LieSubmodule.ker_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
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : comap N.incl (ucs k ⊥) = ucs k ⊥
⊢ comap N.incl (ucs (k + 1) ⊥) = ucs (k + 1) ⊥

Tactic:
simp [← 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
zero : comap N.incl (ucs 0 ⊥) = ucs 0 ⊥
succ : ∀ (k : ℕ) (ih : comap N.incl (ucs k ⊥) = ucs k ⊥), comap N.incl (ucs (k + 1) ⊥) = ucs (k + 1) ⊥
⊢ comap N.incl (ucs k ⊥) = ucs k ⊥

Tactic:
induction k with
  | zero => exact N.ker_incl
  | succ k ih => simp [← ih]

Premises used: LieSubmodule.ker_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
N : LieSubmodule R L M
inst_6 : LieModule R L M
simp_rw : (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (ucs k ⊥) ⊤) ↔ ∃ (k : ℕ), N ≤ ucs k ⊥
simp_rw₁ : (∃ (k : ℕ), comap N.incl (ucs k ⊥) = ⊤) ↔ ∃ (k : ℕ), N ≤ ucs k ⊥
⊢ LieModule.IsNilpotent.{v, w} L ↥N ↔ ∃ (k : ℕ), N ≤ ucs k ⊥

Tactic:
simp_rw [LieModule.isNilpotent_iff_exists_ucs_eq_top R, ← ucs_comap_incl, comap_incl_eq_top]

Premises used: LieSubmodule.comap_incl_eq_top, LieSubmodule.ucs_comap_incl, LieModule.isNilpotent_iff_exists_ucs_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
⊢ Eq (α := LieSubmodule R L M) (ucs 1 ⊥) (LieModule.maxTrivSubmodule R L M)

Tactic:
simp [LieSubmodule.normalizer_bot_eq_maxTrivSubmodule]

Premises used: LieSubmodule.normalizer_bot_eq_maxTrivSubmodule
-- 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₂)
⊢ Submodule.map g (↑(lowerCentralSeries R L M 0) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ 0) : Submodule R M₂)

Tactic:
simp [Submodule.map_top]

Premises used: Submodule.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
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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
succ :
  Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {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} ⊆
    (↑(↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) : Set M₂)
⊢ Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M) ≤
    (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂)

Tactic:
rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', Submodule.map_span,
      Submodule.span_le]

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieModule.lowerCentralSeries_succ, Submodule.map_span, Submodule.span_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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
succ :
  Membership.mem (α := M₂) (γ := LieSubmodule R L₂ M₂)
    (Bracket.bracket.{u_1, u_2} (L := LieIdeal R L₂) ⊤ (lowerCentralSeries R L₂ M₂ k)) ((g : (a : M) → M₂) m : M₂)
⊢ Membership.mem (α := M₂) (↑(↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) : Set M₂)
    ((g : (a : M) → M₂) m : M₂)

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

Premises used: LieSubmodule.mem_toSubmodule, LieModule.lowerCentralSeries_succ, 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
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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
h :
  Eq.{u_2 + 1} (α := M₂)
    ((↑(Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂)
            (Subtype.mk (p := fun (x : M₂) ↦
              Membership.mem (γ := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) x) ((g : (a : M) → M₂) m_n)
              ⋯)) :
        M₂) :
      M₂)
    ((g : (a : M) → M₂) m : M₂)
⊢ ∃ (y : L₂) (n : ↥(lowerCentralSeries R L₂ M₂ k)), (↑⁅y, n⁆ : M₂) = (g : (a : M) → M₂) m

Tactic:
use f x, ⟨g m_n, ih (Submodule.mem_map_of_mem h₁)⟩

Premises used: DFunLike.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
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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
⊢ Eq.{u_2 + 1} (α := M₂)
    ((↑(Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂)
            (Subtype.mk (p := fun (x : M₂) ↦
              Membership.mem (γ := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) x) ((g : (a : M) → M₂) m_n)
              ⋯)) :
        M₂) :
      M₂)
    ((g : (a : M) → M₂) m : M₂)

Tactic:
simp [hfg x m_n, 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
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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
⊢ ∃ (y : L₂) (n : ↥(lowerCentralSeries R L₂ M₂ k)), (↑⁅y, n⁆ : M₂) = (g : (a : M) → M₂) m

Tactic:
have : ∃ y : L₂, ∃ n : lowerCentralSeries R L₂ M₂ k, ⁅y, n⁆ = g m := by
      use f x, ⟨g m_n, ih (Submodule.mem_map_of_mem h₁)⟩
      simp [hfg x m_n, 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
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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
this : ∃ (y : L₂) (n : ↥(lowerCentralSeries R L₂ M₂ k)), (↑⁅y, n⁆ : M₂) = (g : (a : M) → M₂) m
succ :
  ∀ (y : L₂) (n : ↥(lowerCentralSeries R L₂ M₂ k)) (hn : (↑⁅y, n⁆ : M₂) = (g : (a : M) → M₂) m),
    Membership.mem (α := M₂) (γ := LieSubmodule R L₂ M₂)
      (Bracket.bracket.{u_1, u_2} (L := LieIdeal R L₂) ⊤ (lowerCentralSeries R L₂ M₂ k)) ((g : (a : M) → M₂) m : M₂)
⊢ Membership.mem (α := M₂) (γ := LieSubmodule R L₂ M₂)
    (Bracket.bracket.{u_1, u_2} (L := LieIdeal R L₂) ⊤ (lowerCentralSeries R L₂ M₂ k)) ((g : (a : M) → M₂) m : M₂)

Tactic:
obtain ⟨y, n, hn⟩ := 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
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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n_1 : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
y : L₂
n : ↥(lowerCentralSeries R L₂ M₂ k)
hn : (↑⁅y, n⁆ : M₂) = (g : (a : M) → M₂) m
succ :
  Membership.mem (γ := LieSubmodule R L₂ M₂)
    (Bracket.bracket.{u_1, u_2} (L := LieIdeal R L₂) ⊤ (lowerCentralSeries R L₂ M₂ k)) (↑⁅y, n⁆ : M₂)
⊢ Membership.mem (α := M₂) (γ := LieSubmodule R L₂ M₂)
    (Bracket.bracket.{u_1, u_2} (L := LieIdeal R L₂) ⊤ (lowerCentralSeries R L₂ M₂ k)) ((g : (a : M) → M₂) m : M₂)

Tactic:
rw [← hn]
-- 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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n_1 : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
y : L₂
n : ↥(lowerCentralSeries R L₂ M₂ k)
hn : (↑⁅y, n⁆ : M₂) = (g : (a : M) → M₂) m
succ : Membership.mem (γ := LieIdeal R L₂) ⊤ y
succ₁ : Membership.mem (γ := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) (↑n : M₂)
⊢ Membership.mem (γ := LieSubmodule R L₂ M₂)
    (Bracket.bracket.{u_1, u_2} (L := LieIdeal R L₂) ⊤ (lowerCentralSeries R L₂ M₂ k)) (↑⁅y, n⁆ : M₂)

Tactic:
apply LieSubmodule.lie_mem_lie

Premises used: LieSubmodule.lie_mem_lie
-- 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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n_1 : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
y : L₂
n : ↥(lowerCentralSeries R L₂ M₂ k)
hn : (↑⁅y, n⁆ : M₂) = (g : (a : M) → M₂) m
⊢ Membership.mem (γ := LieIdeal R L₂) ⊤ y

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
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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n_1 : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
y : L₂
n : ↥(lowerCentralSeries R L₂ M₂ k)
hn : (↑⁅y, n⁆ : M₂) = (g : (a : M) → M₂) m
⊢ Membership.mem (γ := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) (↑n : M₂)

Tactic:
SetLike.coe_mem n

Premises used: SetLike.coe_mem
-- 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₂)
k : ℕ
ih :
  Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
m : M
x : L
n_1 : Membership.mem (γ := LieIdeal R L) ⊤ x
m_n : M
h₁ : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m_n
h₂ : ⁅x, m_n⁆ = m
y : L₂
n : ↥(lowerCentralSeries R L₂ M₂ k)
hn : (↑⁅y, n⁆ : M₂) = (g : (a : M) → M₂) m
⊢ Membership.mem (γ := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) (↑n : M₂)

Tactic:
exact SetLike.coe_mem n

Premises used: SetLike.coe_mem
-- 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₂)
k : ℕ
zero :
  Submodule.map g (↑(lowerCentralSeries R L M 0) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ 0) : Submodule R M₂)
succ :
  ∀ (k : ℕ)
    (ih :
      Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤
        (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)),
    Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M) ≤
      (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂)
⊢ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)

Tactic:
induction k with
  | zero =>
    simp [Submodule.map_top]
  | succ k ih =>
    rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', Submodule.map_span,
      Submodule.span_le]
    rintro m₂ ⟨m, ⟨x, n, m_n, ⟨h₁, h₂⟩⟩, rfl⟩
    simp only [lowerCentralSeries_succ, SetLike.mem_coe, LieSubmodule.mem_toSubmodule]
    have : ∃ y : L₂, ∃ n : lowerCentralSeries R L₂ M₂ k, ⁅y, n⁆ = g m := by
      use f x, ⟨g m_n, ih (Submodule.mem_map_of_mem h₁)⟩
      simp [hfg x m_n, h₂]
    obtain ⟨y, n, hn⟩ := this
    rw [← hn]
    apply LieSubmodule.lie_mem_lie
    · simp
    · exact SetLike.coe_mem n

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, Submodule.map_top, LieModule.lowerCentralSeries_succ, LieSubmodule.lie_mem_lie, SetLike.mem_coe, Submodule.map_span, Submodule.span_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
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₂
obtain : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) ⊥), LieModule.IsNilpotent L M
⊢ LieModule.IsNilpotent L M

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

Premises used: LieModule.IsNilpotent.nilpotent