[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic (minpoly A x)
[PROOFSTEP]
delta minpoly
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic
    (if hx : IsIntegral A x then
      WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
    else 0)
[PROOFSTEP]
rw [dif_pos hx]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic
    (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx)
[PROOFSTEP]
exact (degree_lt_wf.min_mem _ hx).1
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x✝ : B
f : B →ₐ[A] B'
hf : Injective ↑f
x : B
⊢ minpoly A (↑f x) = minpoly A x
[PROOFSTEP]
refine' dif_ctx_congr (isIntegral_algHom_iff _ hf) (fun _ => _) fun _ => rfl
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x✝¹ : B
f : B →ₐ[A] B'
hf : Injective ↑f
x : B
x✝ : IsIntegral A x
⊢ WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A ((fun x => B') x)) (↑f x) x_1 = 0) (_ : IsIntegral A (↑f x)) =
    WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) x✝
[PROOFSTEP]
simp_rw [← Polynomial.aeval_def, aeval_algHom, AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
⊢ ↑(Polynomial.aeval x) (minpoly A x) = 0
[PROOFSTEP]
delta minpoly
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
⊢ ↑(Polynomial.aeval x)
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) =
    0
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) =
    0
[PROOFSTEP]
rw [dif_pos hx]
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) =
    0
[PROOFSTEP]
exact (degree_lt_wf.min_mem _ hx).2
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ¬IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) =
    0
[PROOFSTEP]
rw [dif_neg hx]
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ¬IsIntegral A x
⊢ ↑(Polynomial.aeval x) 0 = 0
[PROOFSTEP]
exact aeval_zero _
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
⊢ minpoly A x ≠ 1
[PROOFSTEP]
intro h
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ False
[PROOFSTEP]
refine' (one_ne_zero : (1 : B) ≠ 0) _
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ 1 = 0
[PROOFSTEP]
simpa using congr_arg (Polynomial.aeval x) h
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
⊢ map f (minpoly A x) ≠ 1
[PROOFSTEP]
by_cases hx : IsIntegral A x
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : IsIntegral A x
⊢ map f (minpoly A x) ≠ 1
[PROOFSTEP]
exact mt ((monic hx).eq_one_of_map_eq_one f) (ne_one A x)
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ map f (minpoly A x) ≠ 1
[PROOFSTEP]
rw [eq_zero hx, Polynomial.map_zero]
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ 0 ≠ 1
[PROOFSTEP]
exact zero_ne_one
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
⊢ ¬IsUnit (minpoly A x)
[PROOFSTEP]
haveI : Nontrivial A := (algebraMap A B).domain_nontrivial
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
this : Nontrivial A
⊢ ¬IsUnit (minpoly A x)
[PROOFSTEP]
by_cases hx : IsIntegral A x
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : IsIntegral A x
⊢ ¬IsUnit (minpoly A x)
[PROOFSTEP]
exact mt (monic hx).eq_one_of_isUnit (ne_one A x)
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit (minpoly A x)
[PROOFSTEP]
rw [eq_zero hx]
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit 0
[PROOFSTEP]
exact not_isUnit_zero
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
⊢ x ∈ RingHom.range (algebraMap A B)
[PROOFSTEP]
have h : IsIntegral A x := by
  by_contra h
  rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx 
  exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
⊢ IsIntegral A x
[PROOFSTEP]
by_contra h
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : ¬IsIntegral A x
⊢ False
[PROOFSTEP]
rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx 
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ⊥ = ↑1
h : ¬IsIntegral A x
⊢ False
[PROOFSTEP]
exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
⊢ x ∈ RingHom.range (algebraMap A B)
[PROOFSTEP]
have key := minpoly.aeval A x
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : ↑(Polynomial.aeval x) (minpoly A x) = 0
⊢ x ∈ RingHom.range (algebraMap A B)
[PROOFSTEP]
rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leadingCoeff, C_1, one_mul, aeval_add, aeval_C, aeval_X, ←
  eq_neg_iff_add_eq_zero, ← RingHom.map_neg] at key 
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : x = ↑(algebraMap A B) (-coeff (minpoly A x) 0)
⊢ x ∈ RingHom.range (algebraMap A B)
[PROOFSTEP]
exact ⟨-(minpoly A x).coeff 0, key.symm⟩
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
⊢ degree (minpoly A x) ≤ degree p
[PROOFSTEP]
delta minpoly
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
⊢ degree
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) ≤
    degree p
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hx : IsIntegral A x
⊢ degree
      (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) ≤
    degree p
