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 : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k₁) ⊥
⊢ k₂ ∈ s

Tactic:
exact eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries ℤ L M h₁₂)

Premises used: Iff.mpr, eq_bot_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 : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
⊢ ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s

Tactic:
have hs : ∀ k₁ k₂, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := by
    rintro k₁ k₂ h₁₂ (h₁ : lowerCentralSeries ℤ L M k₁ = ⊥)
    exact eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries ℤ L M 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
k : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
Nat.sInf_upward_closed_eq_succ_iff hs k

Premises used: Nat.sInf_upward_closed_eq_succ_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 : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
exact Nat.sInf_upward_closed_eq_succ_iff hs k

Premises used: Nat.sInf_upward_closed_eq_succ_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Nontrivial M
rw : IsTrivial L M ∧ Ne (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥ ↔ IsTrivial L M
⊢ nilpotencyLength L M = 1 ↔ IsTrivial L M

Tactic:
rw [nilpotencyLength_eq_succ_iff ℤ, ← trivial_iff_lower_central_eq_bot]

Premises used: LieModule.trivial_iff_lower_central_eq_bot, LieModule.nilpotencyLength_eq_succ_iff, Int
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Nontrivial M
⊢ IsTrivial L M ∧ Ne (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥ ↔ IsTrivial L M

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h : nilpotencyLength L M ≤ 1
⊢ Nontrivial M

Tactic:
nontriviality M
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h : nilpotencyLength L M ≤ 1
h_1 : Nontrivial M
inl : ∀ (h : nilpotencyLength L M = 0), IsTrivial L M
inr : ∀ (h : nilpotencyLength L M = 1), IsTrivial L M
⊢ IsTrivial L M

Tactic:
rcases Nat.le_one_iff_eq_zero_or_eq_one.mp h with h | h

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, Iff.mp
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h_1 : nilpotencyLength L M ≤ 1
h_2 : Nontrivial M
h : nilpotencyLength L M = 0
⊢ Subsingleton M

Tactic:
rw [nilpotencyLength_eq_zero_iff] at h

Premises used: LieModule.nilpotencyLength_eq_zero_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h_1 : nilpotencyLength L M ≤ 1
h_2 : Nontrivial M
h : Subsingleton M
⊢ IsTrivial L M

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h_1 : nilpotencyLength L M ≤ 1
h_2 : Nontrivial M
h : nilpotencyLength L M = 1
inr inr₁ inr₂ inr₃ : ∀ (h : IsTrivial L M), IsTrivial L M
⊢ IsTrivial L M

Tactic:
rwa [nilpotencyLength_eq_one_iff] at h

Premises used: LieModule.nilpotencyLength_eq_one_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
rw :
  LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (maxTrivSubmodule R L M)

Tactic:
rw [lowerCentralSeriesLast]

Premises used: LieModule.lowerCentralSeriesLast
-- 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
zero :
  ∀ (h : nilpotencyLength L M = 0),
    LE.le.{w} (α := LieSubmodule R L M)
      (match (motive := ℕ → LieSubmodule R L M) 0 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k :
        LieSubmodule R L M)
      (maxTrivSubmodule R L M : LieSubmodule R L M)
succ :
  ∀ (k : ℕ) (h : nilpotencyLength L M = k + 1),
    LE.le.{w} (α := LieSubmodule R L M)
      (match (motive := ℕ → LieSubmodule R L M) k + 1 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k :
        LieSubmodule R L M)
      (maxTrivSubmodule R L M : LieSubmodule R L M)
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)

Tactic:
rcases h : nilpotencyLength L M with - | k

Premises used: LieModule.nilpotencyLength
-- 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
h : nilpotencyLength L M = 0
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) 0 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)

Tactic:
bot_le

Premises used: Set.Mem, bot_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
h : nilpotencyLength L M = 0
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) 0 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)

Tactic:
exact bot_le

Premises used: bot_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
k : ℕ
h : nilpotencyLength L M = k + 1
succ :
  Eq.{w + 1} (α := LieSubmodule R L M)
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤
        (match (motive := ℕ → LieSubmodule R L M) k + 1 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k) :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)

Tactic:
rw [le_max_triv_iff_bracket_eq_bot]

Premises used: LieModule.le_max_triv_iff_bracket_eq_bot
-- 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 : ℕ
h : nilpotencyLength L M = k + 1
⊢ Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥ ∧
    Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
rw [nilpotencyLength_eq_succ_iff R, lowerCentralSeries_succ] at h

Premises used: LieModule.nilpotencyLength_eq_succ_iff, LieModule.lowerCentralSeries_succ
-- 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 : ℕ
h :
  Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥ ∧
    Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L M)
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤
        (match (motive := ℕ → LieSubmodule R L M) k + 1 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k) :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)

Tactic:
h.1

Premises used: Set.Mem, setOf, And.left
-- 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 : ℕ
h :
  Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥ ∧
    Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L M)
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤
        (match (motive := ℕ → LieSubmodule R L M) k + 1 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k) :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)

Tactic:
exact h.1

Premises used: And.left
-- 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
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
rw :
  Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
⊢ Nontrivial.{w} ↥(lowerCentralSeriesLast R L M)

Tactic:
rw [LieSubmodule.nontrivial_iff_ne_bot, lowerCentralSeriesLast]

Premises used: LieSubmodule.nontrivial_iff_ne_bot, LieModule.lowerCentralSeriesLast
-- 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
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
zero :
  ∀ (h : nilpotencyLength L M = 0),
    Ne.{w + 1} (α := LieSubmodule R L M)
      (match (motive := ℕ → LieSubmodule R L M) 0 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k :
        LieSubmodule R L M)
      (⊥ : LieSubmodule R L M)
