case inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p

case inr
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
⊢ natDegree (↑(expand R p) f) = natDegree f * p
cases' p.eq_zero_or_pos with hp hp
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p

case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
case inr
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
by_cases hf : f = 0
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree (↑(expand R p) f)) = ↑(natDegree f * p)
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
rw [← WithBot.coe_eq_coe]
case h.e'_3
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree f * p) = degree (↑(expand R p) f)
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree (↑(expand R p) f)) = ↑(natDegree f * p)
convert (degree_eq_natDegree hf1).symm
case h.e'_3
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ degree (↑(expand R p) f) = ↑(natDegree f * p)
case h.e'_3
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree f * p) = degree (↑(expand R p) f)
symm
case h.e'_3.refine'_1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
⊢ coeff (↑(expand R p) f) n = 0

case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree f * p) ≤ degree (↑(expand R p) f)
case h.e'_3
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ degree (↑(expand R p) f) = ↑(natDegree f * p)
refine' le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => _) _
no goals
case inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
rw [hp, coe_expand, pow_zero, MulZeroClass.mul_zero, ← C_1, eval₂_hom, natDegree_C]
no goals
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
rw [hf, AlgHom.map_zero, natDegree_zero, MulZeroClass.zero_mul]
case h.e'_3.refine'_1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
⊢ (if p ∣ n then coeff f (n / p) else 0) = 0
case h.e'_3.refine'_1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
⊢ coeff (↑(expand R p) f) n = 0
rw [coeff_expand hp]
case h.e'_3.refine'_1.inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : p ∣ n
⊢ coeff f (n / p) = 0

case h.e'_3.refine'_1.inr
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0
case h.e'_3.refine'_1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
⊢ (if p ∣ n then coeff f (n / p) else 0) = 0
split_ifs with hpn
case h.e'_3.refine'_1.inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : p ∣ n
⊢ natDegree f < n / p
case h.e'_3.refine'_1.inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : p ∣ n
⊢ coeff f (n / p) = 0
rw [coeff_eq_zero_of_natDegree_lt]
case h.e'_3.refine'_1.inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ natDegree f
⊢ ↑n ≤ ↑(natDegree f * p)
case h.e'_3.refine'_1.inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : p ∣ n
⊢ natDegree f < n / p
contrapose! hn
case h.e'_3.refine'_1.inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ natDegree f
⊢ ↑(n / p * p) ≤ natDegree f * p
case h.e'_3.refine'_1.inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ natDegree f
⊢ ↑n ≤ ↑(natDegree f * p)
erw [WithBot.coe_le_coe, ← Nat.div_mul_cancel hpn]
no goals
case h.e'_3.refine'_1.inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ natDegree f
⊢ ↑(n / p * p) ≤ natDegree f * p
exact Nat.mul_le_mul_right p hn
no goals
case h.e'_3.refine'_1.inr
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0
rfl
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ coeff (↑(expand R p) f) (Mul.mul (natDegree f) p) ≠ 0
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree f * p) ≤ degree (↑(expand R p) f)
refine' le_degree_of_ne_zero _
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ leadingCoeff f ≠ 0
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ coeff (↑(expand R p) f) (Mul.mul (natDegree f) p) ≠ 0
erw [coeff_expand_mul hp, ← leadingCoeff]
no goals
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ leadingCoeff f ≠ 0
exact mt leadingCoeff_eq_zero.1 hf