mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f✝ : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
⊢ m • eval x f + m • eval x g = m • eval x f + m • eval x g

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ m • r * (m • x) ^ (n + 1) = m • r * (m • x) ^ (n + 1)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R L M (2 * k) ≤ lowerCentralSeries R L M k

Tactic:
]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R L M (2 * k) ≤ lowerCentralSeries R L M k
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: S : Type u_3
inst✝² : CommSemiring S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval (g • x) f = eval (g • x) f

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: S : Type u_3
inst✝² : CommSemiring S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval x (g • f) = eval x (g • f)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M (2 * k) = ⊥
m : M
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M (2 * k) = ⊥
m : M
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : G ⧸ stabilizer G x
⊢ X - C (g • ofQuotientStabilizer G x g') = X - C (g • ofQuotientStabilizer G x g')

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
n : ℕ
⊢ (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
h₂ : ∃ k, lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
h₂ : ∃ k, lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ ∃ k, lowerCentralSeries R L M k = ⊥
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
⊢ C (m • g b) = C (m • g b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
this : ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥

Tactic:
]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
this : ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
⊢ K'.toSubmodule ≤ K.normalizer.toSubmodule

Tactic:
]

Goal state after:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
⊢ K'.toSubmodule ≤ K.normalizer.toSubmodule
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L (M ⧸ N) k

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L (M ⧸ N) k
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ (∃ k, lowerCentralSeries R L (M ⧸ N) k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k ≤ N

Tactic:
]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ (∃ k, lowerCentralSeries R L (M ⧸ N) k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k ≤ N
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lowerCentralSeries R L (M ⧸ N) k = ⊥ ↔ lowerCentralSeries R L (M ⧸ N) k = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p✝ p q : P[X]
ihp : map (↑g) (m • p) = (MonoidHom.id M) m • map (↑g) p
ihq : map (↑g) (m • q) = (MonoidHom.id M) m • map (↑g) q
⊢ (MonoidHom.id M) m • map (↑g) p + (MonoidHom.id M) m • map (↑g) q =
    (MonoidHom.id M) m • map (↑g) p + (MonoidHom.id M) m • map (↑g) q

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ lowerCentralSeries ℤ L M 0 = ⊥

Tactic:
]

Goal state after:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ lowerCentralSeries ℤ L M 0 = ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
h : lowerCentralSeries ℤ L M 0 = ⊥
⊢ 0 ∈ s ∨ s = ∅

Tactic:
]

Goal state after:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
h : lowerCentralSeries ℤ L M 0 = ⊥
⊢ 0 ∈ s ∨ s = ∅
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries ℤ L M (k + 1) = ⊥ ∧ ¬lowerCentralSeries ℤ L M k = ⊥

Tactic:
]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries ℤ L M (k + 1) = ⊥ ∧ ¬lowerCentralSeries ℤ L M k = ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : Nontrivial M
⊢ IsTrivial L M ∧ lowerCentralSeries ℤ L M 0 ≠ ⊥ ↔ IsTrivial L M

Tactic:
]

Goal state after:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : Nontrivial M
⊢ IsTrivial L M ∧ lowerCentralSeries ℤ L M 0 ≠ ⊥ ↔ IsTrivial L M
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
⊢ IsTrivial L M

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

Goal state after:
case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 0
⊢ IsTrivial L M

case inr
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 1
⊢ IsTrivial L M
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : Subsingleton M
⊢ IsTrivial L M

Tactic:
]

Goal state after:
case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : Subsingleton M
⊢ IsTrivial L M
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case inr
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : IsTrivial L M
⊢ IsTrivial L M

Tactic:
]

Goal state after:
case inr
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : IsTrivial L M
⊢ IsTrivial L M
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ C (m • g b) * X ^ (n + 1) = C (m • g b) * X ^ (n + 1)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ (match nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    maxTrivSubmodule R L M

Tactic:
]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ (match nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    maxTrivSubmodule R L M
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
h : nilpotencyLength L M = k + 1
⊢ ⁅⊤,
      match k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k⁆ =
    ⊥

Tactic:
]

Goal state after:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
h : nilpotencyLength L M = k + 1
⊢ ⁅⊤,
      match k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k⁆ =
    ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
h : ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥
⊢ ⁅⊤,
      match k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k⁆ =
    ⊥

Tactic:
]

Goal state after:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
h : ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥
⊢ ⁅⊤,
      match k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k⁆ =
    ⊥
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule (↥K') M
_i4 : LieModule R (↥K') M
h : ∀ (x : ↥K'), IsNilpotent ((toEnd R (↥K') M) x)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ R ∙ ⟨x, hxK'⟩ ⊔ (LieSubalgebra.ofLe hKK').toSubmodule = ⊤

Tactic:
]

Goal state after:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule (↥K') M
_i4 : LieModule R (↥K') M
h : ∀ (x : ↥K'), IsNilpotent ((toEnd R (↥K') M) x)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ R ∙ ⟨x, hxK'⟩ ⊔ (LieSubalgebra.ofLe hKK').toSubmodule = ⊤
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
⊢ (match nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥

Tactic:
]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
⊢ (match nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
h : ¬Nontrivial M
⊢ (match 0 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥

Tactic:
]

Goal state after:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
h : ¬Nontrivial M
⊢ (match 0 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
n✝ : ℕ
h : lowerCentralSeries R L M (n✝ + 1) = ⊥ ∧ lowerCentralSeries R L M n✝ ≠ ⊥
⊢ (match n✝ + 1 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥

Tactic:
]

Goal state after:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
n✝ : ℕ
h : lowerCentralSeries R L M (n✝ + 1) = ⊥ ∧ lowerCentralSeries R L M n✝ ≠ ⊥
⊢ (match n✝ + 1 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
n✝ : ℕ
h : nilpotencyLength L M = n✝ + 1
⊢ (match n✝ + 1 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥

Tactic:
rw [nilpotencyLength_eq_succ_iff R] at h
    exact h.2

Goal state after:
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule (↥K') M
_i4 : LieModule R (↥K') M
h : ∀ (x : ↥K'), IsNilpotent ((toEnd R (↥K') M) x)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ R ∙ ↑⟨x, hxK'⟩ ⊔ K.toSubmodule = K'.toSubmodule

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h : ¬IsTrivial L M
⊢ (match nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1

Tactic:
]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h : ¬IsTrivial L M
⊢ (match nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h : 1 < 0
hk : nilpotencyLength L M = 0
⊢ (match 0 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1

Tactic:
]

Goal state after:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h : 1 < 0
hk : nilpotencyLength L M = 0
⊢ (match 0 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
k : ℕ
h : 1 < k + 1
hk : nilpotencyLength L M = k + 1
⊢ (match k + 1 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1

Tactic:
]

Goal state after:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
k : ℕ
h : 1 < k + 1
hk : nilpotencyLength L M = k + 1
⊢ (match k + 1 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1