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
inst_7 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
h_1 : Nontrivial M
by_contra : ∀ (contra : ¬IsTrivial L M), False
⊢ IsTrivial 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 : LieModule R L M
inst_7 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M)

Tactic:
have : lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M :=
    le_inf_iff.mpr ⟨lowerCentralSeriesLast_le_of_not_isTrivial R L M contra,
      lowerCentralSeriesLast_le_max_triv R L M⟩
-- 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)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
this_1 :
  LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M)
this : ¬Nontrivial.{w} ↥(lowerCentralSeriesLast R L M)
⊢ False

Tactic:
this (nontrivial_lowerCentralSeriesLast R L M)

Premises used: LieModule.nontrivial_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 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
this_1 :
  LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M)
this : ¬Nontrivial.{w} ↥(lowerCentralSeriesLast R L M)
⊢ False

Tactic:
exact this (nontrivial_lowerCentralSeriesLast R L M)

Premises used: LieModule.nontrivial_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 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
this :
  LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M)
suffices : ¬Nontrivial.{w} ↥(lowerCentralSeriesLast R L M)
⊢ False

Tactic:
suffices ¬ Nontrivial (lowerCentralSeriesLast R L M) by
    exact this (nontrivial_lowerCentralSeriesLast R L M)
-- 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)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
this :
  LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M)
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) ⊥

Tactic:
rw [h.eq_bot, le_bot_iff] at this

Premises used: le_bot_iff, Disjoint.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
inst_7 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
this : Eq (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) ⊥
⊢ ¬Nontrivial.{w} ↥(lowerCentralSeriesLast R L M)

Tactic:
this ▸ not_nontrivial _

Premises used: Eq.rec, not_nontrivial, Eq.symm
-- 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)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
this : Eq (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) ⊥
⊢ ¬Nontrivial.{w} ↥(lowerCentralSeriesLast R L M)

Tactic:
exact this ▸ not_nontrivial _
-- 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
⊢ Nontrivial.{w} ↥(maxTrivSubmodule R L M)

Tactic:
Set.nontrivial_mono (lowerCentralSeriesLast_le_max_triv R L M)
    (nontrivial_lowerCentralSeriesLast R L M)

Premises used: LieModule.lowerCentralSeriesLast_le_max_triv, LieModule.nontrivial_lowerCentralSeriesLast, Set.nontrivial_mono
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M 0) : Submodule R M)
    (↑(lowerCentralSeries R L M 0) : Submodule R 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
k : ℕ
ih :
  Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
    (↑(lowerCentralSeries R L M k) : Submodule R M)
succ :
  Eq.{w + 1} (α := Submodule R M)
    (Submodule.span R
      {x : M |
        ∃ (x_1 : ↥(LieHom.range (toEnd R L M))),
          Membership.mem (γ := LieIdeal R ↥(LieHom.range (toEnd R L M))) ⊤ x_1 ∧
            ∃ (n : M),
              Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x_1, n⁆ = x})
    (Submodule.span R
      {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})
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M (k + 1)) : Submodule R M)
    (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)

Tactic:
simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (lowerCentralSeries R (toEnd R L M).range M k).mem_toSubmodule, ih]

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, Membership.mem, LieModule.lowerCentralSeries_succ, LieHom.range, Subtype, LieModule.lowerCentralSeries, LieModule.toEnd
-- 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 : ℕ
ih :
  Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
    (↑(lowerCentralSeries R L M k) : Submodule R M)
⊢ Eq.{w + 1} (α := Submodule R M)
    (Submodule.span R
      {x : M |
        ∃ (x_1 : ↥(LieHom.range (toEnd R L M))),
          Membership.mem (γ := LieIdeal R ↥(LieHom.range (toEnd R L M))) ⊤ x_1 ∧
            ∃ (n : M),
              Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x_1, n⁆ = x})
    (Submodule.span R
      {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})

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
k : ℕ
zero :
  Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M 0) : Submodule R M)
    (↑(lowerCentralSeries R L M 0) : Submodule R M)
succ :
  ∀ (k : ℕ)
    (ih :
      Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
        (↑(lowerCentralSeries R L M k) : Submodule R M)),
    Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M (k + 1)) : Submodule R M)
      (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
    (↑(lowerCentralSeries R L M k) : Submodule R M)

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (lowerCentralSeries R (toEnd R L M).range M k).mem_toSubmodule, ih]
    simp

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, Membership.mem, LieModule.lowerCentralSeries_succ, LieHom.range, Subtype, LieModule.lowerCentralSeries, LieModule.toEnd
-- 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
simp :
  (∃ (k : ℕ),
      Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
        (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥) ↔
    ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ IsNilpotent (↥(LieHom.range (toEnd R L M))) M ↔ IsNilpotent L M

Tactic:
simp only [isNilpotent_iff R _ M]

Premises used: LieModule.isNilpotent_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
mp :
  (∃ (k : ℕ),
      Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
        (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥) →
    ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
mpr :
  (∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥) →
    ∃ (k : ℕ),
      Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
        (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥
⊢ (∃ (k : ℕ),
      Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
        (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥) ↔
    ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
constructor
-- 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 : ℕ
hk :
  Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M) (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k)
    ⊥
h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
use k
-- 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 : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
h :
  Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M) (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k)
    ⊥
⊢ ∃ (k : ℕ),
    Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
      (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥

Tactic:
use k
-- 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 : ℕ
hk :
  Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M) (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k)
    ⊥
h :
  ∀
    (hk :
      Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
        (↑⊥ : Submodule R M)),
    Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥

Tactic:
rw [← LieSubmodule.toSubmodule_inj] at hk ⊢

Premises used: LieSubmodule.toSubmodule_inj
-- 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 : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
h :
  ∀ (hk : Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)),
    Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
      (↑⊥ : Submodule R M)
⊢ Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M) (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k)
    ⊥

