-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem add_algebraMap {B : Type*} [CommRing B] [Algebra A B] (x : B)
    (a : A) : minpoly A (x + algebraMap A B a) = (minpoly A x).comp (X - C a)

Proof state:
case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
⊢ ¬IsIntegral A (x + (algebraMap A B) a)

Tactic:
refine fun h ↦ hx ?_

Result:
case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
h : IsIntegral A (x + (algebraMap A B) a)
⊢ IsIntegral A x

Proof state:
case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
h : IsIntegral A (x + (algebraMap A B) a)
⊢ IsIntegral A x

Tactic:
simpa only [add_sub_cancel_right] using IsIntegral.sub h (isIntegral_algebraMap (x := a))

Result:
no goals

Proof state:
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
⊢ (Polynomial.aeval x) (q.comp (X + C a)) = 0

Tactic:
simpa [aeval_comp] using hq

Result:
no goals

Proof state:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree

Tactic:
have H := minpoly.min A x (qmo.comp_X_add_C _) this

Result:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : (minpoly A x).degree ≤ (q.comp (X + C a)).degree
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree

Proof state:
case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
⊢ minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)

Tactic:
rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]

Result:
case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
⊢ ¬IsIntegral A (x + (algebraMap A B) a)

Proof state:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree

Tactic:
have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq

Result:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree

Proof state:
case pos.refine_1
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
⊢ (Polynomial.aeval (x + (algebraMap A B) a)) ((minpoly A x).comp (X - C a)) = 0

Tactic:
simp [aeval_comp]

Result:
no goals

Proof state:
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
⊢ minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)

Tactic:
by_cases hx : IsIntegral A x

Result:
case pos
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
⊢ minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)

case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
⊢ minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)

Proof state:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : (minpoly A x).degree ≤ (q.comp (X + C a)).degree
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree

Tactic:
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]

Result:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : (minpoly A x).degree ≤ (q.comp (X + C a)).degree
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree

Proof state:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : (minpoly A x).degree ≤ (q.comp (X + C a)).degree
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree

Tactic:
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

Result:
no goals

Proof state:
case pos
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
⊢ minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)

Tactic:
refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun q qmo hq => ?_).symm

Result:
case pos.refine_1
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
⊢ (Polynomial.aeval (x + (algebraMap A B) a)) ((minpoly A x).comp (X - C a)) = 0

case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree