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
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
have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp
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
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
have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr
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
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
have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1 := by simp [show _ = _ from hmp]
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
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
have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm
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
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
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]
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
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
have hnp : 0 < natDegree p := by
  rw [← WithBot.coe_lt_coe, ← Nat.cast_withBot, ← Nat.cast_withBot,
    ← degree_eq_natDegree hp0]; exact hp
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
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
have := congr_arg natDegree hr
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
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
rw [natDegree_mul' hpnr0, natDegree_pow' hpn0', add_mul, add_assoc] at this
no goals
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
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
no goals
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
simp [hp0] at hp
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
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
subst hr0
no goals
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
simp [hq] at hr
no goals
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
simp [show _ = _ from hmp]
no goals
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
simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_pow, one_mul, Ne.def,
    hr0]
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
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
rw [← WithBot.coe_lt_coe, ← Nat.cast_withBot, ← Nat.cast_withBot,
  ← degree_eq_natDegree hp0]
no goals
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
exact hp
no goals
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
rwa [one_mul]