[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
f : R[X]
x✝ : X ∣ f
g : R[X]
hfg : f = X * g
⊢ coeff f 0 = 0
[PROOFSTEP]
rw [hfg, mul_comm, coeff_mul_X_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
f : R[X]
hf : coeff f 0 = 0
⊢ f = X * divX f
[PROOFSTEP]
rw [mul_comm, ← add_zero (f.divX * X), ← C_0, ← hf, divX_mul_X_add]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n : ℕ
x✝ : X ^ n ∣ f
d : ℕ
hd : d < n
g : R[X]
hgf : f = X ^ n * g
⊢ coeff f d = 0
[PROOFSTEP]
simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_lt hd, IsEmpty.forall_iff]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n : ℕ
hd : ∀ (d : ℕ), d < n → coeff f d = 0
⊢ X ^ n ∣ f
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n : ℕ
hd✝ : ∀ (d : ℕ), d < n → coeff f d = 0
hd : ∀ (d : ℕ), d < Nat.zero → coeff f d = 0
⊢ X ^ Nat.zero ∣ f
[PROOFSTEP]
simp [pow_zero, one_dvd]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
⊢ X ^ Nat.succ n ∣ f
[PROOFSTEP]
obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
[GOAL]
case succ.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
⊢ X ^ Nat.succ n ∣ f
[PROOFSTEP]
have := coeff_X_pow_mul g n 0
[GOAL]
case succ.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : coeff (X ^ n * g) (0 + n) = coeff g 0
⊢ X ^ Nat.succ n ∣ f
[PROOFSTEP]
rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this 
[GOAL]
case succ.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = coeff g 0
⊢ X ^ Nat.succ n ∣ f
[PROOFSTEP]
obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
[GOAL]
case succ.intro.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = coeff g 0
k : R[X]
hgk : g = X * k
⊢ X ^ Nat.succ n ∣ f
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
hd✝ : ∀ (d : ℕ), d < n✝ → coeff f d = 0
n : ℕ
hn : (∀ (d : ℕ), d < n → coeff f d = 0) → X ^ n ∣ f
hd : ∀ (d : ℕ), d < Nat.succ n → coeff f d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = coeff g 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ Nat.succ n * k
[PROOFSTEP]
rwa [pow_succ, mul_comm X _, mul_assoc, ← hgk]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
⊢ False
[PROOFSTEP]
have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp 
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p = 0
⊢ False
[PROOFSTEP]
simp [hp0] at hp 
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
⊢ False
[PROOFSTEP]
have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr 
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r = 0
⊢ False
[PROOFSTEP]
subst hr0
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
hp0 : p ≠ 0
hr : q = p ^ (natDegree q + 1) * 0
⊢ False
[PROOFSTEP]
simp [hq] at hr 
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
⊢ False
[PROOFSTEP]
have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1 := by simp [show _ = _ from hmp]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
⊢ leadingCoeff p ^ (natDegree q + 1) = 1
[PROOFSTEP]
simp [show _ = _ from hmp]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
⊢ False
[PROOFSTEP]
have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0
⊢ False
[PROOFSTEP]
have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
  simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_pow, one_mul, Ne.def, hr0]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0
⊢ leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0
[PROOFSTEP]
simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_pow, one_mul, Ne.def, hr0]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0
hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0
⊢ False
[PROOFSTEP]
have hnp : 0 < natDegree p := by
  rw [← WithBot.coe_lt_coe, ← Nat.cast_withBot, ← Nat.cast_withBot, ← degree_eq_natDegree hp0]; exact hp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0
hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0
⊢ 0 < natDegree p
[PROOFSTEP]
rw [← WithBot.coe_lt_coe, ← Nat.cast_withBot, ← Nat.cast_withBot, ← degree_eq_natDegree hp0]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0
hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0
⊢ ↑0 < degree p
[PROOFSTEP]
exact hp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0
hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0
hnp : 0 < natDegree p
⊢ False
[PROOFSTEP]
have := congr_arg natDegree hr
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0
hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0
hnp : 0 < natDegree p
this : natDegree q = natDegree (p ^ (natDegree q + 1) * r)
⊢ False
[PROOFSTEP]
rw [natDegree_mul' hpnr0, natDegree_pow' hpn0', add_mul, add_assoc] at this 
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0
hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0
hnp : 0 < natDegree p
this : natDegree q = natDegree q * natDegree p + (1 * natDegree p + natDegree r)
⊢ False
[PROOFSTEP]
exact
  ne_of_lt
    (lt_add_of_le_of_pos (le_mul_of_one_le_right (Nat.zero_le _) hnp)
      (add_pos_of_pos_of_nonneg (by rwa [one_mul]) (Nat.zero_le _)))
    this
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
hp : 0 < degree p
hmp : Monic p
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (natDegree q + 1) ∣ q
r : R[X]
hr : q = p ^ (natDegree q + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1
hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0
hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0
hnp : 0 < natDegree p
this : natDegree q = natDegree q * natDegree p + (1 * natDegree p + natDegree r)
⊢ 0 < 1 * natDegree p
[PROOFSTEP]
rwa [one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q ≤ degree p ∧ p ≠ 0
hq : Monic q
hp : leadingCoeff p ≠ 0
hq0 : q ≠ 0
⊢ ↑(natDegree q) ≤ ↑(natDegree p)
[PROOFSTEP]
rw [← Nat.cast_withBot, ← Nat.cast_withBot, ← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q ≤ degree p ∧ p ≠ 0
hq : Monic q
hp : leadingCoeff p ≠ 0
hq0 : q ≠ 0
⊢ degree q ≤ degree p
[PROOFSTEP]
exact h.1
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q ≤ degree p ∧ p ≠ 0
hq : Monic q
hp : leadingCoeff p ≠ 0
hq0 : q ≠ 0
hlt : natDegree q ≤ natDegree p
⊢ degree p = degree (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q)
[PROOFSTEP]
rw [hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2, degree_eq_natDegree hq0, ← Nat.cast_add,
  tsub_add_cancel_of_le hlt]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q ≤ degree p ∧ p ≠ 0
hq : Monic q
hp : leadingCoeff p ≠ 0
hq0 : q ≠ 0
hlt : natDegree q ≤ natDegree p
⊢ leadingCoeff p = leadingCoeff (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q)
[PROOFSTEP]
rw [leadingCoeff_mul_monic hq, leadingCoeff_mul_X_pow, leadingCoeff_C]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
⊢ degree (p %ₘ q) < degree q
[PROOFSTEP]
have _wf := div_wf_lemma ⟨h.1, h.2⟩ hq
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
⊢ degree (p %ₘ q) < degree q
[PROOFSTEP]
have : degree ((p - C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q) < degree q :=
  degree_modByMonic_lt (p - C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this : degree ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q) < degree q
⊢ degree (p %ₘ q) < degree q
[PROOFSTEP]
unfold modByMonic at this ⊢
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this :
  degree
      (if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd
      else p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) <
    degree q
⊢ degree (if hq : Monic q then (divModByMonicAux p hq).snd else p) < degree q
[PROOFSTEP]
unfold divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this :
  degree
      (if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd
      else p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) <
    degree q
⊢ degree
      (if h : Monic q then
        (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
            let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
            let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
            let dm := divModByMonicAux (p - z * q) (_ : Monic q);
            (z + dm.fst, dm.snd)
          else (0, p)).snd
      else p) <
    degree q
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this :
  degree
      (if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd
      else p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) <
    degree q
⊢ degree
      (if h : Monic q then
        (if degree q ≤ degree p ∧ ¬p = 0 then
            (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
          else (0, p)).snd
      else p) <
    degree q
[PROOFSTEP]
rw [dif_pos hq] at this ⊢
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this : degree (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd < degree q
⊢ degree
      (if degree q ≤ degree p ∧ ¬p = 0 then
          (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
        else (0, p)).snd <
    degree q
[PROOFSTEP]
rw [if_pos h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
this : degree (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd < degree q
⊢ degree
      (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
          (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd).snd <
    degree q
[PROOFSTEP]
exact this
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p → degree (p %ₘ q) < degree q
[PROOFSTEP]
unfold modByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p →
    degree
        (if h : Monic q then
          (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
              let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
              let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
              let dm := divModByMonicAux (p - z * q) (_ : Monic q);
              (z + dm.fst, dm.snd)
            else (0, p)).snd
        else p) <
      degree q
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p →
    degree
        (if h : Monic q then
          (if degree q ≤ degree p ∧ ¬p = 0 then
              (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
            else (0, p)).snd
        else p) <
      degree q
[PROOFSTEP]
rw [dif_pos hq, if_neg h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬degree q ≤ degree p → degree (0, p).snd < degree q
[PROOFSTEP]
exact lt_of_not_ge
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ ¬p ≠ 0 → degree (p %ₘ q) < degree q
[PROOFSTEP]
intro hp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree (p %ₘ q) < degree q
[PROOFSTEP]
unfold modByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree
      (if h : Monic q then
        (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
            let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
            let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
            let dm := divModByMonicAux (p - z * q) (_ : Monic q);
            (z + dm.fst, dm.snd)
          else (0, p)).snd
      else p) <
    degree q
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree
      (if h : Monic q then
        (if degree q ≤ degree p ∧ ¬p = 0 then
            (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
          else (0, p)).snd
      else p) <
    degree q
[PROOFSTEP]
rw [dif_pos hq, if_neg h, Classical.not_not.1 hp]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p✝ q✝ : R[X]
inst✝ : Nontrivial R
p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree (0, 0).snd < degree q
[PROOFSTEP]
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 hq.ne_zero))
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ 0 %ₘ p = 0
[PROOFSTEP]
unfold modByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ (if h : Monic p then
      (if h_1 : degree p ≤ degree 0 ∧ 0 ≠ 0 then
          let z := ↑C (leadingCoeff 0) * X ^ (natDegree 0 - natDegree p);
          let_fun _wf := (_ : degree (0 - ↑C (leadingCoeff 0) * X ^ (natDegree 0 - natDegree p) * p) < degree 0);
          let dm := divModByMonicAux (0 - z * p) (_ : Monic p);
          (z + dm.fst, dm.snd)
        else (0, 0)).snd
    else 0) =
    0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).snd
    else 0) =
    0
[PROOFSTEP]
by_cases hp : Monic p
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
hp : Monic p
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).snd
    else 0) =
    0
[PROOFSTEP]
rw [dif_pos hp, if_neg (mt And.right (not_not_intro rfl))]
[GOAL]
case neg
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
hp : ¬Monic p
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).snd
    else 0) =
    0
[PROOFSTEP]
rw [dif_neg hp]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ 0 /ₘ p = 0
[PROOFSTEP]
unfold divByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ (if h : Monic p then
      (if h_1 : degree p ≤ degree 0 ∧ 0 ≠ 0 then
          let z := ↑C (leadingCoeff 0) * X ^ (natDegree 0 - natDegree p);
          let_fun _wf := (_ : degree (0 - ↑C (leadingCoeff 0) * X ^ (natDegree 0 - natDegree p) * p) < degree 0);
          let dm := divModByMonicAux (0 - z * p) (_ : Monic p);
          (z + dm.fst, dm.snd)
        else (0, 0)).fst
    else 0) =
    0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).fst
    else 0) =
    0
[PROOFSTEP]
by_cases hp : Monic p
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
hp : Monic p
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).fst
    else 0) =
    0
[PROOFSTEP]
rw [dif_pos hp, if_neg (mt And.right (not_not_intro rfl))]
[GOAL]
case neg
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
hp : ¬Monic p
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).fst
    else 0) =
    0
