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
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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
⊢ ⊥ < 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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
⊢ ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)

Tactic:
6

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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
⊢ ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)

Tactic:
5 → 6

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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
contrapose! : (∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)) → ¬⊥ < ker φ
⊢ ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)

Tactic:
contrapose!
-- 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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
simp : (∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)) → ker φ ≤ ⊥
⊢ (∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)) → ¬⊥ < ker φ

Tactic:
simp only [not_bot_lt_iff, eq_bot_iff]

Premises used: not_bot_lt_iff, eq_bot_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
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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
h : ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)
x : M
contrapose! : x ≠ 0 → Ne (α := M) ((φ : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((φ : (a : M) → M) x : M) (0 : M) → x = 0

Tactic:
contrapose!
-- 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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
h : ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)
x : M
⊢ x ≠ 0 → Ne (α := M) ((φ : (a : M) → M) x : M) (0 : M)

Tactic:
apply 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
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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
⊢ ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)

Tactic:
tfae_have 5 → 6 := by
    contrapose!
    simp only [not_bot_lt_iff, eq_bot_iff]
    intro h x
    simp only [mem_ker, Submodule.mem_bot]
    contrapose!
    apply 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
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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
tfae_5_to_6 : ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)
⊢ ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)

Tactic:
6

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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
tfae_5_to_6 : ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : 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
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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
tfae_5_to_6 : ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)
⊢ ∀ (a : ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)), φ.HasEigenvalue 0

Tactic:
6 → 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
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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
tfae_5_to_6 : ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)
x : M
h1 : x ≠ 0
h2 : Eq (α := M) ((φ : (a : M) → M) x : M) (0 : M)
apply : Membership.mem (γ := Submodule K M) ((φ.genEigenspace 0 : (a : ℕ∞) → Submodule K M) 1 : Submodule K M) x
⊢ φ.HasEigenvalue 0

Tactic:
apply Module.End.hasEigenvalue_of_hasEigenvector ⟨_, h1⟩

Premises used: Module.End.hasEigenvalue_of_hasEigenvector, And.intro
-- 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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
tfae_5_to_6 : ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)
x : M
h1 : x ≠ 0
h2 : Eq (α := M) ((φ : (a : M) → M) x : M) (0 : M)
⊢ Membership.mem (γ := Submodule K M) ((φ.genEigenspace 0 : (a : ℕ∞) → Submodule K M) 1 : Submodule K M) x

Tactic:
simpa only [Module.End.eigenspace_zero, mem_ker] using h2

Premises used: LinearMap.mem_ker, Module.End.eigenspace_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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
tfae_5_to_6 : ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)
⊢ ∀ (a : ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)), φ.HasEigenvalue 0

Tactic:
tfae_have 6 → 1
  | ⟨x, h1, h2⟩ => by
    apply Module.End.hasEigenvalue_of_hasEigenvector ⟨_, h1⟩
    simpa only [Module.End.eigenspace_zero, mem_ker] using h2
-- 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)
tfae_4_to_5 : ∀ (a : Eq.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K)), ⊥ < ker φ
tfae_5_to_6 : ∀ (a : ⊥ < ker φ), ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)
tfae_6_to_1 : ∀ (a : ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)), φ.HasEigenvalue 0
⊢ [φ.HasEigenvalue 0, 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), ⊥ < ker φ,
      ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE

Tactic:
tfae_finish
-- 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
⊢ Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K) ↔
    ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)

Tactic:
(hasEigenvalue_zero_tfae φ).out 2 5

Premises used: LinearMap.hasEigenvalue_zero_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
⊢ (List.map Not
      [φ.HasEigenvalue 0, 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), ⊥ < ker φ,
        ∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)]).TFAE

Tactic:
have := (hasEigenvalue_zero_tfae φ).not
-- 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
this :
  [¬φ.HasEigenvalue 0, ¬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), ¬⊥ < ker φ,
      ¬∃ (m : M), m ≠ 0 ∧ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
