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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
l : ℕ
hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M) (le : m ≤ n)
  (hn : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) m) ⊥),
  Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) n) ⊥ :=
  ⋯
h₁ : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) (max k l)) ⊥
h₂ : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) (max k l)) ⊥
⊢ IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)
have refine : Eq.{w + 1} (α := LieSubmodule R L ↥(M₁ + M₂)) (lowerCentralSeries R L (↥(M₁ + M₂)) (max k l)) ⊥
Tactic: refine (isNilpotent_iff R L (M₁ + M₂)).mpr ⟨k ⊔ l, ?_⟩
-- 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
⊢ ∃ (k : ℕ),
    ∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0
have obtain : ∀ (k : ℕ) (hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥),
  ∃ (k : ℕ),
    ∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0
Tactic: obtain ⟨k, hM⟩ := 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
inst_7 : IsNilpotent L M
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ ∃ (k : ℕ),
    ∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0
have h : ∀ (x : L),
  HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
    0
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
inst_7 : IsNilpotent L M
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
x : L
⊢ HPow.hPow (α := Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
    0
have h : ∀ (m : M),
  Eq (α := M)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k :
          (a : M) → M)
        m :
      M)
    ((0 : (a : M) → M) m : M)
Tactic: ext 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
inst_7 : IsNilpotent L M
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
x : L
m : M
⊢ Eq (α := M)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k :
          (a : M) → M)
        m :
      M)
    ((0 : (a : M) → M) m : M)
have h : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k)
  ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
        (a : M) → M)^[k]
    m)
Tactic: rw [Module.End.pow_apply, LinearMap.zero_apply, ← @LieSubmodule.mem_bot R L M, ← hM]
-- 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
inst_7 : IsNilpotent L M
x : L
⊢ ∃ (k : ℕ),
    HPow.hPow (α := Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
      0
have this : ∃ (k : ℕ),
  ∀ (x : L),
    HPow.hPow (α := Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
      0
Tactic: have := exists_forall_pow_toEnd_eq_zero 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
inst_7 : IsNilpotent L M
x : L
this :
  ∃ (k : ℕ),
    ∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0
⊢ ∃ (k : ℕ),
    HPow.hPow (α := Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
      0
have tauto : ∀ (w : ℕ),
  (∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) w =
        0) →
    ∃ (k : ℕ),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0
Tactic: tauto
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
inst_7 : IsNilpotent L M
x y : L
⊢ _root_.IsNilpotent.{w} (R := M →ₗ[R] M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
      ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
have obtain : ∀ (k : ℕ) (hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥),
  _root_.IsNilpotent.{w} (R := M →ₗ[R] M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
      ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
Tactic: obtain ⟨k, hM⟩ := 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
inst_7 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
have rw : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) (lowerCentralSeries R L M k)
Tactic: rw [eq_bot_iff, ← hM]
-- 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
inst_7 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ _root_.IsNilpotent.{w} (R := M →ₗ[R] M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
      ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
have hM₁ : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
Tactic: replace hM : lowerCentralSeries R L M (2 * k) = ⊥ := by
    rw [eq_bot_iff, ← hM]; exact antitone_lowerCentralSeries R L M (by lia)
Cleared hypotheses: hM
-- 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
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
⊢ _root_.IsNilpotent.{w} (R := M →ₗ[R] M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
      ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
have h : HPow.hPow (α := M →ₗ[R] M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
      ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
    k =
  0
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
inst_7 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
⊢ HPow.hPow (α := M →ₗ[R] M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
        ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
      k =
    0
have h : ∀ (m : M),
  Eq (α := M)
    ((HPow.hPow (α := M →ₗ[R] M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
            k :
          (a : M) → M)
        m :
      M)
    ((0 : (a : M) → M) m : M)
Tactic: ext 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
inst_7 : IsNilpotent L M
x y : L
k : ℕ
hM : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k)) ⊥
m : M
⊢ Eq (α := M)
    ((HPow.hPow (α := M →ₗ[R] M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y)
            k :
          (a : M) → M)
        m :
      M)
    ((0 : (a : M) → M) m : M)
have h : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
  ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
            ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
        (a : M) → M)^[k]
    m)
Tactic: rw [Module.End.pow_apply, LinearMap.zero_apply, ← LieSubmodule.mem_bot (R := R) (L := L), ← hM]
-- 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
x : L
⊢ Eq.{w + 1} (α := Submodule R M)
    (Module.End.maxGenEigenspace (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x)
      0)
    ⊤
have h : ∀ (m : M),
  Membership.mem (γ := Submodule R M)
      (Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) 0)
      m ↔
    Membership.mem (γ := Submodule R M) ⊤ m
Tactic: ext 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
inst_7 : IsNilpotent L M
x : L
m : M
⊢ Membership.mem (γ := Submodule R M)
      (Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) 0)
      m ↔
    Membership.mem (γ := Submodule R M) ⊤ m
have h : ∃ (k : ℕ),
  Eq (α := M)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k :
          (a : M) → M)
        m :
      M)
    (0 : M)
