awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
rcases :
  ∀ (w : M)
    (H : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) w)
    (ne0 : w ≠ 0), IsRoot (minpoly R f) μ
⊢ IsRoot (minpoly R f) μ

Tactic:
rcases (Submodule.ne_bot_iff _).1 h with ⟨w, ⟨H, ne0⟩⟩

Premises used: Submodule.ne_bot_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) w
ne0 : w ≠ 0
⊢ IsRoot (minpoly R f) μ

Tactic:
Or.resolve_right (smul_eq_zero.1 ?_) ne0

Premises used: Iff.mp, Or.resolve_right, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) w
ne0 : w ≠ 0
refine : eval μ (minpoly R f) • w = 0
⊢ IsRoot (minpoly R f) μ

Tactic:
refine Or.resolve_right (smul_eq_zero.1 ?_) ne0

Premises used: Iff.mp, Or.resolve_right, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) w
ne0 : w ≠ 0
rw : Eq (α := M) ((((aeval f : (a : R[X]) → End R M) (minpoly R f) : End R M) : (a : M) → M) w : M) (0 : M)
⊢ eval μ (minpoly R f) • w = 0

Tactic:
rw [← aeval_apply_of_hasEigenvector ⟨H, ne0⟩]

Premises used: Module.End.aeval_apply_of_hasEigenvector, And.intro
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) w
ne0 : w ≠ 0
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → End R M) (minpoly R f) : End R M) : (a : M) → M) w : M) (0 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
obtain :
  ∀ (q : R[X]) (hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q),
    f.HasEigenvalue μ
⊢ f.HasEigenvalue μ

Tactic:
obtain ⟨q, hq⟩ := dvd_iff_isRoot.mpr h

Premises used: Iff.mpr, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
by_contra! :
  ∀ (h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)),
    False
⊢ ∃ (v : M), Ne (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)

Tactic:
by_contra! h_contra
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
⊢ degree (minpoly R f) ≤ q.degree

Tactic:
have := minpoly.min R f
      ((monic_X_sub_C μ).of_mul_monic_left (hq ▸ minpoly.monic (Algebra.IsIntegral.isIntegral f)))
      (LinearMap.ext h_contra)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
this : degree (minpoly R f) ≤ q.degree
rw : ∀ (this : HAdd.hAdd (α := WithBot ℕ) 1 (↑q.natDegree : WithBot ℕ) ≤ (↑q.natDegree : WithBot ℕ)), False
rw₁ : ∀ (this : 1 + q.degree ≤ q.degree), q ≠ 0
⊢ False

Tactic:
rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this

Premises used: Polynomial.degree_eq_natDegree, Polynomial.degree_X_sub_C, Polynomial.degree_mul
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
this : HAdd.hAdd (α := WithBot ℕ) 1 (↑q.natDegree : WithBot ℕ) ≤ (↑q.natDegree : WithBot ℕ)
⊢ 1 + q.natDegree ≤ q.natDegree

Tactic:
norm_cast at this
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
this : 1 + q.natDegree ≤ q.natDegree
⊢ False

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * 0
h_contra : ∀ (v : M), Eq (α := M) (((aeval f : (a : R[X]) → End R M) 0 : (a : M) → M) v : M) (0 : M)
this : 1 + degree.{v} (R := R) 0 ≤ degree.{v} (R := R) 0
⊢ False

Tactic:
minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.ne_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * 0
h_contra : ∀ (v : M), Eq (α := M) (((aeval f : (a : R[X]) → End R M) 0 : (a : M) → M) v : M) (0 : M)
this : 1 + degree.{v} (R := R) 0 ≤ degree.{v} (R := R) 0
⊢ False

Tactic:
exact minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.ne_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
obtain :
  ∀ (v : M) (hv : Ne (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)),
    f.HasEigenvalue μ
⊢ f.HasEigenvalue μ

Tactic:
obtain ⟨v, hv⟩ : ∃ v : M, q.aeval f v ≠ 0 := by
    by_contra! h_contra
    have := minpoly.min R f
      ((monic_X_sub_C μ).of_mul_monic_left (hq ▸ minpoly.monic (Algebra.IsIntegral.isIntegral f)))
      (LinearMap.ext h_contra)
    rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this
    · norm_cast at this; grind
    · rintro rfl
      exact minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
