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
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) x : M) (0 : M)
h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) x : M) (0 : M)
h₂ : Eq (α := M) ((φ * φ ^ n : (a : M) → M) x : M) (0 : M)
h₃ : Eq (α := M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) x : M) : M) (0 : M)
h₄ : Eq (α := M) ((φ : (a : M) → M) 0 : M) (0 : M)
h₅ h₆ : Eq.{u_3 + 1} (α := M) 0 0
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)

Tactic:
rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply, hx, map_zero]

Premises used: pow_succ, map_zero, Module.End.mul_apply, pow_succ'
-- 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
⊢ ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)

Tactic:
have hφV : ∀ x ∈ V, φ x ∈ V := by
    simp only [V, Module.End.mem_maxGenEigenspace, zero_smul, sub_zero,
      forall_exists_index]
    intro x n hx
    use n
    rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply, hx, map_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)
simp :
  ∀ (x : M),
    (∀ (i : ℕ), ∃ (y : M), (φ ^ i : (a : M) → M) y = x) →
      ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ : (a : M) → M) x : M)
⊢ ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)

Tactic:
simp only [W, Submodule.mem_iInf, mem_range]

Premises used: Submodule.mem_iInf, LinearMap.mem_range
-- 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)
x : M
H : ∀ (i : ℕ), ∃ (y : M), (φ ^ i : (a : M) → M) y = x
n : ℕ
obtain :
  ∀ (y : M) (H : ∀ (i : ℕ), ∃ (y_1 : M), Eq (α := M) ((φ ^ i : (a : M) → M) y_1 : M) ((φ ^ n : (a : M) → M) y : M)),
    ∃ (y_1 : M), Eq (α := M) ((φ ^ n : (a : M) → M) y_1 : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
⊢ ∃ (y : M), Eq (α := M) ((φ ^ n : (a : M) → M) y : M) ((φ : (a : M) → M) x : M)

Tactic:
obtain ⟨y, rfl⟩ := H n

Premises used: rfl
-- 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)
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ (y_1 : M), Eq (α := M) ((φ ^ i : (a : M) → M) y_1 : M) ((φ ^ n : (a : M) → M) y : M)
h :
  Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) y : M) : M)
    ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
⊢ ∃ (y_1 : M), Eq (α := M) ((φ ^ n : (a : M) → M) y_1 : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)

Tactic:
use φ y

Premises used: DFunLike.coe
-- 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)
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ (y_1 : M), Eq (α := M) ((φ ^ i : (a : M) → M) y_1 : M) ((φ ^ n : (a : M) → M) y : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
h₂ : Eq (α := M) ((φ * φ ^ n : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
h₃ h₄ :
  Eq (α := M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
    ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) y : M) : M)
    ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)

Tactic:
rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply]

Premises used: pow_succ, Module.End.mul_apply, pow_succ'
-- 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)
⊢ ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)

Tactic:
have hφW : ∀ x ∈ W, φ x ∈ W := by
    simp only [W, Submodule.mem_iInf, mem_range]
    intro x H n
    obtain ⟨y, rfl⟩ := H n
    use φ y
    rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply]
-- 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
apply :
  ∀ (i : ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W),
    Eq (α := ↥V × ↥W)
      ((ψ : (a : ↥V × ↥W) → ↥V × ↥W) ((b : (a : ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) → ↥V × ↥W) i : ↥V × ↥W) :
        ↥V × ↥W)
      (((((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))
                φ :
              End K (↥V × ↥W)) :
            (a : ↥V × ↥W) → ↥V × ↥W)
          ((b : (a : ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) → ↥V × ↥W) i : ↥V × ↥W) :
        ↥V × ↥W)
⊢ ψ =
    ((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))
      φ

Tactic:
apply b.ext

Premises used: Module.Basis.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
⊢ ∀ (i : ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W),
    Eq (α := ↥V × ↥W)
      ((ψ : (a : ↥V × ↥W) → ↥V × ↥W) ((b : (a : ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) → ↥V × ↥W) i : ↥V × ↥W) :
        ↥V × ↥W)
      (((((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))
                φ :
              End K (↥V × ↥W)) :
            (a : ↥V × ↥W) → ↥V × ↥W)
          ((b : (a : ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) → ↥V × ↥W) i : ↥V × ↥W) :
        ↥V × ↥W)

Tactic:
simp only [Basis.prod_apply, coe_inl, coe_inr, prodMap_apply, LinearEquiv.conj_apply,
      LinearEquiv.symm_symm, Submodule.coe_prodEquivOfIsCompl, coe_comp, LinearEquiv.coe_coe,
      Function.comp_apply, coprod_apply, Submodule.coe_subtype, map_add, Sum.forall, Sum.elim_inl,
      map_zero, ZeroMemClass.coe_zero, add_zero, LinearEquiv.eq_symm_apply, and_self,
      Submodule.coe_prodEquivOfIsCompl', coe_restrict_apply, implies_true, Sum.elim_inr, zero_add,
      e, V, W, ψ, F, G, b]

