-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem Function.Injective.lieModuleIsNilpotent [IsNilpotent L₂ M₂] : IsNilpotent L M

Proof state:
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : ↑(lowerCentralSeries R L₂ M₂ k) = ↑⊥
⊢ ↑(lowerCentralSeries R L M k) = ↑⊥

Tactic:
apply Submodule.map_injective_of_injective hg_inj

Result:
case h.a
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : ↑(lowerCentralSeries R L₂ M₂ k) = ↑⊥
⊢ Submodule.map g ↑(lowerCentralSeries R L M k) = Submodule.map g ↑⊥

Proof state:
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : lowerCentralSeries R L₂ M₂ k = ⊥
⊢ lowerCentralSeries R L M k = ⊥

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

Result:
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : ↑(lowerCentralSeries R L₂ M₂ k) = ↑⊥
⊢ ↑(lowerCentralSeries R L M 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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
⊢ LieModule.IsNilpotent L M

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L₂ M₂

Result:
case intro
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : lowerCentralSeries R L₂ M₂ k = ⊥
⊢ LieModule.IsNilpotent L M

Proof state:
case h.a
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : ↑(lowerCentralSeries R L₂ M₂ k) = ↑⊥
⊢ Submodule.map g ↑(lowerCentralSeries R L M k) = Submodule.map g ↑⊥

Tactic:
simpa [hk] using lieModule_lcs_map_le hfg k

Result:
no goals

Proof state:
case intro
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : lowerCentralSeries R L₂ M₂ k = ⊥
⊢ LieModule.IsNilpotent L M

Tactic:
rw [isNilpotent_iff R]

Result:
case intro
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : lowerCentralSeries R L₂ M₂ k = ⊥
⊢ ∃ k, lowerCentralSeries R L M k = ⊥

Proof state:
case intro
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : lowerCentralSeries R L₂ M₂ k = ⊥
⊢ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
use k

Result:
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : lowerCentralSeries R L₂ M₂ k = ⊥
⊢ lowerCentralSeries R L M k = ⊥