Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h.zero
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
h' : x ∈ φ.maxGenEigenspace 0
⊢ ↑((restrict φ hφV ^ 0) ⟨x, h'⟩) = (φ ^ 0) x

pp: case h.succ
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
h' : x ∈ φ.maxGenEigenspace 0
n✝ : ℕ
a✝ : ↑((restrict φ hφV ^ n✝) ⟨x, h'⟩) = (φ ^ n✝) x
⊢ ↑((restrict φ hφV ^ (n✝ + 1)) ⟨x, h'⟩) = (φ ^ (n✝ + 1)) x

Tactic:
<;>

Goal state after:
case h.zero
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
h' : x ∈ φ.maxGenEigenspace 0
⊢ ↑((restrict φ hφV ^ 0) ⟨x, h'⟩) = (φ ^ 0) x

case h.succ
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
h' : x ∈ φ.maxGenEigenspace 0
n✝ : ℕ
a✝ : ↑((restrict φ hφV ^ n✝) ⟨x, h'⟩) = (φ ^ n✝) x
⊢ ↑((restrict φ hφV ^ (n✝ + 1)) ⟨x, h'⟩) = (φ ^ (n✝ + 1)) x