awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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₂)
⊢ Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M) ≤
    (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂)
have 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₂)
Tactic: rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', Submodule.map_span,
      Submodule.span_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
⊢ Membership.mem (α := M₂) (↑(↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) : Set M₂)
    ((g : (a : M) → M₂) m : M₂)
have 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₂)
Tactic: simp only [lowerCentralSeries_succ, SetLike.mem_coe, LieSubmodule.mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
have 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) sorry)) :
      M₂) :
    M₂)
  ((g : (a : M) → M₂) m : M₂)
Tactic: use f x, ⟨g m_n, ih (Submodule.mem_map_of_mem h₁)⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
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
⊢ 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₂)
have this : ∃ (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₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
⊢ 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₂)
have 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₂)
Tactic: obtain ⟨y, n, hn⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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 (α := 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₂)
have 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₂)
Tactic: rw [← hn]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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₂)
    (Bracket.bracket.{u_1, u_2} (L := LieIdeal R L₂) ⊤ (lowerCentralSeries R L₂ M₂ k)) (↑⁅y, n⁆ : M₂)
have succ : Membership.mem (γ := LieIdeal R L₂) ⊤ y
Tactic: apply LieSubmodule.lie_mem_lie
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
⊢ Membership.mem (γ := LieSubmodule R L₂ M₂)
    (Bracket.bracket.{u_1, u_2} (L := LieIdeal R L₂) ⊤ (lowerCentralSeries R L₂ M₂ k)) (↑⁅y, n⁆ : M₂)
have succ₁ : Membership.mem (γ := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) (↑n : M₂)
Tactic: apply LieSubmodule.lie_mem_lie
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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 : ℕ
⊢ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
have zero : Submodule.map g (↑(lowerCentralSeries R L M 0) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ 0) : 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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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₂)
⊢ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) ≤ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂)
have 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₂)
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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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₂
⊢ LieModule.IsNilpotent L M
have obtain : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) ⊥), LieModule.IsNilpotent L M
Tactic: obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L₂ M₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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) ⊥
⊢ LieModule.IsNilpotent L M
have rw : ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
Tactic: rw [isNilpotent_iff R]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
Tactic: use k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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) ⊥
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have 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)
Tactic: rw [← LieSubmodule.toSubmodule_inj] at hk ⊢
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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₂)
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)
have h : Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M) = Submodule.map g (↑⊥ : Submodule R M)
Tactic: apply Submodule.map_injective_of_injective hg_inj
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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₂)
have refine : (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
Tactic: refine le_antisymm (lieModule_lcs_map_le hfg k) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
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})
⊢ (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) ≤
    Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)
have 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})
Tactic: simp only [← LieSubmodule.mem_toSubmodule] at this
Cleared hypotheses: this