[PROOFSTEP]
exact le_of_not_lt (degree_lt_wf.not_lt_min _ hx ⟨pmonic, hp⟩)
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hx : ¬IsIntegral A x
⊢ degree 0 ≤ degree p
[PROOFSTEP]
simp only [degree_zero, bot_le]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
⊢ p = minpoly A x
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
⊢ p = minpoly A x
[PROOFSTEP]
have hx : IsIntegral A x := ⟨p, hm, hp⟩
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
⊢ p = minpoly A x
[PROOFSTEP]
obtain h | h := hl _ ((minpoly A x).degree_modByMonic_lt hm)
[GOAL]
case inl
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : ↑(Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x
[PROOFSTEP]
swap
[GOAL]
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : ↑(Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x
[PROOFSTEP]
exact (h <| (aeval_modByMonic_eq_self_of_root hm hp).trans <| aeval A x).elim
[GOAL]
case inl
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x
[PROOFSTEP]
obtain ⟨r, hr⟩ := (dvd_iff_modByMonic_eq_zero hm).1 h
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = minpoly A x
[PROOFSTEP]
rw [hr]
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = p * r
[PROOFSTEP]
have hlead := congr_arg leadingCoeff hr
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : leadingCoeff (minpoly A x) = leadingCoeff (p * r)
⊢ p = p * r
[PROOFSTEP]
rw [mul_comm, leadingCoeff_mul_monic hm, (monic hx).leadingCoeff] at hlead 
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ p = p * r
[PROOFSTEP]
have : natDegree r ≤ 0 :=
  by
  have hr0 : r ≠ 0 := by
    rintro rfl
    exact ne_zero hx (mul_zero p ▸ hr)
  apply_fun natDegree at hr 
  rw [hm.natDegree_mul' hr0] at hr 
  apply Nat.le_of_add_le_add_left
  rw [add_zero]
  exact hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ natDegree r ≤ 0
[PROOFSTEP]
have hr0 : r ≠ 0 := by
  rintro rfl
  exact ne_zero hx (mul_zero p ▸ hr)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ r ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
hr : minpoly A x = p * 0
hlead : 1 = leadingCoeff 0
⊢ False
[PROOFSTEP]
exact ne_zero hx (mul_zero p ▸ hr)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
⊢ natDegree r ≤ 0
[PROOFSTEP]
apply_fun natDegree at hr 
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree (p * r)
⊢ natDegree r ≤ 0
[PROOFSTEP]
rw [hm.natDegree_mul' hr0] at hr 
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ natDegree r ≤ 0
[PROOFSTEP]
apply Nat.le_of_add_le_add_left
[GOAL]
case h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ?a + natDegree r ≤ ?a + 0
case a
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ℕ
[PROOFSTEP]
rw [add_zero]
[GOAL]
case h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ?h + natDegree r ≤ ?h
case h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ℕ
[PROOFSTEP]
exact hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
this : natDegree r ≤ 0
⊢ p = p * r
[PROOFSTEP]
rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1, mul_one]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
⊢ minpoly A x = 1
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
⊢ minpoly A x = 1
[PROOFSTEP]
have := minpoly.min A x monic_one (Subsingleton.elim _ _)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ degree 1
⊢ minpoly A x = 1
[PROOFSTEP]
rw [degree_one] at this 
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
⊢ minpoly A x = 1
[PROOFSTEP]
cases' le_or_lt (minpoly A x).degree 0 with h h
[GOAL]
case inl
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : degree (minpoly A x) ≤ 0
⊢ minpoly A x = 1
[PROOFSTEP]
rwa [(monic ⟨1, monic_one, by simp⟩ : (minpoly A x).Monic).degree_le_zero_iff_eq_one] at h 
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : degree (minpoly A x) ≤ 0
⊢ eval₂ (algebraMap A B) x 1 = 0
[PROOFSTEP]
simp
[GOAL]
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : 0 < degree (minpoly A x)
⊢ minpoly A x = 1
[PROOFSTEP]
exact (this.not_lt h).elim
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ 0 < natDegree (minpoly A x)
[PROOFSTEP]
rw [pos_iff_ne_zero]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ natDegree (minpoly A x) ≠ 0
[PROOFSTEP]
intro ndeg_eq_zero
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ False
[PROOFSTEP]
have eq_one : minpoly A x = 1 := by
  rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
  convert C_1 (R := A)
  simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ minpoly A x = 1
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ ↑C (coeff (minpoly A x) 0) = 1
[PROOFSTEP]
convert C_1 (R := A)
[GOAL]
case h.e'_2.h.e'_6
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ coeff (minpoly A x) 0 = 1
[PROOFSTEP]
simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
eq_one : minpoly A x = 1
⊢ False
[PROOFSTEP]
simpa only [eq_one, AlgHom.map_one, one_ne_zero] using aeval A x
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
⊢ minpoly A (↑(algebraMap A B) a) = X - ↑C a
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ minpoly A (↑(algebraMap A B) a) = X - ↑C a
[PROOFSTEP]
refine' (unique' A _ (monic_X_sub_C a) _ _).symm
[GOAL]
case refine'_1
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) (X - ↑C a) = 0
[PROOFSTEP]
rw [map_sub, aeval_C, aeval_X, sub_self]
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ∀ (q : A[X]), degree q < degree (X - ↑C a) → q = 0 ∨ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
[PROOFSTEP]
simp_rw [or_iff_not_imp_left]
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ∀ (q : A[X]), degree q < degree (X - ↑C a) → ¬q = 0 → ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
[PROOFSTEP]
intro q hl h0
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : degree q < degree (X - ↑C a)
h0 : ¬q = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
[PROOFSTEP]
rw [← natDegree_lt_natDegree_iff h0, natDegree_X_sub_C, Nat.lt_one_iff] at hl 
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : natDegree q = 0
h0 : ¬q = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero hl] at h0 ⊢
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : natDegree q = 0
h0 : ¬↑C (coeff q 0) = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) (↑C (coeff q 0)) ≠ 0
[PROOFSTEP]
rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
hdvd : DvdNotUnit a (minpoly A x)
⊢ ↑(Polynomial.aeval x) a ≠ 0
[PROOFSTEP]
refine' fun ha => (min A x hamonic ha).not_lt (degree_lt_degree _)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
hdvd : DvdNotUnit a (minpoly A x)
ha : ↑(Polynomial.aeval x) a = 0
⊢ natDegree a < natDegree (minpoly A x)
[PROOFSTEP]
obtain ⟨_, c, hu, he⟩ := hdvd
[GOAL]
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ natDegree a < natDegree (minpoly A x)
[PROOFSTEP]
have hcm := hamonic.of_mul_monic_left (he.subst <| monic hx)
[GOAL]
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ natDegree a < natDegree (minpoly A x)
[PROOFSTEP]
rw [he, hamonic.natDegree_mul hcm]
  -- TODO: port Nat.lt_add_of_zero_lt_left from lean3 core
