case refine'_1
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) (Polynomial.comp (minpoly A x) (X - ↑C a)) = 0

case refine'_2
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ minpoly A (x + ↑(algebraMap A B) a) = Polynomial.comp (minpoly A x) (X - ↑C a)
refine' (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) _ fun q qmo hq => _).symm
no goals
case refine'_1
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) (Polynomial.comp (minpoly A x) (X - ↑C a)) = 0
simp [aeval_comp]
case refine'_2
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
case refine'_2
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq
case refine'_2
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
H : degree (minpoly A x) ≤ degree (Polynomial.comp q (X + ↑C a))
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
case refine'_2
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
have H := minpoly.min A x (qmo.comp_X_add_C _) this
case refine'_2
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
H : degree (minpoly A x) ≤ degree (Polynomial.comp q (X + ↑C a))
⊢ ↑(natDegree (minpoly A x)) ≤ ↑(natDegree q)
case refine'_2
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
H : degree (minpoly A x) ≤ degree (Polynomial.comp q (X + ↑C a))
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
rw [degree_eq_natDegree qmo.ne_zero,
  degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
  natDegree_X_sub_C, mul_one]
no goals
case refine'_2
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
H : degree (minpoly A x) ≤ degree (Polynomial.comp q (X + ↑C a))
⊢ ↑(natDegree (minpoly A x)) ≤ ↑(natDegree q)
rwa [degree_eq_natDegree (minpoly.ne_zero hx),
  degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
  natDegree_X_add_C, mul_one] at H
no goals
A : Type u_2
B✝ : Type ?u.270535
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_1
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
⊢ ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
simpa [aeval_comp] using hq