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₂)
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})
⊢ (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) ≤
    Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)
have 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}))
Tactic: simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span',
        Submodule.map_span, LieSubmodule.mem_top, true_and, ← 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₂)
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}))
have 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}
Tactic: refine Submodule.span_mono (Set.Subset.trans ?_ 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₂)
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
⊢ 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⁆
have 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₂)
Tactic: obtain ⟨n', hn', rfl⟩ := ih hn
Cleared hypotheses: n, 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₂)
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)
⊢ (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) ≤
    Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)
have succ : 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})
Tactic: suffices
      {m | ∃ (x : L₂) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, g n⁆ = m} ⊆
        g '' {m | ∃ (x : L) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} by
      simp only [← LieSubmodule.mem_toSubmodule] at this
      simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span',
        Submodule.map_span, LieSubmodule.mem_top, true_and, ← LieSubmodule.mem_toSubmodule]
      refine Submodule.span_mono (Set.Subset.trans ?_ this)
      rintro m₁ ⟨x, n, hn, rfl⟩
      obtain ⟨n', hn', rfl⟩ := ih hn
      exact ⟨x, n', hn', rfl⟩
-- 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 : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
x : L₂
n : M
hn : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n
⊢ Membership.mem.{u_2, u_2} (α := M₂) (γ := Set 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})
    (⁅x, (g : (a : M) → M₂) n⁆ : M₂)
have succ : ∀ (y : L),
  Membership.mem.{u_2, u_2} (α := M₂) (γ := Set 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})
    (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) y : L₂) ((g : (a : M) → M₂) n) : M₂)
Tactic: obtain ⟨y, rfl⟩ := hf_surj x
Cleared hypotheses: x
-- 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 : ℕ
⊢ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
have zero : (↑(lowerCentralSeries R L₂ M₂ 0) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M 0) : Submodule R M)
Tactic: induction k with
  | zero => simpa [LinearMap.range_eq_top]
  | succ k ih =>
    suffices
      {m | ∃ (x : L₂) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, g n⁆ = m} ⊆
        g '' {m | ∃ (x : L) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} by
      simp only [← LieSubmodule.mem_toSubmodule] at this
      simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span',
        Submodule.map_span, LieSubmodule.mem_top, true_and, ← LieSubmodule.mem_toSubmodule]
      refine Submodule.span_mono (Set.Subset.trans ?_ this)
      rintro m₁ ⟨x, n, hn, rfl⟩
      obtain ⟨n', hn', rfl⟩ := ih hn
      exact ⟨x, n', hn', rfl⟩
    rintro m₂ ⟨x, n, hn, rfl⟩
    obtain ⟨y, rfl⟩ := hf_surj x
    exact ⟨⁅y, n⁆, ⟨y, n, hn, rfl⟩, (hfg y n).symm⟩
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₂
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 : ℕ
zero :
  (↑(lowerCentralSeries R L₂ M₂ 0) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M 0) : Submodule R M)
⊢ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
have succ : ∀ (k : ℕ)
  (ih :
    (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤
      Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)),
  (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) ≤
    Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)
Tactic: induction k with
  | zero => simpa [LinearMap.range_eq_top]
  | succ k ih =>
    suffices
      {m | ∃ (x : L₂) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, g n⁆ = m} ⊆
        g '' {m | ∃ (x : L) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} by
      simp only [← LieSubmodule.mem_toSubmodule] at this
      simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span',
        Submodule.map_span, LieSubmodule.mem_top, true_and, ← LieSubmodule.mem_toSubmodule]
      refine Submodule.span_mono (Set.Subset.trans ?_ this)
      rintro m₁ ⟨x, n, hn, rfl⟩
      obtain ⟨n', hn', rfl⟩ := ih hn
      exact ⟨x, n', hn', rfl⟩
    rintro m₂ ⟨x, n, hn, rfl⟩
    obtain ⟨y, rfl⟩ := hf_surj x
    exact ⟨⁅y, n⁆, ⟨y, n, hn, rfl⟩, (hfg y n).symm⟩
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₂
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₂)
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₂
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₂)
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₂
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₂)
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₂
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₂)
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 (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
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst_7 : IsNilpotent.{v, w} L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
⊢ IsNilpotent.{v, w} L ↥M₁
have hfg : ∀ (x : L) (m : ↥M₁),
  Eq (α := ↥M₂) (Bracket.bracket (L := L) ((f : (a : L) → L) x : L) ((g : (a : ↥M₁) → ↥M₂) m) : ↥M₂)
    ((g : (a : ↥M₁) → ↥M₂) ⁅x, m⁆ : ↥M₂)
Tactic: have hfg : ∀ x m, ⁅f x, g m⁆ = g ⁅x, m⁆ := by aesop
-- 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
⊢ IsNilpotent.{v, w} L ↥(maxNilpotentSubmodule R L M)
have hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
Tactic: have hwf := CompleteLattice.WellFoundedGT.isSupClosedCompact (LieSubmodule R L M) inferInstance
-- 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
⊢ IsNilpotent.{v, w} L ↥(maxNilpotentSubmodule R L M)
have refine_1 : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} ⊥
Tactic: refine hwf { N : LieSubmodule R L M | IsNilpotent L N } ⟨⊥, ?_⟩ fun N₁ h₁ 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
refine_1 : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} ⊥
⊢ IsNilpotent.{v, w} L ↥(maxNilpotentSubmodule R L M)
have refine_2 : ∀ (N₁ : LieSubmodule R L M)
  (h₁ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₁)
  (N₂ : LieSubmodule R L M)
  (h₂ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₂),
  Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} (N₁ ⊔ N₂)
Tactic: refine hwf { N : LieSubmodule R L M | IsNilpotent L N } ⟨⊥, ?_⟩ fun N₁ h₁ N₂ 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
N₁ : LieSubmodule R L M
h₁ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₁
N₂ : LieSubmodule R L M
h₂ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₂
⊢ Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} (N₁ ⊔ N₂)
have h₃ : IsNilpotent.{v, w} L ↥N₁
Tactic: simp_all
Cleared hypotheses: h₁, 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
N₁ : LieSubmodule R L M
h₁ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₁
N₂ : LieSubmodule R L M
h₂ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₂
h₃ : IsNilpotent.{v, w} L ↥N₁
⊢ Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} (N₁ ⊔ N₂)
have h₄ : IsNilpotent.{v, w} L ↥N₂
Tactic: simp_all
Cleared hypotheses: h₁, 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
inst_7 : IsNilpotent L M
⊢ Eq (α := LieSubmodule R L M) (maxNilpotentSubmodule R L M) ⊤
have rw : LE.le (α := LieSubmodule R L M) ⊤ (maxNilpotentSubmodule R L M)
Tactic: rw [eq_top_iff]
-- 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
inst_7 : IsNilpotent L M
⊢ LE.le (α := LieSubmodule R L M) ⊤ (maxNilpotentSubmodule R L M)
have h : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} ⊤
Tactic: apply le_sSup