-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem iterate_toEnd_mem_lowerCentralSeries₂ (x y : L) (m : M) (k : ℕ) :
    (toEnd R L M x ∘ₗ toEnd R L M y)^[k] m ∈
      lowerCentralSeries R L M (2 * k)

Proof state:
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
x y : L
m : M
k : ℕ
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)

Tactic:
induction k with
| zero => simp
| succ k ih =>
  have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
  simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
    toEnd_apply_apply, LinearMap.coe_comp, toEnd_apply_apply]
  refine LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_
  exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top y) ih

Result:
no goals

Proof state:
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ ⁅x, ⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆⁆ ∈ ⁅⊤, ⁅⊤, lowerCentralSeries R L M (2 * k)⁆⁆

Tactic:
refine LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_

Result:
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ ⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆ ∈ ⁅⊤, lowerCentralSeries R L M (2 * k)⁆

Proof state:
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k + 1] m ∈ lowerCentralSeries R L M (2 * (k + 1))

Tactic:
have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl

Result:
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k + 1] m ∈ lowerCentralSeries R L M (2 * (k + 1))

Proof state:
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ ⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆ ∈ ⁅⊤, lowerCentralSeries R L M (2 * k)⁆

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

Result:
no goals

Proof state:
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k + 1] m ∈ lowerCentralSeries R L M (2 * (k + 1))

Tactic:
simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
  toEnd_apply_apply, LinearMap.coe_comp, toEnd_apply_apply]

Result:
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ ⁅x, ⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆⁆ ∈ ⁅⊤, ⁅⊤, lowerCentralSeries R L M (2 * k)⁆⁆

Proof state:
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
x y : L
m : M
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[0] m ∈ lowerCentralSeries R L M (2 * 0)

Tactic:
simp

Result:
no goals