-- Mathlib/Algebra/Lie/Nilpotent.lean
lemma map_lowerCentralSeries_eq {f : M →ₗ⁅R,L⁆ M₂} (hf : Function.Surjective f) :
    (lowerCentralSeries R L M k).map f = lowerCentralSeries R L M₂ 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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ lowerCentralSeries R L M₂ 0 ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)

Tactic:
rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
  f.range_eq_top]

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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
n✝ : ℕ
a✝ : lowerCentralSeries R L M₂ n✝ ≤ LieSubmodule.map f (lowerCentralSeries R L M n✝)
⊢ lowerCentralSeries R L M₂ (n✝ + 1) ≤ LieSubmodule.map f (lowerCentralSeries R L M (n✝ + 1))

Tactic:
simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]

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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
n✝ : ℕ
a✝ : lowerCentralSeries R L M₂ n✝ ≤ LieSubmodule.map f (lowerCentralSeries R L M n✝)
⊢ ⁅⊤, lowerCentralSeries R L M₂ n✝⁆ ≤ ⁅⊤, LieSubmodule.map f (lowerCentralSeries R L M n✝)⁆

Proof state:
case succ.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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
n✝ : ℕ
a✝ : lowerCentralSeries R L M₂ n✝ ≤ LieSubmodule.map f (lowerCentralSeries R L M n✝)
⊢ lowerCentralSeries R L M₂ n✝ ≤ LieSubmodule.map f (lowerCentralSeries R L M n✝)

Tactic:
assumption

Result:
no goals

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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)

Tactic:
induction k with
| zero =>
  rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
    f.range_eq_top]
| succ =>
  simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
  apply LieSubmodule.mono_lie_right
  assumption

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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
n✝ : ℕ
a✝ : lowerCentralSeries R L M₂ n✝ ≤ LieSubmodule.map f (lowerCentralSeries R L M n✝)
⊢ ⁅⊤, lowerCentralSeries R L M₂ n✝⁆ ≤ ⁅⊤, LieSubmodule.map f (lowerCentralSeries R L M n✝)⁆

Tactic:
apply LieSubmodule.mono_lie_right

Result:
case succ.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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
n✝ : ℕ
a✝ : lowerCentralSeries R L M₂ n✝ ≤ LieSubmodule.map f (lowerCentralSeries R L M n✝)
⊢ lowerCentralSeries R L M₂ n✝ ≤ LieSubmodule.map f (lowerCentralSeries R L M n✝)

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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) = lowerCentralSeries R L M₂ k

Tactic:
apply le_antisymm (map_lowerCentralSeries_le k f)

Result:
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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)