-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem isNilpotent_of_le (M₁ M₂ : LieSubmodule R L M) (h₁ : M₁ ≤ M₂) [IsNilpotent L M₂] :
    IsNilpotent L M₁

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
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
⊢ ∀ (x : L) (m : ↥M₁), ⁅f x, g m⁆ = g ⁅x, m⁆

Tactic:
aesop

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
inst✝¹ : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
⊢ IsNilpotent L ↥M₁

Tactic:
let g : M₁ →ₗ[R] M₂ := Submodule.inclusion h₁

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
inst✝¹ : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
⊢ IsNilpotent L ↥M₁

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
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
hfg : ∀ (x : L) (m : ↥M₁), ⁅f x, g m⁆ = g ⁅x, m⁆
⊢ IsNilpotent L ↥M₁

Tactic:
exact (Submodule.inclusion_injective h₁).lieModuleIsNilpotent hfg

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
inst✝¹ : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
⊢ IsNilpotent L ↥M₁

Tactic:
have hfg : ∀ x m, ⁅f x, g m⁆ = g ⁅x, m⁆ := by aesop

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
inst✝¹ : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
hfg : ∀ (x : L) (m : ↥M₁), ⁅f x, g m⁆ = g ⁅x, m⁆
⊢ IsNilpotent L ↥M₁

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
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
⊢ IsNilpotent L ↥M₁

Tactic:
let f : L →ₗ⁅R⁆ L := LieHom.id

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
inst✝¹ : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
⊢ IsNilpotent L ↥M₁