-- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
theorem hasEigenvalue_of_isRoot (h : (minpoly K f).IsRoot μ) : f.HasEigenvalue μ

Proof state:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
this : (aeval f) p = 0
⊢ False

Tactic:
have h_deg := minpoly.degree_le_of_ne_zero K f p_ne_0 this

Result:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
this : (aeval f) p = 0
h_deg : (minpoly K f).degree ≤ p.degree
⊢ False

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
⊢ (aeval f) (minpoly K f) = 0 → (aeval f) p = 0

Tactic:
simp [hp, ← hu, Algebra.algebraMap_eq_smul_one]

Result:
no goals

Proof state:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
⊢ False

Tactic:
have : (aeval f) p = 0 := by
  have h_aeval := minpoly.aeval K f
  revert h_aeval
  simp [hp, ← hu, Algebra.algebraMap_eq_smul_one]

Result:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
this : (aeval f) p = 0
⊢ False

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
h_aeval : (aeval f) (minpoly K f) = 0
⊢ (aeval f) p = 0

Tactic:
revert h_aeval

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
⊢ (aeval f) (minpoly K f) = 0 → (aeval f) p = 0

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
⊢ (aeval f) p = 0

Tactic:
have h_aeval := minpoly.aeval K f

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
h_aeval : (aeval f) (minpoly K f) = 0
⊢ (aeval f) p = 0

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
⊢ p ≠ 0

Tactic:
intro con

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con✝ : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
con : p = 0
⊢ False

Proof state:
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
⊢ False

Tactic:
obtain ⟨u, hu⟩ := (LinearMap.isUnit_iff_ker_eq_bot _).2 con

Result:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
⊢ False

Proof state:
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
⊢ LinearMap.ker (f - μ • 1) ≠ ⊥

Tactic:
intro con

Result:
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
⊢ False

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con✝ : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
con : p = 0
⊢ minpoly K f = 0

Tactic:
rw [hp, con, mul_zero]

Result:
no goals

Proof state:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
⊢ False

Tactic:
have p_ne_0 : p ≠ 0 := by
  intro con
  apply minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := K) f)
  rw [hp, con, mul_zero]

Result:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
⊢ False

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con✝ : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
con : p = 0
⊢ False

Tactic:
apply minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := K) f)

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con✝ : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
con : p = 0
⊢ minpoly K f = 0

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
⊢ f.HasEigenvalue μ

Tactic:
obtain ⟨p, hp⟩ := dvd_iff_isRoot.2 h

Result:
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
⊢ f.HasEigenvalue μ