succ :
  ∀ (n : ℕ) (h : nilpotencyLength L M = n + 1),
    Ne.{w + 1} (α := LieSubmodule R L M)
      (match (motive := ℕ → LieSubmodule R L M) n + 1 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k :
        LieSubmodule R L M)
      (⊥ : LieSubmodule R L M)
⊢ Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)

Tactic:
cases h : nilpotencyLength L M

Premises used: LieModule.nilpotencyLength
-- 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
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
h : nilpotencyLength L M = 0
⊢ ¬Nontrivial M

Tactic:
rw [nilpotencyLength_eq_zero_iff, ← not_nontrivial_iff_subsingleton] at h

Premises used: not_nontrivial_iff_subsingleton, LieModule.nilpotencyLength_eq_zero_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
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
h : ¬Nontrivial M
⊢ Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) 0 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)

Tactic:
contradiction
-- 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
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
n : ℕ
h : nilpotencyLength L M = n + 1
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (n + 1)) ⊥ ∧
    Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M n) ⊥

Tactic:
rw [nilpotencyLength_eq_succ_iff R] at h

Premises used: LieModule.nilpotencyLength_eq_succ_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
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
n : ℕ
h :
  Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (n + 1)) ⊥ ∧
    Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M n) ⊥
⊢ Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) n + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)

Tactic:
h.2

Premises used: And.right
-- 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
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
n : ℕ
h :
  Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (n + 1)) ⊥ ∧
    Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M n) ⊥
⊢ Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) n + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)

Tactic:
exact h.2

Premises used: And.right
-- 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 : IsNilpotent L M
h : ¬IsTrivial L M
rw :
  LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1)

Tactic:
rw [lowerCentralSeriesLast]

Premises used: LieModule.lowerCentralSeriesLast
-- 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 : IsNilpotent L M
h : ¬IsTrivial L M
by_contra : ∀ (contra : ¬1 < nilpotencyLength L M), False
⊢ 1 < nilpotencyLength L M

Tactic:
by_contra contra
-- 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 : IsNilpotent L M
h : ¬IsTrivial L M
contra : ¬1 < nilpotencyLength L M
⊢ IsTrivial L M

Tactic:
have := isTrivial_of_nilpotencyLength_le_one L M (not_lt.mp contra)
-- 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 : IsNilpotent L M
h : ¬IsTrivial L M
contra : ¬1 < nilpotencyLength L M
this : IsTrivial L M
⊢ False

Tactic:
contradiction
-- 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 : IsNilpotent L M
h : ¬IsTrivial L M
⊢ 1 < nilpotencyLength L M

Tactic:
replace h : 1 < nilpotencyLength L M := by
    by_contra contra
    have := isTrivial_of_nilpotencyLength_le_one L M (not_lt.mp contra)
    contradiction
-- 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 : IsNilpotent L M
h : 1 < nilpotencyLength L M
zero :
  ∀ (hk : nilpotencyLength L M = 0),
    LE.le.{w} (α := LieSubmodule R L M)
      (match (motive := ℕ → LieSubmodule R L M) 0 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k :
        LieSubmodule R L M)
      (lowerCentralSeries R L M 1 : LieSubmodule R L M)
succ :
  ∀ (k : ℕ) (hk : nilpotencyLength L M = k + 1),
    LE.le.{w} (α := LieSubmodule R L M)
      (match (motive := ℕ → LieSubmodule R L M) k + 1 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k :
        LieSubmodule R L M)
      (lowerCentralSeries R L M 1 : LieSubmodule R L M)
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)

Tactic:
rcases hk : nilpotencyLength L M with - | k

Premises used: LieModule.nilpotencyLength
-- 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 : IsNilpotent L M
h : 1 < nilpotencyLength L M
hk : nilpotencyLength L M = 0
⊢ LT.lt (α := ℕ) 1 0

Tactic:
rw [hk] at 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 : IsNilpotent L M
h : 1 < nilpotencyLength L M
hk : nilpotencyLength L M = 0
h₁ : LT.lt (α := ℕ) 1 0
⊢ nilpotencyLength L M = 0

Tactic:
rw [hk] at 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 : IsNilpotent L M
h : 1 < nilpotencyLength L M
k : ℕ
hk : nilpotencyLength L M = k + 1
⊢ 1 < k + 1

Tactic:
rw [hk] at 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 : IsNilpotent L M
h : 1 < nilpotencyLength L M
k : ℕ
hk : nilpotencyLength L M = k + 1
h₁ : 1 < k + 1
⊢ nilpotencyLength L M = k + 1

Tactic:
rw [hk] at 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 : IsNilpotent L M
h : LT.lt (α := ℕ) 1 0
hk : nilpotencyLength L M = 0
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) 0 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)

Tactic:
contradiction
-- 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 : IsNilpotent L M
k : ℕ
h : 1 < k + 1
hk : nilpotencyLength L M = k + 1
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)

Tactic:
antitone_lowerCentralSeries _ _ _ (Nat.le_of_lt_succ h)

Premises used: Set.Mem, LieModule.antitone_lowerCentralSeries, Nat.le_of_lt_succ
-- 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 : IsNilpotent L M
k : ℕ
h : 1 < k + 1
hk : nilpotencyLength L M = k + 1
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)

Tactic:
exact antitone_lowerCentralSeries _ _ _ (Nat.le_of_lt_succ h)

Premises used: LieModule.antitone_lowerCentralSeries, Nat.le_of_lt_succ
-- 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
inst_7 : IsNilpotent L M
h : IsTrivial L M
⊢ Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)

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
inst_7 : IsNilpotent L M
refine : ∀ (h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)), IsTrivial L M
⊢ Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M) ↔ IsTrivial L M

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by 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
inst_7 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
⊢ Nontrivial M

Tactic:
nontriviality M