v : M
hv : Ne (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
⊢ f.HasEigenvalue μ

Tactic:
Module.End.hasEigenvalue_of_hasEigenvector (hasEigenvector_iff.mpr ⟨?_, hv⟩)

Premises used: Iff.mpr, Module.End.hasEigenvalue_of_hasEigenvector, Module.End.hasEigenvector_iff, And.intro
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
v : M
hv : Ne (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
refine : Membership.mem (α := M) (f.eigenspace μ) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M)
⊢ f.HasEigenvalue μ

Tactic:
refine Module.End.hasEigenvalue_of_hasEigenvector (hasEigenvector_iff.mpr ⟨?_, hv⟩)

Premises used: Iff.mpr, Module.End.hasEigenvalue_of_hasEigenvector, Module.End.hasEigenvector_iff, And.intro
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
v : M
hv : Ne (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
⊢ Membership.mem (α := M) (f.eigenspace μ) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M)

Tactic:
simpa [sub_eq_zero, hq] using congr($(minpoly.aeval R f) v)

Premises used: sub_eq_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
⊢ f.HasEigenvalue μ ↔ IsRoot (minpoly R f) μ

Tactic:
⟨isRoot_of_hasEigenvalue, hasEigenvalue_of_isRoot⟩

Premises used: Module.End.isRoot_of_hasEigenvalue, Iff.intro, Module.End.hasEigenvalue_of_isRoot
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
⊢ Ne (α := R[X]) (minpoly R f) 0

Tactic:
have h : minpoly R f ≠ 0 := minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := R) f)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
⊢ (rootSet (minpoly R f) R).Finite

Tactic:
(minpoly R f).rootSet_finite R

Premises used: minpoly, Polynomial.rootSet_finite
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
h₁ : f.HasEigenvalue = rootSet (minpoly R f) R
⊢ Set.Finite f.HasEigenvalue

Tactic:
convert! (minpoly R f).rootSet_finite R

Premises used: minpoly, Polynomial.rootSet_finite
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
h₁ : ∀ (μ : R), μ ∈ f.HasEigenvalue ↔ μ ∈ rootSet (minpoly R f) R
⊢ f.HasEigenvalue = rootSet (minpoly R f) R

Tactic:
ext μ
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
μ : R
h₁ : IsRoot (minpoly R f) μ ↔ μ ∈ rootSet (minpoly R f) R
h₂ : IsRoot (minpoly R f) μ ↔ Eq (α := R) ((aeval μ : (a : R[X]) → R) (minpoly R f) : R) (0 : R)
h₃ : eval μ (minpoly R f) = 0 ↔ Eq (α := R) ((aeval μ : (a : R[X]) → R) (minpoly R f) : R) (0 : R)
h₄ h₅ : eval μ (minpoly R f) = 0 ↔ eval μ (minpoly R f) = 0
⊢ f.HasEigenvalue μ ↔ μ ∈ rootSet (minpoly R f) R

Tactic:
rw [hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]

Premises used: Polynomial.IsRoot, Module.End.hasEigenvalue_iff_isRoot, Polynomial.mem_rootSet_of_ne, Polynomial.coe_aeval_eq_eval
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
hb : q.leadingCoeff ≠ 0
⊢ f.eigenspace (-q.coeff 0 / q.leadingCoeff) =
    LinearMap.ker
      (HSub.hSub (β := End K V) (q.leadingCoeff • f)
        ((algebraMap K (End K V) : (a : K) → End K V) (-q.coeff 0) : End K V))

Tactic:
apply eigenspace_div

Premises used: Module.End.eigenspace_div
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
hb : ¬Eq (α := WithBot ℕ) 1 ⊥
⊢ q.leadingCoeff ≠ 0

Tactic:
rw [Ne, leadingCoeff_eq_zero_iff_deg_eq_bot, hq]

Premises used: Ne, Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ ¬Eq (α := WithBot ℕ) 1 ⊥

Tactic:
WithBot.one_ne_bot

Premises used: WithBot.one_ne_bot
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ ¬Eq (α := WithBot ℕ) 1 ⊥

Tactic:
exact WithBot.one_ne_bot

Premises used: WithBot.one_ne_bot
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
rw :
  LinearMap.ker
      (HSub.hSub (β := End K V) (q.leadingCoeff • f)
        ((algebraMap K (End K V) : (a : K) → End K V) (-q.coeff 0) : End K V)) =
    LinearMap.ker
      (eval₂ (algebraMap K (End K V)) f
        (HAdd.hAdd (β := K[X]) (HSMul.hSMul (β := K[X]) q.leadingCoeff X) ((C : (a : K) → K[X]) (q.coeff 0) : K[X])))
⊢ LinearMap.ker
      (HSub.hSub (β := End K V) (q.leadingCoeff • f)
        ((algebraMap K (End K V) : (a : K) → End K V) (-q.coeff 0) : End K V)) =
    LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K)
      ((aeval f : (a : K[X]) → End K V)
        (HAdd.hAdd (β := K[X]) (HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) q.leadingCoeff : K[X]) X)
          ((C : (a : K) → K[X]) (q.coeff 0) : K[X])))

Tactic:
rw [C_mul', aeval_def]

Premises used: Polynomial.C_mul', Polynomial.aeval_def
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker
      (HSub.hSub (β := End K V) (q.leadingCoeff • f)
        ((algebraMap K (End K V) : (a : K) → End K V) (-q.coeff 0) : End K V)) =
    LinearMap.ker
      (eval₂ (algebraMap K (End K V)) f
        (HAdd.hAdd (β := K[X]) (HSMul.hSMul (β := K[X]) q.leadingCoeff X) ((C : (a : K) → K[X]) (q.coeff 0) : K[X])))

Tactic:
simp [algebraMap, Algebra.algebraMap]

Premises used: Algebra.algebraMap
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
rwa :
  Eq.{w + 1} (α := Submodule K V)
    (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) ((aeval f : (a : K[X]) → End K V) q))
    (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) ((aeval f : (a : K[X]) → End K V) q))
