awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h_1 : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M) := h_1
n : ℕ
hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker
x : M
h₁ : Membership.mem (γ := Submodule R M) (⨆ (m : ℕ), (φ ^ m).ker) x
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)

Tactic:
rw [zero_apply, ← mem_ker, ← hn n le_rfl]

Premises used: LinearMap.zero_apply, le_rfl, LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h_1 : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M) := h_1
n : ℕ
hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker
x : M
h₁ :
  ∀ (k : ℕ) (hk : Eq (α := M) ((φ ^ k : (a : M) → M) x : M) (0 : M)),
    Membership.mem (γ := Submodule R M) (⨆ (m : ℕ), (φ ^ m).ker) x
⊢ Membership.mem (γ := Submodule R M) (⨆ (m : ℕ), (φ ^ m).ker) x

Tactic:
obtain ⟨k, hk⟩ := h x
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h_1 : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M) := h_1
n : ℕ
hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker
x : M
k : ℕ
hk : Eq (α := M) ((φ ^ k : (a : M) → M) x : M) (0 : M)
⊢ x ∈ ker (φ ^ k)

Tactic:
rw [← mem_ker] at hk

Premises used: LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h_1 : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M) := h_1
n : ℕ
hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker
x : M
k : ℕ
hk : x ∈ ker (φ ^ k)
⊢ Membership.mem (γ := Submodule R M) (⨆ (m : ℕ), (φ ^ m).ker) x

Tactic:
Submodule.mem_iSup_of_mem _ hk

Premises used: Submodule.mem_iSup_of_mem
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h_1 : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M) := h_1
n : ℕ
hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker
x : M
k : ℕ
hk : x ∈ ker (φ ^ k)
⊢ Membership.mem (γ := Submodule R M) (⨆ (m : ℕ), (φ ^ m).ker) x

Tactic:
exact Submodule.mem_iSup_of_mem _ hk

Premises used: Submodule.mem_iSup_of_mem
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
⊢ ∀ (a : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)), IsNilpotent φ

Tactic:
tfae_have 3 → 1
  | h => by
    obtain ⟨n, hn⟩ := Filter.eventually_atTop.mp <| φ.eventually_iSup_ker_pow_eq
    use n
    ext x
    rw [zero_apply, ← mem_ker, ← hn n le_rfl]
    obtain ⟨k, hk⟩ := h x
    rw [← mem_ker] at hk
    exact Submodule.mem_iSup_of_mem _ hk
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
tfae_3_to_1 : ∀ (a : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)), IsNilpotent φ
⊢ charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
tfae_3_to_1 : ∀ (a : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)), IsNilpotent φ
⊢ (charpoly φ).natTrailingDegree = finrank R M

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
tfae_3_to_1 : ∀ (a : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)), IsNilpotent φ
⊢ charpoly φ = HPow.hPow (α := R[X]) X (finrank R M) ↔ (charpoly φ).natTrailingDegree = finrank R M

Tactic:
2 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
tfae_3_to_1 : ∀ (a : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)), IsNilpotent φ
rw :
  charpoly φ = HPow.hPow (α := R[X]) X (charpoly φ).natDegree ↔ (charpoly φ).natTrailingDegree = (charpoly φ).natDegree
rw₁ rw₂ :
  (charpoly φ).natTrailingDegree = (charpoly φ).natDegree ↔ (charpoly φ).natTrailingDegree = (charpoly φ).natDegree
⊢ charpoly φ = HPow.hPow (α := R[X]) X (finrank R M) ↔ (charpoly φ).natTrailingDegree = finrank R M

Tactic:
rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree]

Premises used: LinearMap.charpoly_monic, Polynomial.Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree, LinearMap.charpoly_natDegree
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
tfae_3_to_1 : ∀ (a : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)), IsNilpotent φ
⊢ charpoly φ = HPow.hPow (α := R[X]) X (finrank R M) ↔ (charpoly φ).natTrailingDegree = finrank R M

Tactic:
tfae_have 2 ↔ 4 := by
    rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
tfae_3_to_1 : ∀ (a : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)), IsNilpotent φ
tfae_2_iff_4 : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M) ↔ (charpoly φ).natTrailingDegree = finrank R M
⊢ [IsNilpotent φ, charpoly φ = HPow.hPow (α := R[X]) X (finrank R M),
      ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M),
      (charpoly φ).natTrailingDegree = finrank R M].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
⊢ charpoly φ = HPow.hPow (α := R[X]) X (finrank R M) ↔
    ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)

Tactic:
(charpoly_nilpotent_tfae φ).out 1 2

Premises used: LinearMap.charpoly_nilpotent_tfae, List.TFAE.out, 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
⊢ φ.HasEigenvalue 0

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ IsRoot (minpoly K φ) 0

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0

Tactic:
tfae_have 1 ↔ 2 := Module.End.hasEigenvalue_iff_isRoot

