-- Mathlib/Algebra/Polynomial/Expand.lean
theorem natDegree_expand (p : ℕ) (f : R[X]) : (expand R p f).natDegree = f.natDegree * p

Proof state:
case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]

Result:
no goals

Proof state:
case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ↑(f.natDegree * p) ≤ ((expand R p) f).degree

Tactic:
refine le_degree_of_ne_zero ?_

Result:
case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).coeff (f.natDegree * p) ≠ 0

Proof state:
case inr
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
by_cases hf : f = 0

Result:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ f.coeff (n / p) = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

Result:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ f.natDegree < n / p

Proof state:
case neg.refine_1
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
⊢ (if p ∣ n then f.coeff (n / p) else 0) = 0

Tactic:
split_ifs with hpn

Result:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ f.coeff (n / p) = 0

case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
rw [hf, map_zero, natDegree_zero, zero_mul]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ ↑n ≤ ↑(f.natDegree * p)

Tactic:
norm_cast

Result:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ n ≤ f.natDegree * p

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf

Result:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).coeff (f.natDegree * p) ≠ 0

Tactic:
rw [coeff_expand_mul hp, ← leadingCoeff]

Result:
case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ f.leadingCoeff ≠ 0

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ f.natDegree < n / p

Tactic:
contrapose! hn

Result:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ ↑n ≤ ↑(f.natDegree * p)

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
rcases p.eq_zero_or_pos with hp | hp

Result:
case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

case inr
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).degree = ↑(f.natDegree * p)

Tactic:
refine le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => ?_) ?_

Result:
case neg.refine_1
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
⊢ ((expand R p) f).coeff n = 0

case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ↑(f.natDegree * p) ≤ ((expand R p) f).degree

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ n ≤ f.natDegree * p

Tactic:
rw [← Nat.div_mul_cancel hpn]

Result:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ n / p * p ≤ f.natDegree * p

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ n / p * p ≤ f.natDegree * p

Tactic:
exact Nat.mul_le_mul_right p hn

Result:
no goals

Proof state:
case neg.refine_1
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
⊢ ((expand R p) f).coeff n = 0

Tactic:
rw [coeff_expand hp]

Result:
case neg.refine_1
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
⊢ (if p ∣ n then f.coeff (n / p) else 0) = 0

Proof state:
case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ f.leadingCoeff ≠ 0

Tactic:
exact mt leadingCoeff_eq_zero.1 hf

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hf1]

Result:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).degree = ↑(f.natDegree * p)