awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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
⊢ Membership.mem (γ := Submodule R M) (⨆ (m : ℕ), (φ ^ m).ker) x
have h₁ : ∀ (k : ℕ) (hk : Eq (α := M) ((φ ^ k : (a : M) → M) x : M) (0 : M)),
  Membership.mem (γ := Submodule R M) (⨆ (m : ℕ), (φ ^ m).ker) x
Tactic: obtain ⟨k, hk⟩ := h x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
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)
⊢ Membership.mem (γ := Submodule R M) (⨆ (m : ℕ), (φ ^ m).ker) x
have hk₁ : x ∈ ker (φ ^ k)
Tactic: rw [← mem_ker] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
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)
⊢ [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
have tfae_3_to_1 : ∀ (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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
have rw : charpoly φ = HPow.hPow (α := R[X]) X (charpoly φ).natDegree ↔ (charpoly φ).natTrailingDegree = (charpoly φ).natDegree
Tactic: rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
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
⊢ charpoly φ = HPow.hPow (α := R[X]) X (finrank R M) ↔ (charpoly φ).natTrailingDegree = finrank R M
have rw₁ : (charpoly φ).natTrailingDegree = (charpoly φ).natDegree ↔ (charpoly φ).natTrailingDegree = (charpoly φ).natDegree
Tactic: rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
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 φ
⊢ [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
have tfae_2_iff_4 : 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]
-- 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
⊢ [φ.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
have tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
Tactic: tfae_have 1 ↔ 2 := Module.End.hasEigenvalue_iff_isRoot
-- 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
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)
have 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)
Tactic: obtain ⟨F, hF⟩ := minpoly_dvd_charpoly φ
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
⊢ ∀ (a : IsRoot (minpoly K φ) 0), Eq (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K)
have simp : ∀ (a : eval 0 (minpoly K φ) = 0), eval 0 (minpoly K φ) * eval 0 F = 0
Tactic: simp only [IsRoot.def, constantCoeff_apply, coeff_zero_eq_eval_zero, hF, eval_mul]
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
h : eval 0 (minpoly K φ) = 0
⊢ eval 0 (minpoly K φ) * eval 0 F = 0
have rw : 0 * eval 0 F = 0
Tactic: rw [h, zero_mul]
-- 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
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
⊢ eval 0 (minpoly K φ) * eval 0 F = 0
have rw₁ : Eq.{u_2 + 1} (α := K) 0 0
Tactic: rw [h, zero_mul]
-- 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ IsRoot (minpoly K φ) 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
have tfae_2_to_3 : ∀ (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]
-- 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
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)
have 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
Tactic: rw [← LinearMap.det_toMatrix (chooseBasis K M), Matrix.det_eq_sign_charpoly_coeff,
      constantCoeff_apply, charpoly]
-- 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
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
⊢ 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
have rw : HPow.hPow (α := K) (-1) (Fintype.card.{u_3} (ChooseBasisIndex K M)) * 0 = 0
Tactic: rw [h, mul_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
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
⊢ 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
have rw₁ : Eq.{u_2 + 1} (α := K) 0 0
Tactic: rw [h, mul_zero]
-- 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
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)
⊢ [φ.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
have 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)
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]
-- 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
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)
⊢ [φ.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
have tfae_4_to_5 : ∀ (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
-- 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
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)
have contrapose! : (∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)) → ¬⊥ < ker φ
Tactic: contrapose!
-- 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
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), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)) → ¬⊥ < ker φ
have simp : (∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)) → ker φ ≤ ⊥
Tactic: simp only [not_bot_lt_iff, eq_bot_iff]
-- 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
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
⊢ Eq (α := M) ((φ : (a : M) → M) x : M) (0 : M) → x = 0
have contrapose! : x ≠ 0 → Ne (α := M) ((φ : (a : M) → M) x : M) (0 : M)
Tactic: contrapose!
-- 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
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 φ
⊢ [φ.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
have tfae_5_to_6 : ∀ (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
-- 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
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)
⊢ φ.HasEigenvalue 0
have apply : Membership.mem (γ := Submodule K M) ((φ.genEigenspace 0 : (a : ℕ∞) → Submodule K M) 1 : Submodule K M) x
Tactic: apply Module.End.hasEigenvalue_of_hasEigenvector ⟨_, h1⟩
-- 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
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, 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
have tfae_6_to_1 : ∀ (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
-- 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
⊢ [¬φ.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
have this : (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
-- 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
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), Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0].TFAE
have 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
Tactic: push Not at this
Cleared hypotheses: this