awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
x : ↥W
hx : Eq (α := ↥W) ((G : (a : ↥W) → ↥W) x : ↥W) (0 : ↥W)
h : Eq (α := M) ((HPow.hPow (β := ℕ) φ 1 : (a : M) → M) (↑x : M) : M) (0 : M)
⊢ ∃ (k : ℕ), Eq (α := M) ((φ ^ k : (a : M) → M) (↑x : M) : M) (0 : M)

Tactic:
use 1
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
x : ↥W
hx : Eq (α := ↥W) ((G : (a : ↥W) → ↥W) x : ↥W) (0 : ↥W)
h : Eq (α := M) ((φ : (a : M) → M) (↑x : M) : M) (0 : M)
⊢ Eq (α := M) ((HPow.hPow (β := ℕ) φ 1 : (a : M) → M) (↑x : M) : M) (0 : M)

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
x : ↥W
hx : Eq (α := ↥W) ((G : (a : ↥W) → ↥W) x : ↥W) (0 : ↥W)
h h₁ h₂ h₃ :
  ∀ (hx : Eq.{u_3 + 1} (α := M) (↑((G : (a : ↥W) → ↥W) x) : M) (↑0 : M)),
    Eq (α := M) ((φ : (a : M) → M) (↑x : M) : M) (0 : M)
⊢ Eq (α := M) ((φ : (a : M) → M) (↑x : M) : M) (0 : M)

Tactic:
rwa [Subtype.ext_iff] at hx

Premises used: Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
⊢ G.charpoly.natTrailingDegree = 0

Tactic:
have hG : natTrailingDegree (charpoly G) = 0 := by
    apply Polynomial.natTrailingDegree_eq_zero_of_constantCoeff_ne_zero
    apply ((not_hasEigenvalue_zero_tfae G).out 2 5).mpr
    intro x hx
    apply Subtype.ext
    suffices x.1 ∈ V ⊓ W by rwa [hVW.inf_eq_bot, Submodule.mem_bot] at this
    suffices x.1 ∈ V from ⟨this, x.2⟩
    simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, V]
    use 1
    rw [pow_one]
    rwa [Subtype.ext_iff] at hx
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
rw : F.charpoly.natTrailingDegree = finrank.{u_2, u_3} K ↥V
⊢ finrank.{u_2, u_3} K ↥V = F.charpoly.natTrailingDegree + G.charpoly.natTrailingDegree

Tactic:
rw [hG, add_zero, eq_comm]

Premises used: eq_comm, add_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
apply : ∀ (m : ↥V), ∃ (n : ℕ), Eq (α := ↥V) ((F ^ n : (a : ↥V) → ↥V) m : ↥V) (0 : ↥V)
⊢ F.charpoly.natTrailingDegree = finrank.{u_2, u_3} K ↥V

Tactic:
apply ((charpoly_nilpotent_tfae F).out 2 3).mp

Premises used: LinearMap.charpoly_nilpotent_tfae, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
simp :
  ∀ (a : M) (b : ∃ (k : ℕ), Eq (α := M) ((φ ^ k : (a : M) → M) a : M) (0 : M)),
    ∃ (n : ℕ),
      Eq (α := ↥(φ.maxGenEigenspace 0))
        ((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) a ⋯) :
          ↥(φ.maxGenEigenspace 0))
        (0 : ↥V)
⊢ ∀ (m : ↥V), ∃ (n : ℕ), Eq (α := ↥V) ((F ^ n : (a : ↥V) → ↥V) m : ↥V) (0 : ↥V)

Tactic:
simp only [Subtype.forall, Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, V, F]

Premises used: sub_zero, Subtype.forall, zero_smul, Module.End.mem_maxGenEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h :
  Eq (α := ↥(φ.maxGenEigenspace 0))
    ((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
        (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯) :
      ↥(φ.maxGenEigenspace 0))
    (0 : ↥V)
⊢ ∃ (n_1 : ℕ),
    Eq (α := ↥(φ.maxGenEigenspace 0))
      ((restrict φ hφV ^ n_1 : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯) :
        ↥(φ.maxGenEigenspace 0))
      (0 : ↥V)

Tactic:
use n
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h :
  Eq.{u_3 + 1} (α := M)
    (↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
      M)
    (↑0 : M)
⊢ Eq (α := ↥(φ.maxGenEigenspace 0))
    ((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
        (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯) :
      ↥(φ.maxGenEigenspace 0))
    (0 : ↥V)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h :
  Eq.{u_3 + 1} (α := M)
    (↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
      M)
    0
⊢ Eq.{u_3 + 1} (α := M)
    (↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
      M)
    (↑0 : M)

Tactic:
rw [ZeroMemClass.coe_zero]

Premises used: ZeroMemClass.coe_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M)
    (↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
      M)
    0

Tactic:
.trans ?_ hx

Premises used: Eq.trans
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h :
  Eq (α := M)
    ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
        M) :
      M)
    ((φ ^ n : (a : M) → M) x : M)
⊢ Eq.{u_3 + 1} (α := M)
    (↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
      M)
    0

Tactic:
refine .trans ?_ hx
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h :
  ∀ (h' : x ∈ φ.maxGenEigenspace 0),
    Eq (α := M)
      ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
              (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
          M) :
        M)
      ((φ ^ n : (a : M) → M) x : M)
⊢ Eq (α := M)
    ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
        M) :
      M)
    ((φ ^ n : (a : M) → M) x : M)

Tactic:
generalize_proofs h'
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : 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, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
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.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
h' : x ∈ φ.maxGenEigenspace 0
h :
  Eq (α := M)
    ((↑((HPow.hPow (β := ℕ) (restrict φ hφV) 0 : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
        M) :
      M)
    ((HPow.hPow (β := ℕ) φ 0 : (a : M) → M) x : M)
h₁ :
  ∀ (n : ℕ),
    Eq (α := M)
        ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
                (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
            M) :
          M)
        ((φ ^ n : (a : M) → M) x : M) →
      Eq (α := M)
        ((↑((restrict φ hφV ^ (n + 1) : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
                (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
            M) :
          M)
        ((φ ^ (n + 1) : (a : M) → M) x : M)
⊢ Eq (α := M)
    ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
        M) :
      M)
    ((φ ^ n : (a : M) → M) x : M)

Tactic:
induction n