awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
simp :
  coeff
      (f.sum fun (e : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X p ^ e))
      n =
    if p ∣ n then f.coeff (n / p) else 0
⊢ coeff ((expand R p : (a : R[X]) → R[X]) f) n = if p ∣ n then f.coeff (n / p) else 0

Tactic:
simp only [expand_eq_sum]

Premises used: Polynomial.expand_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
simp_rw : (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = if p ∣ n then f.coeff (n / p) else 0
⊢ coeff
      (f.sum fun (e : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X p ^ e))
      n =
    if p ∣ n then f.coeff (n / p) else 0

Tactic:
simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum]

Premises used: Polynomial.sum, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.coeff_monomial, pow_mul, Polynomial.coeff_sum
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
pos : ∀ (h : p ∣ n), (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = f.coeff (n / p)
neg : ∀ (h : ¬p ∣ n), Eq.{u + 1} (α := R) (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) 0
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = if p ∣ n then f.coeff (n / p) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
pos : ∀ b ∈ f.support, b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0
pos₁ : n / p ∉ f.support → (if p * (n / p) = n then f.coeff (n / p) else 0) = 0
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = f.coeff (n / p)

Tactic:
rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]

Premises used: HDiv.hDiv, if_pos, Finset.sum_eq_single, Nat.mul_div_cancel', rfl
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
pos : b ∈ f.support → b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0
⊢ b ∈ f.support → b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0

Tactic:
_
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
h_1 : b ∈ f.support
hb2 : b ≠ n / p
pos : ¬p * b = n
⊢ (if p * b = n then f.coeff b else 0) = 0

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
h_1 : b ∈ f.support
hb2 : b ≠ n / p
hb3 : p * b = n
pos : b = n / p
⊢ False

Tactic:
apply hb2
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
h_1 : b ∈ f.support
hb2 : b ≠ n / p
hb3 : p * b = n
pos : b = p * b / p
pos₁ pos₂ : b = b
⊢ b = n / p

Tactic:
rw [← hb3, Nat.mul_div_cancel_left b hp]

Premises used: Nat.mul_div_cancel_left
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
pos : Eq.{u + 1} (α := R) (if p * (n / p) = n then 0 else 0) 0
⊢ (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Tactic:
rw [notMem_support_iff.1 hn]

Premises used: Polynomial.notMem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
pos : p * (n / p) = n → Eq.{u + 1} (α := R) 0 0
neg : ¬p * (n / p) = n → Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) (if p * (n / p) = n then 0 else 0) 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h_1 : p * (n / p) = n
⊢ Eq.{u + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h_1 : ¬p * (n / p) = n
⊢ Eq.{u + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
neg : ∀ x ∈ f.support, (if p * x = n then f.coeff x else 0) = 0
⊢ Eq.{u + 1} (α := R) (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) 0

Tactic:
rw [Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
neg : k ∈ f.support → (if p * k = n then f.coeff k else 0) = 0
⊢ k ∈ f.support → (if p * k = n then f.coeff k else 0) = 0

Tactic:
_
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
h_1 : k ∈ f.support
neg : ¬p * k = n
⊢ (if p * k = n then f.coeff k else 0) = 0

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
h_1 : k ∈ f.support
⊢ ¬p * k = n

Tactic:
fun hkn => h ⟨k, hkn.symm⟩

Premises used: Exists.intro, Eq.symm, Not
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
h_1 : k ∈ f.support
⊢ ¬p * k = n

Tactic:
exact fun hkn => h ⟨k, hkn.symm⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
rw : (if p ∣ n * p then f.coeff (n * p / p) else 0) = f.coeff n
rw₁ : f.coeff (n * p / p) = f.coeff n
rw₂ rw₃ : f.coeff n = f.coeff n
⊢ coeff ((expand R p : (a : R[X]) → R[X]) f) (n * p) = f.coeff n

Tactic:
rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]

Premises used: Nat.mul_div_cancel, if_pos, dvd_mul_left, Polynomial.coeff_expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
rw : coeff ((expand R p : (a : R[X]) → R[X]) f) (n * p) = f.coeff n
rw₁ rw₂ : f.coeff n = f.coeff n
⊢ coeff ((expand R p : (a : R[X]) → R[X]) f) (p * n) = f.coeff n

Tactic:
rw [mul_comm, coeff_expand_mul hp]

Premises used: Polynomial.coeff_expand_mul, mul_comm
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : Eq (α := R[X]) ((expand R n : (a : R[X]) → R[X]) g : R[X]) ((expand R n : (a : R[X]) → R[X]) g' : R[X])
k : ℕ
rw : coeff ((expand R n : (a : R[X]) → R[X]) g) (k * n) = g'.coeff k
rw₁ : coeff ((expand R n : (a : R[X]) → R[X]) g') (k * n) = g'.coeff k
rw₂ rw₃ : g'.coeff k = g'.coeff k
⊢ g.coeff k = g'.coeff k

Tactic:
rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]

Premises used: Polynomial.coeff_expand_mul
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f g : R[X]
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((expand R p : (a : R[X]) → R[X]) g : R[X]) ↔ f = g

Tactic:
(expand_injective hp).eq_iff

Premises used: Function.Injective.eq_iff, Polynomial.expand_injective
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X]) ↔ f = 0

Tactic:
(expand_injective hp).eq_iff' (map_zero _)

Premises used: map_zero, Function.Injective.eq_iff', Polynomial.expand_injective
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
⊢ Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X]) ↔ f ≠ 0

