-- Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
theorem Module.End.genEigenspace_restrict_eq_top
    {p : Submodule K V} {f : Module.End K V} [FiniteDimensional K V] {k : ℕ∞}
    (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ μ, f.genEigenspace μ k = ⊤) :
    ⨆ μ, Module.End.genEigenspace (LinearMap.restrict f h) μ k = ⊤

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : Submodule.comap p.subtype p = Submodule.comap p.subtype (⨆ μ, p ⊓ (f.genEigenspace μ) k)
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Tactic:
have h_inj : Function.Injective p.subtype := Subtype.coe_injective

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : Submodule.comap p.subtype p = Submodule.comap p.subtype (⨆ μ, p ⊓ (f.genEigenspace μ) k)
h_inj : Injective ⇑p.subtype
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : Submodule.comap p.subtype p = Submodule.comap p.subtype (⨆ μ, p ⊓ (f.genEigenspace μ) k)
h_inj : Injective ⇑p.subtype
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Tactic:
simp_rw [Submodule.inf_genEigenspace f p h, Submodule.comap_subtype_self,
  ← Submodule.map_iSup, Submodule.comap_map_eq_of_injective h_inj] at this

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
h_inj : Injective ⇑p.subtype
this : ⊤ = ⨆ i, (genEigenspace (LinearMap.restrict f h) i) k
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Tactic:
have := congr_arg (Submodule.comap p.subtype) (Submodule.eq_iSup_inf_genEigenspace k h h')

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : Submodule.comap p.subtype p = Submodule.comap p.subtype (⨆ μ, p ⊓ (f.genEigenspace μ) k)
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
h_inj : Injective ⇑p.subtype
this : ⊤ = ⨆ i, (genEigenspace (LinearMap.restrict f h) i) k
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Tactic:
exact this.symm

Result:
no goals