Tactic:
rw [← LieSubmodule.toSubmodule_inj] at hk ⊢

Premises used: LieSubmodule.toSubmodule_inj
-- 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 : ℕ
hk :
  Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
    (↑⊥ : Submodule R M)
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)

Tactic:
simpa using hk
-- 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 : ℕ
hk : Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
    (↑⊥ : Submodule R M)

Tactic:
simpa using hk
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
inst_6 : LieModule R L M
⊢ ucs 0 N = N

Tactic:
rfl

Premises used: Nat.iterate, rfl, LieSubmodule.ucs
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
⊢ ucs (k + 1) N = (ucs k N).normalizer

Tactic:
Function.iterate_succ_apply' normalizer k N

Premises used: Function.iterate_succ_apply', LieSubmodule.normalizer, LieSubmodule.ucs
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
inst_6 : LieModule R L M
k l : ℕ
⊢ ucs (k + l) N = ucs k (ucs l N)

Tactic:
Function.iterate_add_apply normalizer k l N

Premises used: Function.iterate_add_apply, LieSubmodule.normalizer, LieSubmodule.ucs
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁ ≤ N₂
⊢ ucs 0 N₁ ≤ ucs 0 N₂

Tactic:
simpa
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
succ : (ucs k N₁).normalizer ≤ (ucs k N₂).normalizer
⊢ ucs (k + 1) N₁ ≤ ucs (k + 1) N₂

Tactic:
simp only [ucs_succ]

Premises used: LieSubmodule.ucs_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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ (ucs k N₁).normalizer ≤ (ucs k N₂).normalizer

Tactic:
gcongr
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
h : N₁ ≤ N₂
zero : ucs 0 N₁ ≤ ucs 0 N₂
succ : ∀ (k : ℕ) (ih : ucs k N₁ ≤ ucs k N₂), ucs (k + 1) N₁ ≤ ucs (k + 1) N₂
⊢ ucs k N₁ ≤ ucs k N₂

Tactic:
induction k with
  | zero => simpa
  | succ k ih =>
    simp only [ucs_succ]
    gcongr

Premises used: LieSubmodule.ucs_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
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
⊢ ucs 0 N₁ = N₁

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
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
ih : ucs k N₁ = N₁
succ : (ucs k N₁).normalizer = N₁
succ₁ succ₂ succ₃ succ₄ : N₁.normalizer = N₁
⊢ ucs (k + 1) N₁ = N₁

Tactic:
rwa [ucs_succ, ih]

Premises used: LieSubmodule.ucs_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
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
zero : ucs 0 N₁ = N₁
succ : ∀ (k : ℕ) (ih : ucs k N₁ = N₁), ucs (k + 1) N₁ = N₁
⊢ ucs k N₁ = N₁

Tactic:
induction k with
  | zero => simp
  | succ k ih => rwa [ucs_succ, ih]

Premises used: LieSubmodule.ucs_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
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
rw : ucs k ⊥ ≤ ucs k N₁
⊢ ucs k ⊥ ≤ N₁

Tactic:
rw [← ucs_eq_self_of_normalizer_eq_self h k]

Premises used: LieSubmodule.ucs_eq_self_of_normalizer_eq_self
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
h₁ : ⊥ ≤ N₁
⊢ ucs k ⊥ ≤ ucs k N₁

Tactic:
gcongr
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ⊥ ≤ N₁

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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
l : ℕ
⊢ lcs (l + 0) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs 0 N₂

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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ l + (k + 1) = l + 1 + k

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
rw : l + (k + 1) = l + 1 + k
succ : lcs (l + 1 + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
succ₁ : lcs (l + 1) N₁ ≤ ucs k N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
succ₂ : lcs (l + 1) N₁ ≤ ucs k N₂ ↔ lcs l N₁ ≤ (ucs k N₂).normalizer
succ₃ : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs l N₁) ≤ ucs k N₂ ↔ lcs l N₁ ≤ (ucs k N₂).normalizer
succ₄ succ₅ : lcs l N₁ ≤ (ucs k N₂).normalizer ↔ lcs l N₁ ≤ (ucs k N₂).normalizer
⊢ lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂

Tactic:
rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]

Premises used: LieSubmodule.ucs_succ, LieSubmodule.top_lie_le_iff_le_normalizer, LieSubmodule.lcs_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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
l k : ℕ
zero : ∀ (l : ℕ), lcs (l + 0) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs 0 N₂
succ :
  ∀ (k : ℕ) (ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂) (l : ℕ),
    lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
⊢ lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂

Tactic:
induction k generalizing l with
  | zero => simp
  | succ k ih =>
    rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]

Premises used: LieSubmodule.ucs_succ, LieSubmodule.top_lie_le_iff_le_normalizer, LieSubmodule.lcs_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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
⊢ lcs (0 + k) N₁ ≤ N₂ ↔ lcs 0 N₁ ≤ ucs k N₂

Tactic:
lcs_add_le_iff (R := R) (L := L) (M := M) 0 k

Premises used: LieSubmodule.lcs_add_le_iff, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
h : k = 0 + k
⊢ lcs k N₁ ≤ N₂ ↔ N₁ ≤ ucs k N₂

Tactic:
convert! lcs_add_le_iff (R := R) (L := L) (M := M) 0 k

Premises used: LieSubmodule.lcs_add_le_iff, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
h h₁ : k = k
⊢ k = 0 + k

Tactic:
rw [zero_add]

Premises used: zero_add