⊢ [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE

Tactic:
push Not at this

Premises used: Not
-- 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
this :
  [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
m : M
⊢ m ≠ 0 → Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M) ↔ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0

Tactic:
apply not_imp_not

Premises used: not_imp_not
-- 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
this :
  [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
⊢ ∀ (m : M),
    m ≠ 0 → Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M) ↔ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0

Tactic:
have aux₁ : ∀ m, (m ≠ 0 → φ m ≠ 0) ↔ (φ m = 0 → m = 0) := by intro m; apply not_imp_not
-- 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
this :
  [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
aux₁ :
  ∀ (m : M),
    m ≠ 0 → Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M) ↔ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0
rw : ker φ = ⊥ ↔ ¬ker φ ≠ ⊥
rw₁ rw₂ : ker φ = ⊥ ↔ ker φ = ⊥
⊢ ker φ = ⊥ ↔ ¬⊥ < ker φ

Tactic:
rw [bot_lt_iff_ne_bot, not_not]

Premises used: Classical.not_not, bot_lt_iff_ne_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
this :
  [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
aux₁ :
  ∀ (m : M),
    m ≠ 0 → Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M) ↔ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0
⊢ ker φ = ⊥ ↔ ¬⊥ < ker φ

Tactic:
have aux₂ : ker φ = ⊥ ↔ ¬ ⊥ < ker φ := by rw [bot_lt_iff_ne_bot, not_not]
-- 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
this :
  [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
aux₁ :
  ∀ (m : M),
    m ≠ 0 → Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M) ↔ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0
aux₂ : ker φ = ⊥ ↔ ¬⊥ < ker φ
⊢ [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ker φ = ⊥,
      ∀ (m : M), Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0].TFAE

Tactic:
simpa only [aux₁, aux₂] using 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
set :
  let V := φ.maxGenEigenspace 0;
  finrank.{u_2, u_3} K ↥V = (charpoly φ).natTrailingDegree
⊢ finrank.{u_2, u_3} K ↥(φ.maxGenEigenspace 0) = (charpoly φ).natTrailingDegree

Tactic:
set V := φ.maxGenEigenspace 0

Premises used: Module.End.maxGenEigenspace, 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
⊢ V = ⨆ (n : ℕ), ker (φ ^ n)

Tactic:
simp [V, ← Module.End.iSup_genEigenspace_eq, Module.End.genEigenspace_nat]

Premises used: Module.End.iSup_genEigenspace_eq, Module.End.genEigenspace_nat
-- 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
⊢ V = ⨆ (n : ℕ), ker (φ ^ n)

Tactic:
have hV : V = ⨆ (n : ℕ), ker (φ ^ n) := by
    simp [V, ← Module.End.iSup_genEigenspace_eq, Module.End.genEigenspace_nat]
-- 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)
rw : IsCompl (⨆ (n : ℕ), ker (φ ^ n)) W
⊢ IsCompl V W

Tactic:
rw [hV]
-- 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)
⊢ IsCompl (⨆ (n : ℕ), ker (φ ^ n)) W

Tactic:
LinearMap.isCompl_iSup_ker_pow_iInf_range_pow φ

Premises used: Set.Mem, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, setOf
-- 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)
⊢ IsCompl (⨆ (n : ℕ), ker (φ ^ n)) W

Tactic:
exact LinearMap.isCompl_iSup_ker_pow_iInf_range_pow φ

Premises used: LinearMap.isCompl_iSup_ker_pow_iInf_range_pow
-- 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)
⊢ IsCompl V W

Tactic:
have hVW : IsCompl V W := by
    rw [hV]
    exact LinearMap.isCompl_iSup_ker_pow_iInf_range_pow φ
-- 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
simp :
  ∀ (x : M) (x_1 : ℕ) (h : Eq (α := M) ((φ ^ x_1 : (a : M) → M) x : M) (0 : M)),
    ∃ (k : ℕ), Eq (α := M) ((φ ^ k : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
⊢ ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)

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

Premises used: sub_zero, forall_exists_index, 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
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h : Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
⊢ ∃ (k : ℕ), Eq (α := M) ((φ ^ k : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)

Tactic:
use n