rwa₁ : q.degree = 1
rwa₂ :
  Eq.{w + 1} (α := Submodule K V)
    (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) ((aeval f : (a : K[X]) → End K V) q))
    (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) ((aeval f : (a : K[X]) → End K V) q))
rwa₃ rwa₄ rwa₅ : q.degree = 1
⊢ Eq.{w + 1} (α := Submodule K V)
    (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K)
      ((aeval f : (a : K[X]) → End K V)
        (HAdd.hAdd (β := K[X]) (HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) q.leadingCoeff : K[X]) X)
          ((C : (a : K) → K[X]) (q.coeff 0) : K[X]))))
    (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) ((aeval f : (a : K[X]) → End K V) q))

Tactic:
rwa [← eq_X_add_C_of_degree_eq_one]

Premises used: Polynomial.eq_X_add_C_of_degree_eq_one
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
⊢ Set.Finite f.HasEigenvalue

Tactic:
f.finite_hasEigenvalue

Premises used: Module.End.finite_hasEigenvalue
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h : Eq (α := (a : End K V) → Set K) (spectrum K) HasEigenvalue
⊢ (spectrum K f).Finite

Tactic:
convert! f.finite_hasEigenvalue

Premises used: Module.End.finite_hasEigenvalue
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
h : ∀ (f : End K V) (x : K), x ∈ spectrum K f ↔ x ∈ f.HasEigenvalue
⊢ Eq (α := (a : End K V) → Set K) (spectrum K) HasEigenvalue

Tactic:
ext f x
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f_1 f : End K V
x : K
⊢ x ∈ spectrum K f ↔ x ∈ f.HasEigenvalue

Tactic:
Module.End.hasEigenvalue_iff_mem_spectrum.symm

Premises used: Set.Mem, Module.End.HasUnifEigenvalue, Module.End.hasEigenvalue_iff_mem_spectrum, Not, Iff.symm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f_1 f : End K V
x : K
⊢ x ∈ spectrum K f ↔ x ∈ f.HasEigenvalue

Tactic:
exact Module.End.hasEigenvalue_iff_mem_spectrum.symm

Premises used: Module.End.hasEigenvalue_iff_mem_spectrum, Iff.symm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
n : Type u_1
R : Type u_2
inst : Field R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
rw :
  (spectrum R (A := (n → R) →ₗ[R] n → R)
      ((toLinAlgEquiv (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A : (n → R) →ₗ[R] n → R)).Finite
⊢ (spectrum R A).Finite

Tactic:
rw [← AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv <| Pi.basisFun R n) A]

Premises used: AlgEquiv.spectrum_eq, Matrix.toLinAlgEquiv, Pi.basisFun
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
n : Type u_1
R : Type u_2
inst : Field R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
⊢ (spectrum R (A := (n → R) →ₗ[R] n → R)
      ((toLinAlgEquiv (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A : (n → R) →ₗ[R] n → R)).Finite

Tactic:
Module.End.finite_spectrum _

Premises used: Module.End.finite_spectrum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
n : Type u_1
R : Type u_2
inst : Field R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
⊢ (spectrum R (A := (n → R) →ₗ[R] n → R)
      ((toLinAlgEquiv (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A : (n → R) →ₗ[R] n → R)).Finite

Tactic:
exact Module.End.finite_spectrum _

Premises used: Module.End.finite_spectrum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
n : Type u_1
R : Type u_2
inst : Field R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
⊢ Finite.{u_2 + 1} (↑(spectrum R A) : Type u_2)

Tactic:
Set.finite_coe_iff.mpr (Matrix.finite_spectrum A)

Premises used: Iff.mpr, Matrix.finite_spectrum, Set.finite_coe_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
χ : ι → R
m : M
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) m ↔
    ∀ (j : ι), ∃ (k : ℕ), Eq (α := M) (((f j - HSMul.hSMul (β := End R M) (χ j) 1) ^ k : (a : M) → M) m : M) (0 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo (⇑(f i) : (a : M) → M) (↑p : Set M) (↑p : Set M)
inl :
  IsEmpty ι →
    p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
      Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
inr :
  Nonempty ι →
    p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
      Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
⊢ p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo (⇑(f i) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h : IsEmpty ι
⊢ p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
simp [iInf_of_isEmpty]

Premises used: iInf_of_isEmpty
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo (⇑(f i) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h : Nonempty ι
inr :
  ⨅ (x : ι), p ⊓ (f x).maxGenEigenspace (μ x) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
inr₁ :
  ⨅ (x : ι),
      Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) ⋯) (μ x) : (a : ℕ∞) → Submodule R ↥p) ⊤) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
⊢ p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
simp_rw [inf_iInf, p.inf_genEigenspace _ (hfp _), Submodule.map_iInf _ p.injective_subtype]

Premises used: Submodule.inf_genEigenspace, Submodule.map_iInf, Submodule.injective_subtype, inf_iInf
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨i⟩