Tactic:
(expand_eq_zero hp).not

Premises used: Iff.not, Polynomial.expand_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) ↔
    f = (expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)
p₁ : ℕ
rw₁ : f = (C : (a : R) → R[X]) r ↔ f = (expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)
rw₂ rw₃ : f = (C : (a : R) → R[X]) r ↔ f = (C : (a : R) → R[X]) r
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) r : R[X]) ↔
    f = (C : (a : R) → R[X]) r

Tactic:
rw [← expand_C, expand_inj hp, expand_C]

Premises used: Polynomial.expand_C, Polynomial.expand_inj
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
inl : ∀ (hp : p = 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
inr : ∀ (hp : p > 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p

Tactic:
rcases p.eq_zero_or_pos with hp | hp

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
inl : natDegree.{u} (R := R) ((expand R 0 : (a : R[X]) → R[X]) f) = f.natDegree * 0
inl₁ : (eval₂ C (HPow.hPow (α := R[X]) (β := ℕ) X 0) f).natDegree = f.natDegree * 0
inl₂ : (eval₂ C 1 f).natDegree = f.natDegree * 0
inl₃ : (eval₂ C 1 f).natDegree = 0
inl₄ : (eval₂ C ((C : (a : R) → R[X]) 1) f).natDegree = 0
inl₅ : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (eval 1 f)) = 0
inl₆ inl₇ : Eq (α := ℕ) 0 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p

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

Premises used: Polynomial.C_1, Polynomial.eval₂_hom, Polynomial.natDegree_C, pow_zero, MulZeroClass.mul_zero, Polynomial.coe_expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
pos : ∀ (hf : f = 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
neg : ∀ (hf : ¬f = 0), natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
pos : natDegree (R := R) ((expand R p : (a : R[X]) → R[X]) 0) = natDegree.{u} (R := R) 0 * p
pos₁ : natDegree.{u} (R := R) 0 = natDegree.{u} (R := R) 0 * p
pos₂ : 0 = 0 * p
pos₃ pos₄ : Eq (α := ℕ) 0 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p

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

Premises used: MulZeroClass.zero_mul, map_zero, Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])

Tactic:
have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
neg : degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = (↑(f.natDegree * p) : WithBot ℕ)
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p

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

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_inj
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = (↑(f.natDegree * p) : WithBot ℕ)

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

Premises used: Iff.mpr, le_antisymm, Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
neg :
  ∀ (n : ℕ) (hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)),
    Eq.{u + 1} (α := R) (coeff ((expand R p : (a : R[X]) → R[X]) f) n) 0
neg₁ : (↑(f.natDegree * p) : WithBot ℕ) ≤ degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f)
⊢ degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = (↑(f.natDegree * p) : WithBot ℕ)

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

Premises used: Iff.mpr, le_antisymm, Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
neg : (if p ∣ n then f.coeff (n / p) else 0) = 0
⊢ Eq.{u + 1} (α := R) (coeff ((expand R p : (a : R[X]) → R[X]) f) n) 0

Tactic:
rw [coeff_expand hp]

Premises used: Polynomial.coeff_expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
pos : ∀ (hpn : p ∣ n), f.coeff (n / p) = 0
neg : ∀ (hpn : ¬p ∣ n), Eq.{u + 1} (α := R) 0 0
⊢ (if p ∣ n then f.coeff (n / p) else 0) = 0

Tactic:
split_ifs with hpn
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
hpn : p ∣ n
pos : f.natDegree < n / p
⊢ f.coeff (n / p) = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
hpn : p ∣ n
pos : ∀ (hn : n / p ≤ f.natDegree), LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ)
⊢ f.natDegree < n / p

Tactic:
contrapose! hn
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
pos : n ≤ f.natDegree * p
⊢ LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
pos : n / p * p ≤ f.natDegree * p
⊢ n ≤ f.natDegree * p

Tactic:
rw [← Nat.div_mul_cancel hpn]

Premises used: Nat.div_mul_cancel
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ n / p * p ≤ f.natDegree * p

Tactic:
Nat.mul_le_mul_right p hn

Premises used: Nat.mul_le_mul_right
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ n / p * p ≤ f.natDegree * p

Tactic:
exact Nat.mul_le_mul_right p hn

Premises used: Nat.mul_le_mul_right
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
hpn : ¬p ∣ n
⊢ Eq.{u + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ (↑(f.natDegree * p) : WithBot ℕ) ≤ degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f)

