-- Mathlib/RingTheory/AdjoinRoot.lean
theorem minpoly_root (hf : f ≠ 0) : minpoly K (root f) = f * C f.leadingCoeff⁻¹

Proof state:
case h₁.a
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
x✝ : K
⊢ (((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q)).comp C) x✝ = ((mk f).comp C) x✝

Tactic:
simp only [RingHom.comp_apply, mk_C, lift_of]

Result:
case h₁.a
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
x✝ : K
⊢ (algebraMap K (AdjoinRoot f)) x✝ = (of f) x✝

Proof state:
case refine_2.h1
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
this : (mk f) q = 0
⊢ f ∣ q

Tactic:
exact mk_eq_zero.1 this

Result:
no goals

Proof state:
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ minpoly K (root f) = f * C f.leadingCoeff⁻¹

Tactic:
refine (minpoly.unique K _ f'_monic ?_ ?_).symm

Result:
case refine_1
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ (aeval (root f)) (f * C f.leadingCoeff⁻¹) = 0

case refine_2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ ∀ (q : K[X]), q.Monic → (aeval (root f)) q = 0 → (f * C f.leadingCoeff⁻¹).degree ≤ q.degree

Proof state:
case h₁.a
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
x✝ : K
⊢ (algebraMap K (AdjoinRoot f)) x✝ = (of f) x✝

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2.h1
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ f ∣ q

Tactic:
have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, RingHom.map_zero]

Result:
case refine_2.h1
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
this : (mk f) q = 0
⊢ f ∣ q

Proof state:
case refine_2.h2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ q ≠ 0

Tactic:
exact q_monic.ne_zero

Result:
no goals

Proof state:
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ minpoly K (root f) = f * C f.leadingCoeff⁻¹

Tactic:
have f'_monic : Monic _ := monic_mul_leadingCoeff_inv hf

Result:
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ minpoly K (root f) = f * C f.leadingCoeff⁻¹

Proof state:
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
⊢ (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f

Tactic:
ext

Result:
case h₁.a
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
x✝ : K
⊢ (((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q)).comp C) x✝ = ((mk f).comp C) x✝

case h₂
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
⊢ ((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q)) X = (mk f) X

Proof state:
case refine_2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ f.natDegree ≤ q.natDegree

Tactic:
apply natDegree_le_of_dvd

Result:
case refine_2.h1
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ f ∣ q

case refine_2.h2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ q ≠ 0

Proof state:
case refine_2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ C f.leadingCoeff⁻¹ ≠ 0

Tactic:
rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]

Result:
no goals

Proof state:
case refine_2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ (f * C f.leadingCoeff⁻¹).degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree f'_monic.ne_zero, degree_eq_natDegree q_monic.ne_zero,
  Nat.cast_le, natDegree_mul hf, natDegree_C, add_zero]

Result:
case refine_2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ f.natDegree ≤ q.natDegree

case refine_2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ C f.leadingCoeff⁻¹ ≠ 0

Proof state:
case h₂
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
⊢ ((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q)) X = (mk f) X

Tactic:
simp only [RingHom.comp_apply, mk_X, lift_root]

Result:
no goals

Proof state:
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ (mk f) q = 0

Tactic:
rw [← commutes, RingHom.comp_apply, mk_self, RingHom.map_zero]

Result:
no goals

Proof state:
case refine_1
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ (aeval (root f)) (f * C f.leadingCoeff⁻¹) = 0

Tactic:
rw [_root_.map_mul, aeval_eq, mk_self, zero_mul]

Result:
no goals

Proof state:
case refine_2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ ∀ (q : K[X]), q.Monic → (aeval (root f)) q = 0 → (f * C f.leadingCoeff⁻¹).degree ≤ q.degree

Tactic:
intro q q_monic q_aeval

Result:
case refine_2
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
⊢ (f * C f.leadingCoeff⁻¹).degree ≤ q.degree