Premises used: LinearMap.prodMap_apply, LinearMap.coe_inr, and_self, LinearEquiv.eq_symm_apply, LinearMap.coe_restrict_apply, Submodule.coe_prodEquivOfIsCompl', Submodule.coe_prodEquivOfIsCompl, LinearMap.coprod_apply, map_zero, Module.Basis.prod_apply, map_add, LinearEquiv.conj_apply, zero_add, LinearEquiv.symm_symm, Sum.elim_inr, ZeroMemClass.coe_zero, LinearMap.coe_inl, LinearMap.coe_comp, Submodule.coe_subtype, Sum.elim_inl, Function.comp_apply, implies_true, Sum.forall, add_zero, LinearEquiv.coe_coe
-- 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
⊢ ψ =
    ((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))
      φ

Tactic:
have hψ : ψ = e.symm.conj φ := by
    apply b.ext
    simp only [Basis.prod_apply, coe_inl, coe_inr, prodMap_apply, LinearEquiv.conj_apply,
      LinearEquiv.symm_symm, Submodule.coe_prodEquivOfIsCompl, coe_comp, LinearEquiv.coe_coe,
      Function.comp_apply, coprod_apply, Submodule.coe_subtype, map_add, Sum.forall, Sum.elim_inl,
      map_zero, ZeroMemClass.coe_zero, add_zero, LinearEquiv.eq_symm_apply, and_self,
      Submodule.coe_prodEquivOfIsCompl', coe_restrict_apply, implies_true, Sum.elim_inr, zero_add,
      e, V, W, ψ, F, G, b]
-- 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))
      φ
rw : finrank.{u_2, u_3} K ↥V = F.charpoly.natTrailingDegree + G.charpoly.natTrailingDegree
⊢ finrank.{u_2, u_3} K ↥V = (charpoly φ).natTrailingDegree

Tactic:
rw [← e.symm.charpoly_conj φ, ← hψ, charpoly_prodMap,
    natTrailingDegree_mul (charpoly_monic _).ne_zero (charpoly_monic _).ne_zero]

Premises used: LinearEquiv.symm, LinearMap.charpoly_monic, LinearMap.charpoly_prodMap, LinearEquiv.charpoly_conj, Polynomial.natTrailingDegree_mul, Polynomial.Monic.ne_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))
      φ
h : Ne (α := K) ((constantCoeff : (a : K[X]) → K) G.charpoly : K) (0 : K)
⊢ G.charpoly.natTrailingDegree = 0

Tactic:
apply Polynomial.natTrailingDegree_eq_zero_of_constantCoeff_ne_zero

Premises used: Polynomial.natTrailingDegree_eq_zero_of_constantCoeff_ne_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))
      φ
h : ∀ (m : ↥W), Eq (α := ↥W) ((G : (a : ↥W) → ↥W) m : ↥W) (0 : ↥W) → m = 0
⊢ Ne (α := K) ((constantCoeff : (a : K[X]) → K) G.charpoly : K) (0 : K)

Tactic:
apply ((not_hasEigenvalue_zero_tfae G).out 2 5).mpr

Premises used: Iff.mpr, List.TFAE.out, LinearMap.not_hasEigenvalue_zero_tfae, 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))
      φ
x : ↥W
hx : Eq (α := ↥W) ((G : (a : ↥W) → ↥W) x : ↥W) (0 : ↥W)
h : (↑x : M) = (↑0 : M)
⊢ x = 0

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))
      φ
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)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : (↑x : M) = 0), (↑x : M) = (↑0 : M)
⊢ (↑x : M) = (↑0 : M)

Tactic:
rwa [hVW.inf_eq_bot, Submodule.mem_bot] at this

Premises used: Submodule.mem_bot, IsCompl.inf_eq_bot
-- 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 : (↑x : M) ∈ V ⊓ W
⊢ (↑x : M) = (↑0 : M)

Tactic:
suffices x.1 ∈ V ⊓ W by rwa [hVW.inf_eq_bot, Submodule.mem_bot] at this
-- 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 : (↑x : M) ∈ V
⊢ (↑x : M) ∈ V ⊓ W

Tactic:
suffices x.1 ∈ V from ⟨this, x.2⟩
-- 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 : ∃ (k : ℕ), Eq (α := M) ((φ ^ k : (a : M) → M) (↑x : M) : M) (0 : M)
⊢ (↑x : M) ∈ V

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

Premises used: sub_zero, zero_smul, Module.End.mem_maxGenEigenspace