Tactic:
le_degree_of_ne_zero ?_

Premises used: Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
neg : Ne.{u + 1} (α := R) (coeff ((expand R p : (a : R[X]) → R[X]) f) (f.natDegree * p)) 0
⊢ (↑(f.natDegree * p) : WithBot ℕ) ≤ degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f)

Tactic:
refine le_degree_of_ne_zero ?_

Premises used: Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
neg : f.leadingCoeff ≠ 0
⊢ Ne.{u + 1} (α := R) (coeff ((expand R p : (a : R[X]) → R[X]) f) (f.natDegree * p)) 0

Tactic:
rw [coeff_expand_mul hp, ← leadingCoeff]

Premises used: Polynomial.leadingCoeff, Polynomial.coeff_expand_mul
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ f.leadingCoeff ≠ 0

Tactic:
mt leadingCoeff_eq_zero.1 hf

Premises used: mt, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ f.leadingCoeff ≠ 0

Tactic:
exact mt leadingCoeff_eq_zero.1 hf

Premises used: mt, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
simp_rw :
  coeff ((expand R p : (a : R[X]) → R[X]) f) (natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f)) =
    f.coeff f.natDegree
simp_rw₁ : coeff ((expand R p : (a : R[X]) → R[X]) f) (f.natDegree * p) = f.coeff f.natDegree
⊢ leadingCoeff ((expand R p : (a : R[X]) → R[X]) f) = f.leadingCoeff

Tactic:
simp_rw [leadingCoeff, natDegree_expand, coeff_expand_mul hp]

Premises used: Polynomial.leadingCoeff, Polynomial.coeff_expand_mul, Polynomial.natDegree_expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ Monic.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) ↔ f.Monic

Tactic:
simp only [Monic, leadingCoeff_expand hp]

Premises used: Polynomial.Monic, Polynomial.leadingCoeff_expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
pos : ∀ (hp : p = 0), map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)
neg : ∀ (hp : ¬p = 0), map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)
⊢ map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : p = 0
⊢ map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
neg :
  ∀ (n : ℕ), (map f ((expand R p : (a : R[X]) → R[X]) q)).coeff n = coeff ((expand S p : (a : S[X]) → S[X]) (map f q)) n
⊢ map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n : ℕ
neg : (f : (a : R) → S) (if p ∣ n then q.coeff (n / p) else 0) = if p ∣ n then (map f q).coeff (n / p) else 0
⊢ (map f ((expand R p : (a : R[X]) → R[X]) q)).coeff n = coeff ((expand S p : (a : S[X]) → S[X]) (map f q)) n

Tactic:
rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]

Premises used: Polynomial.coeff_map, Nat.pos_of_ne_zero, Polynomial.coeff_expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n : ℕ
pos : p ∣ n → (f : (a : R) → S) (q.coeff (n / p)) = (map f q).coeff (n / p)
neg : ¬p ∣ n → Eq.{v + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
⊢ (f : (a : R) → S) (if p ∣ n then q.coeff (n / p) else 0) = if p ∣ n then (map f q).coeff (n / p) else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n : ℕ
h : p ∣ n
⊢ (f : (a : R) → S) (q.coeff (n / p)) = (map f q).coeff (n / p)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n : ℕ
h : ¬p ∣ n
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r a : R
⊢ eval r ((expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) a)) = eval (r ^ p) ((C : (a : R) → R[X]) a)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r : R
n : ℕ
a : R
h :
  eval r
      ((expand R p : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))) =
    eval (r ^ p) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ eval r
      ((expand R p : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) =
    eval (r ^ p) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r : R
refine :
  ∀ (f g : R[X]) (hf : eval r ((expand R p : (a : R[X]) → R[X]) f) = eval (r ^ p) f)
    (hg : eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) g),
    eval r ((expand R p : (a : R[X]) → R[X]) (f + g)) = eval (r ^ p) (f + g)
⊢ eval r ((expand R p : (a : R[X]) → R[X]) P) = eval (r ^ p) P

Tactic:
refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p : (a : R[X]) → R[X]) f) = eval (r ^ p) f
hg : eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) g
rw :
  eval r
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
        ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    eval (r ^ p) (f + g)
rw₁ : eval r ((expand R p : (a : R[X]) → R[X]) f) + eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) (f + g)
rw₂ :
  eval r ((expand R p : (a : R[X]) → R[X]) f) + eval r ((expand R p : (a : R[X]) → R[X]) g) =
    eval (r ^ p) f + eval (r ^ p) g
rw₃ : eval (r ^ p) f + eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) f + eval (r ^ p) g
rw₄ rw₅ : eval (r ^ p) f + eval (r ^ p) g = eval (r ^ p) f + eval (r ^ p) g
⊢ eval r ((expand R p : (a : R[X]) → R[X]) (f + g)) = eval (r ^ p) (f + g)

Tactic:
rw [map_add, eval_add, eval_add, hf, hg]

Premises used: map_add, Polynomial.eval_add