[GOAL]
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ natDegree a < natDegree a + natDegree c
[PROOFSTEP]
apply lt_add_of_pos_right
[GOAL]
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ 0 < natDegree c
[PROOFSTEP]
refine (lt_of_not_le fun h => hu ?_)
[GOAL]
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
h : natDegree c ≤ 0
⊢ IsUnit c
[PROOFSTEP]
rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff, C_1]
[GOAL]
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
h : natDegree c ≤ 0
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
⊢ Irreducible (minpoly A x)
[PROOFSTEP]
refine' (irreducible_of_monic (monic hx) <| ne_one A x).2 fun f g hf hg he => _
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
⊢ f = 1 ∨ g = 1
[PROOFSTEP]
rw [← hf.isUnit_iff, ← hg.isUnit_iff]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
⊢ IsUnit f ∨ IsUnit g
[PROOFSTEP]
by_contra' h
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
⊢ False
[PROOFSTEP]
have heval := congr_arg (Polynomial.aeval x) he
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) (f * g) = ↑(Polynomial.aeval x) (minpoly A x)
⊢ False
[PROOFSTEP]
rw [aeval A x, aeval_mul, mul_eq_zero] at heval 
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) f = 0 ∨ ↑(Polynomial.aeval x) g = 0
⊢ False
[PROOFSTEP]
cases' heval with heval heval
[GOAL]
case inl
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) f = 0
⊢ False
[PROOFSTEP]
exact aeval_ne_zero_of_dvdNotUnit_minpoly hx hf ⟨hf.ne_zero, g, h.2, he.symm⟩ heval
[GOAL]
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) g = 0
⊢ False
[PROOFSTEP]
refine' aeval_ne_zero_of_dvdNotUnit_minpoly hx hg ⟨hg.ne_zero, f, h.1, _⟩ heval
[GOAL]
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) g = 0
⊢ minpoly A x = g * f
[PROOFSTEP]
rw [mul_comm, he]