Premises used: Module.End.hasEigenvalue_iff_isRoot
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
⊢ IsRoot (minpoly K φ) 0

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
⊢ Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
⊢ ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
obtain :
  ∀ (F : K[X]) (hF : charpoly φ = minpoly K φ * F) (a : IsRoot (minpoly K φ) 0),
    Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
⊢ ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)

Tactic:
obtain ⟨F, hF⟩ := minpoly_dvd_charpoly φ

Premises used: LinearMap.minpoly_dvd_charpoly
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
simp : ∀ (a : eval 0 (minpoly K φ) = 0), eval 0 (minpoly K φ) * eval 0 F = 0
⊢ ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)

Tactic:
simp only [IsRoot.def, constantCoeff_apply, coeff_zero_eq_eval_zero, hF, eval_mul]

Premises used: Polynomial.coeff_zero_eq_eval_zero, Polynomial.constantCoeff_apply, Polynomial.IsRoot.def, Polynomial.eval_mul
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
h : eval 0 (minpoly K φ) = 0
rw : 0 * eval 0 F = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := K) 0 0
⊢ eval 0 (minpoly K φ) * eval 0 F = 0

Tactic:
rw [h, zero_mul]

Premises used: MulZeroClass.zero_mul
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
⊢ ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)

Tactic:
tfae_have 2 → 3 := by
    obtain ⟨F, hF⟩ := minpoly_dvd_charpoly φ
    simp only [IsRoot.def, constantCoeff_apply, coeff_zero_eq_eval_zero, hF, eval_mul]
    intro h; rw [h, zero_mul]
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
⊢ Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
⊢ ∀ (a : Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)),
    Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
rw :
  ∀
    (a :
      Eq.{u_2 + 1} (α := K)
        (coeff
          (Matrix.charpoly.{u_2, u_3} (n := ChooseBasisIndex K M)
            ((toMatrix (chooseBasis K M) (chooseBasis K M) :
                (a : M →ₗ[K] M) → Matrix (ChooseBasisIndex K M) (ChooseBasisIndex K M) K)
              φ))
          0)
        0),
    HPow.hPow (α := K) (-1) (Fintype.card.{u_3} (ChooseBasisIndex K M)) *
        coeff
          (Matrix.charpoly.{u_2, u_3} (n := ChooseBasisIndex K M)
            ((toMatrix (chooseBasis K M) (chooseBasis K M) :
                (a : M →ₗ[K] M) → Matrix (ChooseBasisIndex K M) (ChooseBasisIndex K M) K)
              φ))
          0 =
      0
⊢ ∀ (a : Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)),
    Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)

Tactic:
rw [← LinearMap.det_toMatrix (chooseBasis K M), Matrix.det_eq_sign_charpoly_coeff,
      constantCoeff_apply, charpoly]

Premises used: Polynomial.constantCoeff_apply, LinearMap.charpoly, LinearMap.det_toMatrix, Matrix.det_eq_sign_charpoly_coeff, Module.Free.chooseBasis
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
h :
  Eq.{u_2 + 1} (α := K)
    (coeff
      (Matrix.charpoly.{u_2, u_3} (n := ChooseBasisIndex K M)
        ((toMatrix (chooseBasis K M) (chooseBasis K M) :
            (a : M →ₗ[K] M) → Matrix (ChooseBasisIndex K M) (ChooseBasisIndex K M) K)
          φ))
      0)
    0
rw : HPow.hPow (α := K) (-1) (Fintype.card.{u_3} (ChooseBasisIndex K M)) * 0 = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := K) 0 0
⊢ HPow.hPow (α := K) (-1) (Fintype.card.{u_3} (ChooseBasisIndex K M)) *
      coeff
        (Matrix.charpoly.{u_2, u_3} (n := ChooseBasisIndex K M)
          ((toMatrix (chooseBasis K M) (chooseBasis K M) :
              (a : M →ₗ[K] M) → Matrix (ChooseBasisIndex K M) (ChooseBasisIndex K M) K)
            φ))
        0 =
    0

Tactic:
rw [h, mul_zero]

Premises used: MulZeroClass.mul_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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
⊢ ∀ (a : Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)),
    Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)

Tactic:
tfae_have 3 → 4 := by
    rw [← LinearMap.det_toMatrix (chooseBasis K M), Matrix.det_eq_sign_charpoly_coeff,
      constantCoeff_apply, charpoly]
    intro h; rw [h, mul_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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
tfae_3_to_4 :
  ∀ (a : Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)),
    Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
tfae_3_to_4 :
  ∀ (a : Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)),
    Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)
⊢ ⊥ < ker φ

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
tfae_3_to_4 :
  ∀ (a : Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)),
    Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)
⊢ ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ

Tactic:
4 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
tfae_2_to_3 : ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
tfae_3_to_4 :
  ∀ (a : Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)),
    Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)
⊢ ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ

Tactic:
tfae_have 4 → 5 := bot_lt_ker_of_det_eq_zero

Premises used: LinearMap.bot_lt_ker_of_det_eq_zero