[PROOFSTEP]
rw [dif_neg hp]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : Monic 0
⊢ p %ₘ 0 = p
[PROOFSTEP]
haveI := monic_zero_iff_subsingleton.mp h
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : Monic 0
this : Subsingleton R
⊢ p %ₘ 0 = p
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : ¬Monic 0
⊢ p %ₘ 0 = p
[PROOFSTEP]
unfold modByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ degree p ∧ p ≠ 0 then
          let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree 0);
          let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree 0) * 0) < degree p);
          let dm := divModByMonicAux (p - z * 0) (_ : Monic 0);
          (z + dm.fst, dm.snd)
        else (0, p)).snd
    else p) =
    p
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : Monic 0
⊢ p /ₘ 0 = 0
[PROOFSTEP]
haveI := monic_zero_iff_subsingleton.mp h
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : Monic 0
this : Subsingleton R
⊢ p /ₘ 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : ¬Monic 0
⊢ p /ₘ 0 = 0
[PROOFSTEP]
unfold divByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ degree p ∧ p ≠ 0 then
          let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree 0);
          let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree 0) * 0) < degree p);
          let dm := divModByMonicAux (p - z * 0) (_ : Monic 0);
          (z + dm.fst, dm.snd)
        else (0, p)).fst
    else 0) =
    0
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
⊢ p %ₘ q = p
[PROOFSTEP]
have : ¬degree q ≤ degree p := not_le_of_gt h
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ p %ₘ q = p
[PROOFSTEP]
unfold modByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ (if h : Monic q then
      (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
          let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
          let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
          let dm := divModByMonicAux (p - z * q) (_ : Monic q);
          (z + dm.fst, dm.snd)
        else (0, p)).snd
    else p) =
    p
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ (if h : Monic q then
      (if degree q ≤ degree p ∧ ¬p = 0 then
          (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
        else (0, p)).snd
    else p) =
    p
[PROOFSTEP]
rw [dif_pos hq, if_neg (mt And.left this)]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q✝ p q : R[X]
hq : Monic q
⊢ degree (p %ₘ q) ≤ degree q
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q✝ p q : R[X]
hq : Monic q
✝ : Nontrivial R
⊢ degree (p %ₘ q) ≤ degree q
[PROOFSTEP]
exact (degree_modByMonic_lt _ hq).le
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
⊢ p %ₘ q = p - q * (p /ₘ q)
[PROOFSTEP]
have _wf := div_wf_lemma h hq
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
⊢ p %ₘ q = p - q * (p /ₘ q)
[PROOFSTEP]
have ih := modByMonic_eq_sub_mul_div (p - C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
ih :
  (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q =
    p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q -
      q * ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) /ₘ q)
⊢ p %ₘ q = p - q * (p /ₘ q)
[PROOFSTEP]
unfold modByMonic divByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
ih :
  (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q =
    p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q -
      q * ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) /ₘ q)
⊢ (if h : Monic q then
      (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
          let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
          let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
          let dm := divModByMonicAux (p - z * q) (_ : Monic q);
          (z + dm.fst, dm.snd)
        else (0, p)).snd
    else p) =
    p -
      q *
        if h : Monic q then
          (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
              let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
              let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
              let dm := divModByMonicAux (p - z * q) (_ : Monic q);
              (z + dm.fst, dm.snd)
            else (0, p)).fst
        else 0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
ih :
  (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q =
    p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q -
      q * ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) /ₘ q)
