-- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
theorem aeval_apply_of_hasEigenvector {f : End K V} {p : K[X]} {μ : K} {x : V}
    (h : f.HasEigenvector μ x) : aeval f p x = p.eval μ • x

Proof state:
case refine_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
⊢ ∀ (n : ℕ) (a : K),
    ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x →
      ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x

Tactic:
intro n a hna

Result:
case refine_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
n : ℕ
a : K
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x

Proof state:
case refine_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
n : ℕ
a : K
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) X) (eval μ (C a * X ^ n) • x) = eval μ (X * (C a * X ^ n)) • x

Tactic:
simp only [mem_eigenspace_iff.1 h.1, smul_smul, aeval_X, eval_mul, eval_C, eval_pow, eval_X,
  LinearMap.map_smulₛₗ, RingHom.id_apply, mul_comm]

Result:
no goals

Proof state:
case refine_2
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
⊢ ∀ (p q : K[X]),
    ((aeval f) p) x = eval μ p • x → ((aeval f) q) x = eval μ q • x → ((aeval f) (p + q)) x = eval μ (p + q) • x

Tactic:
intro p q hp hq

Result:
case refine_2
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p✝ : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
p q : K[X]
hp : ((aeval f) p) x = eval μ p • x
hq : ((aeval f) q) x = eval μ q • x
⊢ ((aeval f) (p + q)) x = eval μ (p + q) • x

Proof state:
case refine_1
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
⊢ ∀ (a : K), ((aeval f) (C a)) x = eval μ (C a) • x

Tactic:
intro a

Result:
case refine_1
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
a : K
⊢ ((aeval f) (C a)) x = eval μ (C a) • x

Proof state:
case refine_1
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
a : K
⊢ ((aeval f) (C a)) x = eval μ (C a) • x

Tactic:
simp [Module.algebraMap_end_apply]

Result:
no goals

Proof state:
case refine_2
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p✝ : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
p q : K[X]
hp : ((aeval f) p) x = eval μ p • x
hq : ((aeval f) q) x = eval μ q • x
⊢ ((aeval f) (p + q)) x = eval μ (p + q) • x

Tactic:
simp [hp, hq, add_smul]

Result:
no goals

Proof state:
case refine_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
n : ℕ
a : K
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x

Tactic:
rw [mul_comm, pow_succ', mul_assoc, map_mul, LinearMap.mul_apply, mul_comm, hna]

Result:
case refine_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
n : ℕ
a : K
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) X) (eval μ (C a * X ^ n) • x) = eval μ (X * (C a * X ^ n)) • x

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
⊢ ((aeval f) p) x = eval μ p • x

Tactic:
refine p.induction_on ?_ ?_ ?_

Result:
case refine_1
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
⊢ ∀ (a : K), ((aeval f) (C a)) x = eval μ (C a) • x

case refine_2
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
⊢ ∀ (p q : K[X]),
    ((aeval f) p) x = eval μ p • x → ((aeval f) q) x = eval μ q • x → ((aeval f) (p + q)) x = eval μ (p + q) • x

case refine_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : f.HasEigenvector μ x
⊢ ∀ (n : ℕ) (a : K),
    ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x →
      ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x