-- Mathlib/Algebra/Lie/Weights/Basic.lean
@[simp] lemma posFittingCompOf_le_lowerCentralSeries (x : L) (k : ℕ) :
    posFittingCompOf R M x ≤ lowerCentralSeries R L M k

Proof state:
case zero
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
⊢ ((toEnd R L M) x ^ 0) m ∈ lowerCentralSeries R L M 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
⊢ posFittingCompOf R M x ≤ lowerCentralSeries R L M k

Tactic:
suffices ∀ m l, (toEnd R L M x ^ l) m ∈ lowerCentralSeries R L M l by
  intro m hm
  obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k
  exact this n k

Result:
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
⊢ ∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l

Proof state:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
this : ∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
n : M
hm : ((toEnd R L M) x ^ k) n ∈ posFittingCompOf R M x
⊢ ((toEnd R L M) x ^ k) n ∈ lowerCentralSeries R L M k

Tactic:
exact this n k

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
l : ℕ
⊢ ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l

Tactic:
induction l with
| zero => simp
| succ l ih =>
  simp only [lowerCentralSeries_succ, pow_succ', LinearMap.mul_apply]
  exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
⊢ ∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l

Tactic:
intro m l

Result:
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
l : ℕ
⊢ ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l

Proof state:
case succ
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
l : ℕ
ih : ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
⊢ ((toEnd R L M) x ^ (l + 1)) m ∈ lowerCentralSeries R L M (l + 1)

Tactic:
simp only [lowerCentralSeries_succ, pow_succ', LinearMap.mul_apply]

Result:
case succ
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
l : ℕ
ih : ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
⊢ ((toEnd R L M) x) (((toEnd R L M) x ^ l) m) ∈ ⁅⊤, lowerCentralSeries R L M l⁆

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
this : ∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
m : M
hm : m ∈ posFittingCompOf R M x
⊢ m ∈ lowerCentralSeries R L M k

Tactic:
obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k

Result:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
this : ∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
n : M
hm : ((toEnd R L M) x ^ k) n ∈ posFittingCompOf R M x
⊢ ((toEnd R L M) x ^ k) n ∈ lowerCentralSeries R L M k

Proof state:
case succ
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
l : ℕ
ih : ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
⊢ ((toEnd R L M) x) (((toEnd R L M) x ^ l) m) ∈ ⁅⊤, lowerCentralSeries R L M l⁆

Tactic:
exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
this : ∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
⊢ posFittingCompOf R M x ≤ lowerCentralSeries R L M k

Tactic:
intro m hm

Result:
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
this : ∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
m : M
hm : m ∈ posFittingCompOf R M x
⊢ m ∈ lowerCentralSeries R L M k