awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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
have h : Ne (α := K) ((constantCoeff : (a : K[X]) → K) G.charpoly : K) (0 : K)
Tactic: apply Polynomial.natTrailingDegree_eq_zero_of_constantCoeff_ne_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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))
      φ
⊢ Ne (α := K) ((constantCoeff : (a : K[X]) → K) G.charpoly : K) (0 : K)
have h : ∀ (m : ↥W), Eq (α := ↥W) ((G : (a : ↥W) → ↥W) m : ↥W) (0 : ↥W) → m = 0
Tactic: apply ((not_hasEigenvalue_zero_tfae G).out 2 5).mpr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
⊢ x = 0
have h : (↑x : M) = (↑0 : M)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
this : (↑x : M) ∈ V ⊓ W
⊢ (↑x : M) = (↑0 : M)
have rwa : ∀ (this : Membership.mem (γ := Submodule K M) ⊥ (↑x : M)), (↑x : M) = (↑0 : M)
Tactic: rwa [hVW.inf_eq_bot, Submodule.mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
this : (↑x : M) ∈ V ⊓ W
rwa : ∀ (this : Membership.mem (γ := Submodule K M) ⊥ (↑x : M)), (↑x : M) = (↑0 : M)
⊢ (↑x : M) = (↑0 : M)
have rwa₁ : ∀ (this : (↑x : M) = 0), (↑x : M) = (↑0 : M)
Tactic: rwa [hVW.inf_eq_bot, Submodule.mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
⊢ (↑x : M) = (↑0 : M)
have h : (↑x : M) ∈ V ⊓ W
Tactic: suffices x.1 ∈ V ⊓ W by rwa [hVW.inf_eq_bot, Submodule.mem_bot] at this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
⊢ (↑x : M) ∈ V ⊓ W
have h : (↑x : M) ∈ V
Tactic: suffices x.1 ∈ V from ⟨this, x.2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
⊢ (↑x : M) ∈ V
have h : ∃ (k : ℕ), Eq (α := M) ((φ ^ k : (a : M) → M) (↑x : M) : M) (0 : M)
Tactic: simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, V]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
⊢ ∃ (k : ℕ), Eq (α := M) ((φ ^ k : (a : M) → M) (↑x : M) : M) (0 : M)
have h : Eq (α := M) ((HPow.hPow (β := ℕ) φ 1 : (a : M) → M) (↑x : M) : M) (0 : M)
Tactic: use 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
⊢ Eq (α := M) ((HPow.hPow (β := ℕ) φ 1 : (a : M) → M) (↑x : M) : M) (0 : M)
have h : Eq (α := M) ((φ : (a : M) → M) (↑x : M) : M) (0 : M)
Tactic: rw [pow_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
⊢ Eq (α := M) ((φ : (a : M) → M) (↑x : M) : M) (0 : M)
have 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)
Tactic: rwa [Subtype.ext_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
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))
      φ
⊢ finrank.{u_2, u_3} K ↥V = F.charpoly.natTrailingDegree + G.charpoly.natTrailingDegree
have hG : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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
⊢ finrank.{u_2, u_3} K ↥V = F.charpoly.natTrailingDegree + G.charpoly.natTrailingDegree
have rw : F.charpoly.natTrailingDegree = finrank.{u_2, u_3} K ↥V
Tactic: rw [hG, add_zero, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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
⊢ F.charpoly.natTrailingDegree = finrank.{u_2, u_3} K ↥V
have apply : ∀ (m : ↥V), ∃ (n : ℕ), Eq (α := ↥V) ((F ^ n : (a : ↥V) → ↥V) m : ↥V) (0 : ↥V)
Tactic: apply ((charpoly_nilpotent_tfae F).out 2 3).mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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
⊢ ∀ (m : ↥V), ∃ (n : ℕ), Eq (α := ↥V) ((F ^ n : (a : ↥V) → ↥V) m : ↥V) (0 : ↥V)
have 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 sorry) :
        ↥(φ.maxGenEigenspace 0))
      (0 : ↥V)
Tactic: simp only [Subtype.forall, Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, V, F]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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)
⊢ ∃ (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)
have h : Eq (α := ↥(φ.maxGenEigenspace 0))
  ((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
      (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x sorry) :
    ↥(φ.maxGenEigenspace 0))
  (0 : ↥V)
Tactic: use n