⊢ (if h : Monic q then
      (if degree q ≤ degree p ∧ ¬p = 0 then
          (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
        else (0, p)).snd
    else p) =
    p -
      q *
        if h : Monic q then
          (if degree q ≤ degree p ∧ ¬p = 0 then
              (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
            else (0, p)).fst
        else 0
[PROOFSTEP]
rw [dif_pos hq, if_pos h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
ih :
  (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q =
    p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q -
      q * ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) /ₘ q)
⊢ (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
          (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
        (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd).snd =
    p -
      q *
        if h : Monic q then
          (if degree q ≤ degree p ∧ ¬p = 0 then
              (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
            else (0, p)).fst
        else 0
[PROOFSTEP]
rw [modByMonic, dif_pos hq] at ih 
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
ih :
  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd =
    p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q -
      q * ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) /ₘ q)
⊢ (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
          (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
        (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd).snd =
    p -
      q *
        if h : Monic q then
          (if degree q ≤ degree p ∧ ¬p = 0 then
              (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
            else (0, p)).fst
        else 0
[PROOFSTEP]
refine' ih.trans _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
ih :
  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd =
    p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q -
      q * ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) /ₘ q)
⊢ p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q -
      q * ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) /ₘ q) =
    p -
      q *
        if h : Monic q then
          (if degree q ≤ degree p ∧ ¬p = 0 then
              (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
            else (0, p)).fst
        else 0
[PROOFSTEP]
unfold divByMonic
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : degree q ≤ degree p ∧ p ≠ 0
_wf : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p
ih :
  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).snd =
    p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q -
      q * ((p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) /ₘ q)
⊢ (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q -
      q *
        if hq : Monic q then (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq).fst
        else 0) =
    p -
      q *
        if h : Monic q then
          (if degree q ≤ degree p ∧ ¬p = 0 then
              (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
            else (0, p)).fst
        else 0
[PROOFSTEP]
rw [dif_pos hq, dif_pos hq, if_pos h, mul_add, sub_add_eq_sub_sub, mul_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ p %ₘ q = p - q * (p /ₘ q)
[PROOFSTEP]
unfold modByMonic divByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ (if h : Monic q then
      (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
          let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
          let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
          let dm := divModByMonicAux (p - z * q) (_ : Monic q);
          (z + dm.fst, dm.snd)
        else (0, p)).snd
    else p) =
    p -
      q *
        if h : Monic q then
          (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
              let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
              let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
              let dm := divModByMonicAux (p - z * q) (_ : Monic q);
              (z + dm.fst, dm.snd)
            else (0, p)).fst
        else 0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
h : ¬(degree q ≤ degree p ∧ p ≠ 0)
⊢ (if h : Monic q then
      (if degree q ≤ degree p ∧ ¬p = 0 then
          (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
        else (0, p)).snd
    else p) =
    p -
      q *
        if h : Monic q then
          (if degree q ≤ degree p ∧ ¬p = 0 then
              (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
                  (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
                (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
            else (0, p)).fst
        else 0
[PROOFSTEP]
rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : p /ₘ q = 0
⊢ degree p < degree q
[PROOFSTEP]
have := modByMonic_add_div p hq
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : p /ₘ q = 0
this : p %ₘ q + q * (p /ₘ q) = p
⊢ degree p < degree q
[PROOFSTEP]
rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this 
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
⊢ p /ₘ q = 0
[PROOFSTEP]
have : ¬degree q ≤ degree p := not_le_of_gt h
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ p /ₘ q = 0
[PROOFSTEP]
unfold divByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ (if h : Monic q then
      (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
          let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
          let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
          let dm := divModByMonicAux (p - z * q) (_ : Monic q);
          (z + dm.fst, dm.snd)
        else (0, p)).fst
    else 0) =
    0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ (if h : Monic q then
      (if degree q ≤ degree p ∧ ¬p = 0 then
          (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
        else (0, p)).fst
    else 0) =
    0
[PROOFSTEP]
rw [dif_pos hq, if_neg (mt And.left this)]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p
⊢ degree q + degree (p /ₘ q) = degree p
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p
✝ : Nontrivial R
⊢ degree q + degree (p /ₘ q) = degree p
[PROOFSTEP]
have hdiv0 : p /ₘ q ≠ 0 := by rwa [Ne.def, divByMonic_eq_zero_iff hq, not_lt]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p
✝ : Nontrivial R
⊢ p /ₘ q ≠ 0
[PROOFSTEP]
rwa [Ne.def, divByMonic_eq_zero_iff hq, not_lt]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p
✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ degree q + degree (p /ₘ q) = degree p
[PROOFSTEP]
have hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul, Ne.def, leadingCoeff_eq_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p
✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
[PROOFSTEP]
rwa [Monic.def.1 hq, one_mul, Ne.def, leadingCoeff_eq_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p
✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ degree q + degree (p /ₘ q) = degree p
[PROOFSTEP]
have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
  calc
    degree (p %ₘ q) < degree q := degree_modByMonic_lt _ hq
    _ ≤ _ :=
      by
      rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ← Nat.cast_add, Nat.cast_withBot,
        Nat.cast_withBot, WithBot.coe_le_coe]
      exact Nat.le_add_right _ _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p
✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ degree q ≤ degree (q * (p /ₘ q))
[PROOFSTEP]
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ← Nat.cast_add, Nat.cast_withBot,
  Nat.cast_withBot, WithBot.coe_le_coe]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p
✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ natDegree q ≤ natDegree q + natDegree (p /ₘ q)
[PROOFSTEP]
exact Nat.le_add_right _ _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : degree q ≤ degree p
✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
hmod : degree (p %ₘ q) < degree (q * (p /ₘ q))
⊢ degree q + degree (p /ₘ q) = degree p
[PROOFSTEP]
calc
  degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) := Eq.symm (degree_mul' hlc)
  _ = degree (p %ₘ q + q * (p /ₘ q)) := (degree_add_eq_right_of_degree_lt hmod).symm
  _ = _ := congr_arg _ (modByMonic_add_div _ hq)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : p = 0
⊢ degree (p /ₘ q) ≤ degree p
[PROOFSTEP]
simp only [hp0, zero_divByMonic, le_refl]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : degree q ≤ degree p
⊢ degree (p /ₘ q) ≤ degree p
[PROOFSTEP]
haveI := Nontrivial.of_polynomial_ne hp0
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : degree q ≤ degree p
this : Nontrivial R
⊢ degree (p /ₘ q) ≤ degree p
[PROOFSTEP]
rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
  degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : degree q ≤ degree p
this : Nontrivial R
⊢ ↑(natDegree (p /ₘ q)) ≤ ↑(natDegree q) + ↑(natDegree (p /ₘ q))
[PROOFSTEP]
exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : ¬degree q ≤ degree p
⊢ degree (p /ₘ q) ≤ degree p
[PROOFSTEP]
unfold divByMonic divModByMonicAux
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : ¬degree q ≤ degree p
⊢ degree
      (if h : Monic q then
        (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
            let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
            let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
            let dm := divModByMonicAux (p - z * q) (_ : Monic q);
            (z + dm.fst, dm.snd)
          else (0, p)).fst
      else 0) ≤
    degree p
[PROOFSTEP]
simp [dif_pos hq, h, false_and_iff, if_false, degree_zero, bot_le]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : degree p < degree q
⊢ degree (p /ₘ q) < degree p
[PROOFSTEP]
haveI := Nontrivial.of_polynomial_ne hp0
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : degree p < degree q
this : Nontrivial R
⊢ degree (p /ₘ q) < degree p
[PROOFSTEP]
rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : degree p < degree q
this : Nontrivial R
⊢ degree 0 < ↑(natDegree p)
[PROOFSTEP]
exact WithBot.bot_lt_coe _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
⊢ degree (p /ₘ q) < degree p
[PROOFSTEP]
haveI := Nontrivial.of_polynomial_ne hp0
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
this : Nontrivial R
⊢ degree (p /ₘ q) < degree p
[PROOFSTEP]
rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
  degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
this : Nontrivial R
⊢ ↑(natDegree (p /ₘ q)) < ↑(natDegree q) + ↑(natDegree (p /ₘ q))
[PROOFSTEP]
exact
  WithBot.coe_lt_coe.2
    (Nat.lt_add_of_pos_left
      (WithBot.coe_lt_coe.1 <| by simpa [Nat.cast_withBot, degree_eq_natDegree hq.ne_zero] using h0q))
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
this : Nontrivial R
⊢ ↑0 < ↑↑(natDegree q)
[PROOFSTEP]
simpa [Nat.cast_withBot, degree_eq_natDegree hq.ne_zero] using h0q
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
nontriviality R
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
by_cases hfg : f /ₘ g = 0
[GOAL]
case pos
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
rw [hfg, natDegree_zero]
[GOAL]
case pos
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = natDegree f - natDegree g
[PROOFSTEP]
rw [divByMonic_eq_zero_iff hg] at hfg 
[GOAL]
case pos
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : degree f < degree g
⊢ 0 = natDegree f - natDegree g
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr (natDegree_le_natDegree <| le_of_lt hfg)]
[GOAL]
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
have hgf := hfg
[GOAL]
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg hgf : ¬f /ₘ g = 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
rw [divByMonic_eq_zero_iff hg] at hgf 
[GOAL]
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬degree f < degree g
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
push_neg at hgf 
[GOAL]
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
have := degree_add_divByMonic hg hgf
[GOAL]
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
have hf : f ≠ 0 := by
  intro hf
  apply hfg
  rw [hf, zero_divByMonic]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
⊢ f ≠ 0
[PROOFSTEP]
intro hf
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
hf : f = 0
⊢ False
[PROOFSTEP]
apply hfg
[GOAL]
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
hf : f = 0
⊢ f /ₘ g = 0
[PROOFSTEP]
rw [hf, zero_divByMonic]
[GOAL]
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : degree g + degree (f /ₘ g) = degree f
hf : f ≠ 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg, Nat.cast_withBot, Nat.cast_withBot,
  Nat.cast_withBot, ← WithBot.coe_add, WithBot.coe_eq_coe] at this 
[GOAL]
case neg
R✝ : Type u
S : Type v
T : Type w
A : Type z
a b : R✝
n : ℕ
inst✝¹ : CommRing R✝
p q : R✝[X]
R : Type u
inst✝ : CommRing R
f g : R[X]
hg : Monic g
✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : degree g ≤ degree f
this : natDegree g + natDegree (f /ₘ g) = natDegree f
hf : f ≠ 0
⊢ natDegree (f /ₘ g) = natDegree f - natDegree g
[PROOFSTEP]
rw [← this, add_tsub_cancel_left]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
⊢ f /ₘ g = q ∧ f %ₘ g = r
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
⊢ f /ₘ g = q ∧ f %ₘ g = r
[PROOFSTEP]
have h₁ : r - f %ₘ g = -g * (q - f /ₘ g) :=
  eq_of_sub_eq_zero
    (by
      rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f hg).symm)]
      simp [mul_add, mul_comm, sub_eq_add_neg, add_comm, add_left_comm, add_assoc])
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = 0
[PROOFSTEP]
rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f hg).symm)]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = r + g * q - (f %ₘ g + g * (f /ₘ g))
[PROOFSTEP]
simp [mul_add, mul_comm, sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
⊢ f /ₘ g = q ∧ f %ₘ g = r
[PROOFSTEP]
have h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g)) := by simp [h₁]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
⊢ degree (r - f %ₘ g) = degree (g * (q - f /ₘ g))
[PROOFSTEP]
simp [h₁]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g))
⊢ f /ₘ g = q ∧ f %ₘ g = r
[PROOFSTEP]
have h₄ : degree (r - f %ₘ g) < degree g :=
  calc
    degree (r - f %ₘ g) ≤ max (degree r) (degree (f %ₘ g)) := degree_sub_le _ _
    _ < degree g := max_lt_iff.2 ⟨h.2, degree_modByMonic_lt _ hg⟩
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g))
h₄ : degree (r - f %ₘ g) < degree g
⊢ f /ₘ g = q ∧ f %ₘ g = r
[PROOFSTEP]
have h₅ : q - f /ₘ g = 0 :=
  _root_.by_contradiction fun hqf =>
    not_le_of_gt h₄ <|
      calc
        degree g ≤ degree g + degree (q - f /ₘ g) :=
          by
          erw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf, WithBot.coe_le_coe]
          exact Nat.le_add_right _ _
        _ = degree (r - f %ₘ g) := by rw [h₂, degree_mul']; simpa [Monic.def.1 hg]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g))
h₄ : degree (r - f %ₘ g) < degree g
hqf : ¬q - f /ₘ g = 0
⊢ degree g ≤ degree g + degree (q - f /ₘ g)
[PROOFSTEP]
erw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf, WithBot.coe_le_coe]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g))
h₄ : degree (r - f %ₘ g) < degree g
hqf : ¬q - f /ₘ g = 0
⊢ ↑(natDegree g) ≤ (fun x x_1 => x + x_1) ↑(natDegree g) ↑(natDegree (q - f /ₘ g))
[PROOFSTEP]
exact Nat.le_add_right _ _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g))
h₄ : degree (r - f %ₘ g) < degree g
hqf : ¬q - f /ₘ g = 0
⊢ degree g + degree (q - f /ₘ g) = degree (r - f %ₘ g)
[PROOFSTEP]
rw [h₂, degree_mul']
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g))
h₄ : degree (r - f %ₘ g) < degree g
hqf : ¬q - f /ₘ g = 0
⊢ leadingCoeff g * leadingCoeff (q - f /ₘ g) ≠ 0
[PROOFSTEP]
simpa [Monic.def.1 hg]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g))
h₄ : degree (r - f %ₘ g) < degree g
h₅ : q - f /ₘ g = 0
⊢ f /ₘ g = q ∧ f %ₘ g = r
[PROOFSTEP]
exact ⟨Eq.symm <| eq_of_sub_eq_zero h₅, Eq.symm <| eq_of_sub_eq_zero <| by simpa [h₅] using h₁⟩
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q✝ : R[X]
f g : R[X]
q r : R[X]
hg : Monic g
h : r + g * q = f ∧ degree r < degree g
✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g))
h₄ : degree (r - f %ₘ g) < degree g
h₅ : q - f /ₘ g = 0
⊢ r - f %ₘ g = 0
[PROOFSTEP]
simpa [h₅] using h₁
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
[PROOFSTEP]
nontriviality S
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
[PROOFSTEP]
haveI : Nontrivial R := f.domain_nontrivial
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
[PROOFSTEP]
have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
  div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
    ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div _ hq],
      calc
        _ ≤ degree (p %ₘ q) := degree_map_le _ _
        _ < degree q := (degree_modByMonic_lt _ hq)
        _ = _ :=
          Eq.symm <| degree_map_eq_of_leadingCoeff_ne_zero _ (by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q) + map f q * map f (p /ₘ q)