Tactic: simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, Submodule.mem_top,
    iff_true]
-- 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
x : L
m : M
⊢ ∃ (k : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
              k :
            (a : M) → M)
          m :
        M)
      (0 : M)
have h : ∀ (k : ℕ)
  (hk :
    ∀ (x : L),
      HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k =
        0),
  ∃ (k : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
              k :
            (a : M) → M)
          m :
        M)
      (0 : M)
Tactic: obtain ⟨k, hk⟩ := exists_forall_pow_toEnd_eq_zero 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
h₂ : IsNilpotent.{v, w} L (M ⧸ N)
⊢ IsNilpotent L M
have rw : ∀ (h₂ : ∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥),
  ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
Tactic: rw [isNilpotent_iff R L] at h₂ ⊢
Cleared hypotheses: 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
h₂ : ∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have obtain : ∀ (k : ℕ) (hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥),
  ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
Tactic: obtain ⟨k, hk⟩ := h₂
Cleared hypotheses: 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) ⊥
Tactic: use k + 1
-- 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) ⊥
have h : Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
Tactic: simp only [lowerCentralSeries_succ]
-- 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
this : lowerCentralSeries R L M k ≤ N
⊢ Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
have this₁ : LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
  (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (maxTrivSubmodule R L M))
Tactic: replace this := LieSubmodule.mono_lie_right ⊤ (le_trans this h₁)
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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
this :
  LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (maxTrivSubmodule R L M))
⊢ Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
have rwa : ∀
  (this :
    LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥),
  Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
Tactic: rwa [ideal_oper_maxTrivSubmodule_eq_bot, le_bot_iff] at 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
this :
  LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (maxTrivSubmodule R L M))
rwa :
  ∀
    (this :
      LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥),
    Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
⊢ Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
have rwa₁ : ∀ (this : Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥),
  Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
Tactic: rwa [ideal_oper_maxTrivSubmodule_eq_bot, le_bot_iff] at 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
⊢ Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥
have h : lowerCentralSeries R L M k ≤ N
Tactic: suffices lowerCentralSeries R L M k ≤ N by
    replace this := LieSubmodule.mono_lie_right ⊤ (le_trans this h₁)
    rwa [ideal_oper_maxTrivSubmodule_eq_bot, le_bot_iff] at 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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
⊢ lowerCentralSeries R L M k ≤ N
have h : LE.le (α := LieSubmodule R L (M ⧸ N)) (LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k))
  (lowerCentralSeries R L (M ⧸ N) k)
Tactic: rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, ← le_bot_iff, ← 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
⊢ IsNilpotent.{v, w} L (M ⧸ N) ↔ ∃ (k : ℕ), lowerCentralSeries R L M k ≤ N
have rw : (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥) ↔
  ∃ (k : ℕ), lowerCentralSeries R L M k ≤ N
Tactic: rw [isNilpotent_iff R L]
-- 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
⊢ (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥) ↔
    ∃ (k : ℕ), lowerCentralSeries R L M k ≤ N
have refine : ∀ (k : ℕ),
  Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔ lowerCentralSeries R L M k ≤ N
Tactic: refine exists_congr fun 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
⊢ Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔ lowerCentralSeries R L M k ≤ N
have rw : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔
  Eq (α := LieSubmodule R L (M ⧸ N)) (LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k)) ⊥
Tactic: rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, map_lowerCentralSeries_eq k
    (LieSubmodule.Quotient.surjective_mk' N)]
-- 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
rw :
  Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔
    Eq (α := LieSubmodule R L (M ⧸ N)) (LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k)) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔ lowerCentralSeries R L M k ≤ N
have rw₁ : Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥ ↔
  Eq.{w + 1} (α := LieSubmodule R L (M ⧸ N)) (lowerCentralSeries R L (M ⧸ N) k) ⊥
Tactic: rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, map_lowerCentralSeries_eq k
    (LieSubmodule.Quotient.surjective_mk' N)]