-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
lemma isNilpotent_restrict_of_le {f : End R M} {p q : Submodule R M}
    {hp : MapsTo f p p} {hq : MapsTo f q q} (h : p ≤ q) (hf : IsNilpotent (f.restrict hq)) :
    IsNilpotent (f.restrict hp)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
hf : IsNilpotent (LinearMap.restrict f hq)
⊢ IsNilpotent (LinearMap.restrict f hp)

Tactic:
obtain ⟨n, hn⟩ := hf

Result:
case intro
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
⊢ IsNilpotent (LinearMap.restrict f hp)

Proof state:
case h.h.mk.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : (LinearMap.restrict f hq ^ n) ⟨x, ⋯⟩ = 0
⊢ (LinearMap.restrict f hp ^ n) ⟨x, hx⟩ = 0

Tactic:
rw [LinearMap.pow_restrict, LinearMap.restrict_apply] at hn ⊢

Result:
case h.h.mk.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : ⟨(f ^ n) ↑⟨x, ⋯⟩, ⋯⟩ = 0
⊢ ⟨(f ^ n) ↑⟨x, hx⟩, ⋯⟩ = 0

Proof state:
case h.h.mk.a.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : ⟨(f ^ n) ↑⟨x, ⋯⟩, ⋯⟩ = 0
⊢ ↑⟨(f ^ n) ↑⟨x, hx⟩, ⋯⟩ = ↑0

Tactic:
exact (congr_arg Subtype.val hn :)

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
⊢ IsNilpotent (LinearMap.restrict f hp)

Tactic:
use n

Result:
case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
⊢ LinearMap.restrict f hp ^ n = 0

Proof state:
case h.h.mk.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : ⟨(f ^ n) ↑⟨x, ⋯⟩, ⋯⟩ = 0
⊢ ⟨(f ^ n) ↑⟨x, hx⟩, ⋯⟩ = 0

Tactic:
ext

Result:
case h.h.mk.a.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : ⟨(f ^ n) ↑⟨x, ⋯⟩, ⋯⟩ = 0
⊢ ↑⟨(f ^ n) ↑⟨x, hx⟩, ⋯⟩ = ↑0

Proof state:
case h.h.mk.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
x : M
hx : x ∈ p
⊢ ↑((LinearMap.restrict f hp ^ n) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Tactic:
replace hn := DFunLike.congr_fun hn ⟨x, h hx⟩

Result:
case h.h.mk.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : (LinearMap.restrict f hq ^ n) ⟨x, ⋯⟩ = 0 ⟨x, ⋯⟩
⊢ ↑((LinearMap.restrict f hp ^ n) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Proof state:
case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
⊢ LinearMap.restrict f hp ^ n = 0

Tactic:
ext ⟨x, hx⟩

Result:
case h.h.mk.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
x : M
hx : x ∈ p
⊢ ↑((LinearMap.restrict f hp ^ n) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Proof state:
case h.h.mk.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : (LinearMap.restrict f hq ^ n) ⟨x, ⋯⟩ = 0 ⟨x, ⋯⟩
⊢ ↑((LinearMap.restrict f hp ^ n) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Tactic:
simp_rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero] at hn ⊢

Result:
case h.h.mk.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : (LinearMap.restrict f hq ^ n) ⟨x, ⋯⟩ = 0
⊢ (LinearMap.restrict f hp ^ n) ⟨x, hx⟩ = 0