[PROOFSTEP]
rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div _ hq]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ ↑f (leadingCoeff q) ≠ 0
[PROOFSTEP]
rw [Monic.def.1 hq, f.map_one]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this✝ : Nontrivial R
this : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
[PROOFSTEP]
exact ⟨this.1.symm, this.2.symm⟩
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : p %ₘ q = 0
⊢ q ∣ p
[PROOFSTEP]
rw [← modByMonic_add_div p hq, h, zero_add]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
⊢ p %ₘ q = 0
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
⊢ p %ₘ q = 0
[PROOFSTEP]
obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
⊢ p %ₘ q = 0
[PROOFSTEP]
by_contra hpq0
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ False
[PROOFSTEP]
have hmod : p %ₘ q = q * (r - p /ₘ q) := by rw [modByMonic_eq_sub_mul_div _ hq, mul_sub, ← hr]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ p %ₘ q = q * (r - p /ₘ q)
[PROOFSTEP]
rw [modByMonic_eq_sub_mul_div _ hq, mul_sub, ← hr]
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
⊢ False
[PROOFSTEP]
have : degree (q * (r - p /ₘ q)) < degree q := hmod ▸ degree_modByMonic_lt _ hq
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
⊢ False
[PROOFSTEP]
have hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0 := fun h =>
  hpq0 <| leadingCoeff_eq_zero.1 (by rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero])
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h✝ : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
h : leadingCoeff (r - p /ₘ q) = 0
⊢ leadingCoeff (p %ₘ q) = 0
[PROOFSTEP]
rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero]
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
⊢ False
[PROOFSTEP]
have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
⊢ leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0
[PROOFSTEP]
rwa [Monic.def.1 hq, one_mul]
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0
⊢ False
[PROOFSTEP]
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] at this 
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : ↑(natDegree q) + ↑(natDegree (r - p /ₘ q)) < ↑(natDegree q)
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0
⊢ False
[PROOFSTEP]
exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.some_lt_some.1 this)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ↑f
x y : R[X]
hx : Monic x
⊢ map f x ∣ map f y ↔ x ∣ y
[PROOFSTEP]
rw [← dvd_iff_modByMonic_eq_zero hx, ← dvd_iff_modByMonic_eq_zero (hx.map f), ← map_modByMonic f hx]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ↑f
x y : R[X]
hx : Monic x
⊢ map f (y %ₘ x) = 0 ↔ y %ₘ x = 0
[PROOFSTEP]
exact ⟨fun H => map_injective f hf <| by rw [H, Polynomial.map_zero], fun H => by rw [H, Polynomial.map_zero]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ↑f
x y : R[X]
hx : Monic x
H : map f (y %ₘ x) = 0
⊢ map f (y %ₘ x) = map f 0
[PROOFSTEP]
rw [H, Polynomial.map_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ↑f
x y : R[X]
hx : Monic x
H : y %ₘ x = 0
⊢ map f (y %ₘ x) = 0
[PROOFSTEP]
rw [H, Polynomial.map_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
⊢ Monic 1
[PROOFSTEP]
convert monic_one (R := R)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
⊢ p /ₘ 1 = p
[PROOFSTEP]
conv_rhs => rw [← modByMonic_add_div p monic_one]; simp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
| p
[PROOFSTEP]
rw [← modByMonic_add_div p monic_one]; simp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
| p
[PROOFSTEP]
rw [← modByMonic_add_div p monic_one]; simp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
| p
[PROOFSTEP]
rw [← modByMonic_add_div p monic_one]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
| p %ₘ 1 + 1 * (p /ₘ 1)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
[PROOFSTEP]
have h : (p %ₘ (X - C a)).eval a = p.eval a := by
  rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul,
    sub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
⊢ eval a (p %ₘ (X - ↑C a)) = eval a p
[PROOFSTEP]
rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul,
  sub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
[PROOFSTEP]
have : degree (p %ₘ (X - C a)) < 1 := degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
this : degree (p %ₘ (X - ↑C a)) < 1
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
[PROOFSTEP]
have : degree (p %ₘ (X - C a)) ≤ 0 := by
  revert this
  cases degree (p %ₘ (X - C a))
  · exact fun _ => bot_le
  · exact fun h => WithBot.some_le_some.2 (Nat.le_of_lt_succ (WithBot.some_lt_some.1 h))
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
this : degree (p %ₘ (X - ↑C a)) < 1
⊢ degree (p %ₘ (X - ↑C a)) ≤ 0
[PROOFSTEP]
revert this
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
⊢ degree (p %ₘ (X - ↑C a)) < 1 → degree (p %ₘ (X - ↑C a)) ≤ 0
[PROOFSTEP]
cases degree (p %ₘ (X - C a))
[GOAL]
case none
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
⊢ none < 1 → none ≤ 0
[PROOFSTEP]
exact fun _ => bot_le
[GOAL]
case some
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
val✝ : ℕ
⊢ some val✝ < 1 → some val✝ ≤ 0
[PROOFSTEP]
exact fun h => WithBot.some_le_some.2 (Nat.le_of_lt_succ (WithBot.some_lt_some.1 h))
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : eval a (p %ₘ (X - ↑C a)) = eval a p
this✝ : degree (p %ₘ (X - ↑C a)) < 1
this : degree (p %ₘ (X - ↑C a)) ≤ 0
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
[PROOFSTEP]
rw [eq_C_of_degree_le_zero this, eval_C] at h 
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
✝ : Nontrivial R
h : coeff (p %ₘ (X - ↑C a)) 0 = eval a p
this✝ : degree (p %ₘ (X - ↑C a)) < 1
this : degree (p %ₘ (X - ↑C a)) ≤ 0
⊢ p %ₘ (X - ↑C a) = ↑C (eval a p)
[PROOFSTEP]
rw [eq_C_of_degree_le_zero this, h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : (X - ↑C a) * (p /ₘ (X - ↑C a)) = p
⊢ IsRoot p a
[PROOFSTEP]
rw [← h, IsRoot.def, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : eval a p = 0
⊢ (X - ↑C a) * (p /ₘ (X - ↑C a)) = p
[PROOFSTEP]
conv_rhs =>
  rw [← modByMonic_add_div p (monic_X_sub_C a)]
  rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : eval a p = 0
| p
[PROOFSTEP]
  rw [← modByMonic_add_div p (monic_X_sub_C a)]
  rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : eval a p = 0
| p
[PROOFSTEP]
  rw [← modByMonic_add_div p (monic_X_sub_C a)]
  rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : eval a p = 0
| p
[PROOFSTEP]
rw [← modByMonic_add_div p (monic_X_sub_C a)]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : eval a p = 0
| p %ₘ (X - ↑C a) + (X - ↑C a) * (p /ₘ (X - ↑C a))
[PROOFSTEP]
rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : X - ↑C a ∣ p
⊢ IsRoot p a
[PROOFSTEP]
rwa [← dvd_iff_modByMonic_eq_zero (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0, C_inj] at h 
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : IsRoot p a
⊢ p = (X - ↑C a) * (p /ₘ (X - ↑C a))
[PROOFSTEP]
rw [mul_divByMonic_eq_iff_isRoot.2 h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
⊢ X - ↑C a ∣ p - ↑C (eval a p)
[PROOFSTEP]
rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p q b : R[X]
P : R[X][X]
⊢ P ∈ Ideal.span {↑C (X - ↑C a), X - ↑C b} ↔ eval a (eval b P) = 0
[PROOFSTEP]
rw [Ideal.mem_span_pair]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p q b : R[X]
P : R[X][X]
⊢ (∃ a_1 b_1, a_1 * ↑C (X - ↑C a) + b_1 * (X - ↑C b) = P) ↔ eval a (eval b P) = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p q b : R[X]
P : R[X][X]
⊢ (∃ a_1 b_1, a_1 * ↑C (X - ↑C a) + b_1 * (X - ↑C b) = P) → eval a (eval b P) = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p q b : R[X]
P : R[X][X]
⊢ eval a (eval b P) = 0 → ∃ a_2 b_1, a_2 * ↑C (X - ↑C a) + b_1 * (X - ↑C b) = P
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p q b : R[X]
P : R[X][X]
h : ∃ a_1 b_1, a_1 * ↑C (X - ↑C a) + b_1 * (X - ↑C b) = P
⊢ eval a (eval b P) = 0
[PROOFSTEP]
rcases h with ⟨_, _, rfl⟩
[GOAL]
case mp.intro.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p q b : R[X]
w✝¹ w✝ : R[X][X]
⊢ eval a (eval b (w✝¹ * ↑C (X - ↑C a) + w✝ * (X - ↑C b))) = 0
[PROOFSTEP]
simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul, add_zero, mul_zero, sub_self]
[GOAL]
case mpr
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p q b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
⊢ ∃ a_1 b_1, a_1 * ↑C (X - ↑C a) + b_1 * (X - ↑C b) = P
[PROOFSTEP]
rcases dvd_iff_isRoot.mpr h with ⟨p, hp⟩
[GOAL]
case mpr.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p✝ q b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - ↑C a) * p
⊢ ∃ a_1 b_1, a_1 * ↑C (X - ↑C a) + b_1 * (X - ↑C b) = P
[PROOFSTEP]
rcases@X_sub_C_dvd_sub_C_eval _ b _ P with ⟨q, hq⟩
[GOAL]
case mpr.intro.intro
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - ↑C a) * p
q : R[X][X]
hq : P - ↑C (eval b P) = (X - ↑C b) * q
⊢ ∃ a_1 b_1, a_1 * ↑C (X - ↑C a) + b_1 * (X - ↑C b) = P
[PROOFSTEP]
exact ⟨C p, q, by rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b✝ : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - ↑C a) * p
q : R[X][X]
hq : P - ↑C (eval b P) = (X - ↑C b) * q
⊢ ↑C p * ↑C (X - ↑C a) + q * (X - ↑C b) = P
[PROOFSTEP]
rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
⊢ p %ₘ X = ↑C (eval 0 p)
[PROOFSTEP]
rw [← modByMonic_X_sub_C_eq_C_eval, C_0, sub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q✝ : R[X]
inst✝ : CommRing S
f : R →+* S
p q : R[X]
hq : Monic q
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p
[PROOFSTEP]
rw [modByMonic_eq_sub_mul_div p hq, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
n : ℕ
hn : degree q ≤ ↑n
⊢ ∑ i : Fin n, ↑(monomial ↑i) (coeff (p %ₘ q) ↑i) = p %ₘ q
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
n : ℕ
hn : degree q ≤ ↑n
✝ : Nontrivial R
⊢ ∑ i : Fin n, ↑(monomial ↑i) (coeff (p %ₘ q) ↑i) = p %ₘ q
[PROOFSTEP]
exact (sum_fin (fun i c => monomial i c) (by simp) ((degree_modByMonic_lt _ hq).trans_le hn)).trans (sum_monomial_eq _)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
n : ℕ
hn : degree q ≤ ↑n
✝ : Nontrivial R
⊢ ∀ (i : ℕ), (fun i c => ↑(monomial i) c) i 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b✝ : R
n : ℕ
inst✝ : CommRing R
p✝ q : R[X]
a b : R
p : R[X]
⊢ a - b ∣ eval a p - eval b p
[PROOFSTEP]
suffices X - C b ∣ p - C (p.eval b) by
  simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C] using (evalRingHom a).map_dvd this
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b✝ : R
n : ℕ
inst✝ : CommRing R
p✝ q : R[X]
a b : R
p : R[X]
this : X - ↑C b ∣ p - ↑C (eval b p)
⊢ a - b ∣ eval a p - eval b p
[PROOFSTEP]
simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C] using (evalRingHom a).map_dvd this
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b✝ : R
n : ℕ
inst✝ : CommRing R
p✝ q : R[X]
a b : R
p : R[X]
⊢ X - ↑C b ∣ p - ↑C (eval b p)
[PROOFSTEP]
simp [dvd_iff_isRoot]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
⊢ q * p /ₘ q = p
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ q * p /ₘ q = p
[PROOFSTEP]
refine' (div_modByMonic_unique _ 0 hmo ⟨by rw [zero_add], _⟩).1
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ 0 + q * p = q * p
[PROOFSTEP]
rw [zero_add]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ degree 0 < degree q
[PROOFSTEP]
rw [degree_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ ⊥ < degree q
[PROOFSTEP]
exact Ne.bot_lt fun h => hmo.ne_zero (degree_eq_bot.1 h)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
⊢ ¬IsField R[X]
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ¬IsField R[X]
[PROOFSTEP]
rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ∃ I, ⊥ < I ∧ I < ⊤
[PROOFSTEP]
use Ideal.span { Polynomial.X }
[GOAL]
case h
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ⊥ < Ideal.span {X} ∧ Ideal.span {X} < ⊤
[PROOFSTEP]
constructor
[GOAL]
case h.left
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ⊥ < Ideal.span {X}
[PROOFSTEP]
rw [bot_lt_iff_ne_bot, Ne.def, Ideal.span_singleton_eq_bot]
[GOAL]
case h.left
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ¬X = 0
[PROOFSTEP]
exact Polynomial.X_ne_zero
[GOAL]
case h.right
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ Ideal.span {X} < ⊤
[PROOFSTEP]
rw [lt_top_iff_ne_top, Ne.def, Ideal.eq_top_iff_one, Ideal.mem_span_singleton, Polynomial.X_dvd_iff,
  Polynomial.coeff_one_zero]
[GOAL]
case h.right
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ¬1 = 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
x : R
⊢ RingHom.ker (evalRingHom x) = Ideal.span {X - ↑C x}
[PROOFSTEP]
ext y
[GOAL]
case h
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
x : R
y : R[X]
⊢ y ∈ RingHom.ker (evalRingHom x) ↔ y ∈ Ideal.span {X - ↑C x}
[PROOFSTEP]
simp [Ideal.mem_span_singleton, dvd_iff_isRoot, RingHom.mem_ker]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
⊢ multiplicity.Finite (X - ↑C a) p
[PROOFSTEP]
haveI := Nontrivial.of_polynomial_ne h0
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ multiplicity.Finite (X - ↑C a) p
[PROOFSTEP]
refine' multiplicity_finite_of_degree_pos_of_monic _ (monic_X_sub_C _) h0
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < degree (X - ↑C a)
[PROOFSTEP]
rw [degree_X_sub_C]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
p0 : p ≠ 0
a : R
⊢ rootMultiplicity a p = Nat.find (_ : multiplicity.Finite (X - ↑C a) p)
[PROOFSTEP]
dsimp [rootMultiplicity]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
p0 : p ≠ 0
a : R
⊢ (if h0 : p = 0 then 0 else Nat.find (_ : multiplicity.Finite (X - ↑C a) p)) =
    Nat.find (_ : multiplicity.Finite (X - ↑C a) p)
[PROOFSTEP]
rw [dif_neg p0]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
p0 : p ≠ 0
a : R
⊢ Nat.find (_ : multiplicity.Finite (X - ↑C a) p) = Nat.find (_ : multiplicity.Finite (X - ↑C a) p)
[PROOFSTEP]
convert rfl
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
⊢ rootMultiplicity a p =
    if h0 : p = 0 then 0 else Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p)
[PROOFSTEP]
simp [multiplicity, rootMultiplicity, Part.Dom]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
⊢ (if h : p = 0 then 0 else Nat.find (_ : multiplicity.Finite (X - ↑C a) p)) =
    if h : p = 0 then 0 else Nat.find (_ : (PartENat.find fun n => ¬(X - ↑C a) ^ (n + 1) ∣ p).Dom)
[PROOFSTEP]
congr
[GOAL]
case e_e
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
⊢ (fun h => Nat.find (_ : multiplicity.Finite (X - ↑C a) p)) = fun h =>
    Nat.find (_ : (PartENat.find fun n => ¬(X - ↑C a) ^ (n + 1) ∣ p).Dom)
[PROOFSTEP]
funext
[GOAL]
case e_e.h
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
x✝ : ¬p = 0
⊢ Nat.find (_ : multiplicity.Finite (X - ↑C a) p) =
    Nat.find (_ : (PartENat.find fun n => ¬(X - ↑C a) ^ (n + 1) ∣ p).Dom)
[PROOFSTEP]
congr
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
x : R
⊢ rootMultiplicity x p = 0 ↔ IsRoot p x → p = 0
[PROOFSTEP]
simp only [rootMultiplicity_eq_multiplicity, dite_eq_left_iff, PartENat.get_eq_iff_eq_coe, Nat.cast_zero,
  multiplicity.multiplicity_eq_zero, dvd_iff_isRoot, not_imp_not]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
x : R
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ IsRoot p x
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne.def, rootMultiplicity_eq_zero_iff, not_imp, and_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
r a : R
⊢ rootMultiplicity a (↑C r) = 0
[PROOFSTEP]
simp only [rootMultiplicity_eq_zero_iff, IsRoot, eval_C, C_eq_zero, imp_self]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
h : p = 0
⊢ (X - ↑C a) ^ rootMultiplicity a p ∣ p
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
h : ¬p = 0
⊢ (X - ↑C a) ^ rootMultiplicity a p ∣ p
[PROOFSTEP]
rw [rootMultiplicity_eq_multiplicity, dif_neg h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
h : ¬p = 0
⊢ (X - ↑C a) ^ Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) ∣ p
[PROOFSTEP]
exact multiplicity.pow_multiplicity_dvd _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
⊢ p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p = p
[PROOFSTEP]
have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
this : Monic ((X - ↑C a) ^ rootMultiplicity a p)
⊢ p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p = p
[PROOFSTEP]
conv_rhs => rw [← modByMonic_add_div p this, (dvd_iff_modByMonic_eq_zero this).2 (pow_rootMultiplicity_dvd _ _)]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
this : Monic ((X - ↑C a) ^ rootMultiplicity a p)
| p
[PROOFSTEP]
rw [← modByMonic_add_div p this, (dvd_iff_modByMonic_eq_zero this).2 (pow_rootMultiplicity_dvd _ _)]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
this : Monic ((X - ↑C a) ^ rootMultiplicity a p)
| p
[PROOFSTEP]
rw [← modByMonic_add_div p this, (dvd_iff_modByMonic_eq_zero this).2 (pow_rootMultiplicity_dvd _ _)]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
this : Monic ((X - ↑C a) ^ rootMultiplicity a p)
| p
[PROOFSTEP]
rw [← modByMonic_add_div p this, (dvd_iff_modByMonic_eq_zero this).2 (pow_rootMultiplicity_dvd _ _)]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
this : Monic ((X - ↑C a) ^ rootMultiplicity a p)
⊢ p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p =
    0 + (X - ↑C a) ^ rootMultiplicity a p * (p /ₘ (X - ↑C a) ^ rootMultiplicity a p)
[PROOFSTEP]
simp [mul_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
hp : p ≠ 0
⊢ eval a (p /ₘ (X - ↑C a) ^ rootMultiplicity a p) ≠ 0
[PROOFSTEP]
haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ eval a (p /ₘ (X - ↑C a) ^ rootMultiplicity a p) ≠ 0
[PROOFSTEP]
rw [Ne.def, ← IsRoot.def, ← dvd_iff_isRoot]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ ¬X - ↑C a ∣ p /ₘ (X - ↑C a) ^ rootMultiplicity a p
[PROOFSTEP]
rintro ⟨q, hq⟩
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
⊢ False
[PROOFSTEP]
have := divByMonic_mul_pow_rootMultiplicity_eq p a
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p = p
⊢ False
[PROOFSTEP]
rw [mul_comm, hq, ← mul_assoc, ← pow_succ', rootMultiplicity_eq_multiplicity, dif_neg hp] at this 
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ False
[PROOFSTEP]
exact
  multiplicity.is_greatest'
    (multiplicity_finite_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; exact by decide) (monic_X_sub_C _) hp)
    (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ 0 < degree (X - ↑C a)
[PROOFSTEP]
rw [degree_X_sub_C]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ 0 < 1
[PROOFSTEP]
exact by decide
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ 0 < 1
[PROOFSTEP]
decide
