awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
a : R
⊢ Eq.{u_1 + 1} (α := A)
    ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) a) : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) ((C : (a : R) → R[X]) a : R[X]) : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
n : ℕ
a : R
h :
  Eq.{u_1 + 1} (α := A)
    ((aeval r : (a : R[X]) → A)
        ((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)) :
          R[X]) :
      A)
    ((aeval (r ^ p) : (a : R[X]) → A)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
      A)
⊢ Eq.{u_1 + 1} (α := A)
    ((aeval r : (a : R[X]) → A)
        ((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))) :
          R[X]) :
      A)
    ((aeval (r ^ p) : (a : R[X]) → A)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      A)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
refine :
  ∀ (f g : R[X])
    (hf :
      Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
        ((aeval (r ^ p) : (a : R[X]) → A) f : A))
    (hg :
      Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A)
        ((aeval (r ^ p) : (a : R[X]) → A) g : A)),
    Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) (f + g) : R[X]) : A)
      ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
⊢ Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) P : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) P : A)

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
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) f : A)
hg :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) g : A)
rw :
  Eq.{u_1 + 1} (α := A)
    ((aeval r : (a : R[X]) → A)
        (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])) :
      A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
rw₁ :
  HAdd.hAdd (α := A) (β := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
      ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
    (aeval (r ^ p) : (a : R[X]) → A) (f + g)
rw₂ :
  HAdd.hAdd (α := A) (β := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
      ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
    HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A)
rw₃ :
  HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A)
      ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
    HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A)
rw₄ rw₅ :
  HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A) =
    HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A)
⊢ Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) (f + g) : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)

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

Premises used: map_add, Polynomial.aeval_add
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
simp : f.natDegree + 1 ≤ n → 0 = f.coeff (n * p)
⊢ (contract p f).coeff n = f.coeff (n * p)

Tactic:
simp only [contract, coeff_monomial, sum_ite_eq', finsetSum_coeff, mem_range, not_lt,
    ite_eq_left_iff]

Premises used: Finset.sum_ite_eq', ite_eq_left_iff, Polynomial.finsetSum_coeff, Finset.mem_range, Polynomial.coeff_monomial, Polynomial.contract, not_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
apply : f.natDegree < n * p
⊢ 0 = f.coeff (n * p)

Tactic:
apply (coeff_eq_zero_of_natDegree_lt _).symm

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree < f.natDegree + 1

Tactic:
Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree + 1 ≤ n * 1

Tactic:
simpa only [mul_one] using hn

Premises used: mul_one
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
bc : 1 ≤ p
⊢ n * 1 ≤ n * p

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 1 ≤ p

Tactic:
hp.bot_lt

Premises used: Nat.lt, Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 1 ≤ p

Tactic:
exact hp.bot_lt

Premises used: Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
_ : f.natDegree + 1 ≤ n * 1
_₁ : n * 1 ≤ n * p
⊢ f.natDegree < n * p

Tactic:
calc
    f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
    _ ≤ n * 1 := by simpa only [mul_one] using hn
    _ ≤ n * p := by gcongr; exact hp.bot_lt

Premises used: Nat.lt_succ_self, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
hp : p ≠ 0
f : R →+* S
q : R[X]
n : ℕ
⊢ (map f (contract p q)).coeff n = (contract p (map f q)).coeff n

Tactic:
simp only [coeff_map, coeff_contract hp]

Premises used: Polynomial.coeff_map, Polynomial.coeff_contract
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p ≠ 0
a : ∀ (n : ℕ), coeff (contract p ((expand R p : (a : R[X]) → R[X]) f)) n = f.coeff n
⊢ contract p ((expand R p : (a : R[X]) → R[X]) f) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p ≠ 0
n : ℕ
⊢ coeff (contract p ((expand R p : (a : R[X]) → R[X]) f)) n = f.coeff n

Tactic:
simp [coeff_contract hp, coeff_expand hp.bot_lt, Nat.mul_div_cancel _ hp.bot_lt]

Premises used: Nat.mul_div_cancel, Polynomial.coeff_contract, Polynomial.coeff_expand, Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
rw : f.coeff (n * 1) = f.coeff n
rw₁ rw₂ : f.coeff n = f.coeff n
⊢ (contract 1 f).coeff n = f.coeff n

Tactic:
rw [coeff_contract one_ne_zero, mul_one]

Premises used: Polynomial.coeff_contract, mul_one, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
r : R
⊢ Eq.{u + 1} (α := R[X]) (contract p ((C : (a : R) → R[X]) r)) ((C : (a : R) → R[X]) r)

Tactic:
simp [contract]

Premises used: Polynomial.contract
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
a : ∀ (n : ℕ), (contract p (f + g)).coeff n = (contract p f + contract p g).coeff n
⊢ contract p (f + g) = contract p f + contract p g

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a : (contract p (f + g)).coeff n = (contract p f).coeff n + (contract p g).coeff n
a₁ : (f + g).coeff (n * p) = f.coeff (n * p) + g.coeff (n * p)
⊢ (contract p (f + g)).coeff n = (contract p f + contract p g).coeff n

Tactic:
simp_rw [coeff_add, coeff_contract hp, coeff_add]

Premises used: Polynomial.coeff_add, Polynomial.coeff_contract
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
a :
  ∀ (n : ℕ),
    (contract p (HMul.hMul (β := R[X]) f ((expand R p : (a : R[X]) → R[X]) g : R[X]))).coeff n =
      (contract p f * g).coeff n
⊢ contract p (HMul.hMul (β := R[X]) f ((expand R p : (a : R[X]) → R[X]) g : R[X])) = contract p f * g

Tactic:
ext n
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a :
  Eq.{u + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f.coeff (x.1 * p, x.2 * p).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.1 * p, x.2 * p).2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
a₁ :
  Set.InjOn (β := ℕ × ℕ) (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ))
a₂ :
  image (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (@antidiagonal _ Nat.instAddMonoid _ n) ⊆
    @antidiagonal _ Nat.instAddMonoid _ (n * p)
a₃ :
  ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ (n * p),
    x ∉ image (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (@antidiagonal _ Nat.instAddMonoid _ n) →
      f.coeff x.1 * coeff ((expand R p : (a : R[X]) → R[X]) g) x.2 = 0
⊢ (contract p (HMul.hMul (β := R[X]) f ((expand R p : (a : R[X]) → R[X]) g : R[X]))).coeff n =
    (contract p f * g).coeff n

Tactic:
rw [coeff_contract hp, coeff_mul, coeff_mul, ← sum_subset
    (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)), sum_image]

Premises used: Polynomial.coeff_mul, Polynomial.coeff_contract, Finset.sum_subset, Finset.sum_image
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a a₁ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f.coeff (x.1 * p) * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.2 * p))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
a₂ :
  Eq.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff (x.1 * p) * g.coeff x.2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
⊢ Eq.{u + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f.coeff (x.1 * p, x.2 * p).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.1 * p, x.2 * p).2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)

Tactic:
simp_rw [coeff_expand_mul hp.bot_lt, coeff_contract hp]

Premises used: Polynomial.coeff_contract, Polynomial.coeff_expand_mul, Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ))
y : ℕ × ℕ
hy : y ∈ (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ))
eq : Eq (α := ℕ × ℕ) ((fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) x) ((fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) y)
⊢ x = y

Tactic:
simpa only [Prod.ext_iff, Nat.mul_right_cancel_iff hp.bot_lt] using eq

Premises used: Prod.ext_iff, Nat.mul_right_cancel_iff, Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a : ∀ ⦃x : ℕ × ℕ⦄, (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → x.1 + x.2 = n * p
⊢ image (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (@antidiagonal _ Nat.instAddMonoid _ n) ⊆
    @antidiagonal _ Nat.instAddMonoid _ (n * p)

Tactic:
simp_rw [subset_iff, mem_image, mem_antidiagonal]

Premises used: Finset.mem_image, Finset.HasAntidiagonal.mem_antidiagonal, Finset.subset_iff
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
x : ℕ × ℕ
a a₁ : x.1 * p + x.2 * p = (x.1 + x.2) * p
⊢ (x.1 * p, x.2 * p).1 + (x.1 * p, x.2 * p).2 = (x.1 + x.2) * p

Tactic:
simp_rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a :
  ∀ (x : ℕ × ℕ),
    x.1 + x.2 = n * p →
      (¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) →
        f.coeff x.1 * coeff ((expand R p : (a : R[X]) → R[X]) g) x.2 = 0
⊢ ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ (n * p),
    x ∉ image (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (@antidiagonal _ Nat.instAddMonoid _ n) →
      f.coeff x.1 * coeff ((expand R p : (a : R[X]) → R[X]) g) x.2 = 0

Tactic:
simp_rw [mem_image, mem_antidiagonal]

Premises used: Finset.mem_image, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
pos : ∀ (h : p ∣ y), f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
neg : ∀ (h : ¬p ∣ y), f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
⊢ f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0

Tactic:
by_cases h : p ∣ y
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : p ∣ y
⊢ p ∣ x

Tactic:
(Nat.dvd_add_iff_left h).mpr (eq ▸ dvd_mul_left p n)

Premises used: Iff.mpr, Eq.rec, dvd_mul_left, Eq.symm, Nat.dvd_add_iff_left
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : p ∣ y
pos :
  ∀ (x : ℕ) (eq : (p * x, y).1 + (p * x, y).2 = n * p)
    (nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, y)),
    f.coeff (p * x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (p * x, y).2 = 0
⊢ f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0

Tactic:
obtain ⟨x, rfl⟩ : p ∣ x := (Nat.dvd_add_iff_left h).mpr (eq ▸ dvd_mul_left p n)

Premises used: Iff.mpr, Nat.dvd_add_iff_left, rfl
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n y : ℕ
h : p ∣ y
x : ℕ
eq : (p * x, y).1 + (p * x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, y)
pos :
  ∀ (y : ℕ) (eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p)
    (nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)),
    f.coeff (p * x, p * y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (p * x, p * y).2 = 0
⊢ f.coeff (p * x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (p * x, y).2 = 0

Tactic:
obtain ⟨y, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
simp_rw simp_rw₁ : (x * p, y * p) = (p * x, p * y)
⊢ ((x, y).1 * p, (x, y).2 * p) = (p * x, p * y)

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
pos : ((x, y).1 + (x, y).2) * p = n * p
⊢ f.coeff (p * x, p * y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (p * x, p * y).2 = 0

Tactic:
refine (nex ⟨⟨x, y⟩, (Nat.mul_right_cancel_iff hp.bot_lt).mp ?_, by simp_rw [mul_comm]⟩).elim

Premises used: False.elim, Nat.mul_right_cancel_iff, Prod.mk, And.intro, Exists.intro, Iff.mp, Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
pos : ((x, y).1 + (x, y).2) * p = (p * x, p * y).1 + (p * x, p * y).2
pos₁ : p * ((x, y).1 + (x, y).2) = (p * x, p * y).1 + (p * x, p * y).2
pos₂ pos₃ : p * (x, y).1 + p * (x, y).2 = (p * x, p * y).1 + (p * x, p * y).2
⊢ ((x, y).1 + (x, y).2) * p = n * p

Tactic:
rw [← eq, mul_comm, mul_add]

Premises used: mul_comm, mul_add
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
neg : (f.coeff (x, y).1 * if p ∣ (x, y).2 then g.coeff ((x, y).2 / p) else 0) = 0
neg₁ : f.coeff (x, y).1 * 0 = 0
neg₂ neg₃ : Eq.{u + 1} (α := R) 0 0
⊢ f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0

Tactic:
rw [coeff_expand hp.bot_lt, if_neg h, mul_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.coeff_expand, if_neg, Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
h : IsCoprime (R := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((expand R p : (a : R[X]) → R[X]) g : R[X])
a b : R[X]
eq :
  HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X]) +
      HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X]) =
    1
simp_rw :
  contract p (HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X])) +
      contract p (HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    1
simp_rw₁ :
  contract p
      (HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X]) +
        HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    1
simp_rw₂ : Eq.{u + 1} (α := R[X]) (contract p 1) 1
simp_rw₃ : Eq.{u + 1} (α := R[X]) (contract p ((C : (a : R) → R[X]) 1)) ((C : (a : R) → R[X]) 1)
⊢ contract p a * f + contract p b * g = 1

Tactic:
simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]

Premises used: Polynomial.C_1, Polynomial.contract_add, Polynomial.contract_C, Polynomial.contract_mul_expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
a : ∀ (n : ℕ), coeff ((expand R p : (a : R[X]) → R[X]) (contract p f)) n = f.coeff n
⊢ (expand R p : (a : R[X]) → R[X]) (contract p f) = f

Tactic:
ext n
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
a : (if p ∣ n then f.coeff (n / p * p) else 0) = f.coeff n
⊢ coeff ((expand R p : (a : R[X]) → R[X]) (contract p f)) n = f.coeff n

Tactic:
rw [coeff_expand hp.bot_lt, coeff_contract hp]

Premises used: Polynomial.coeff_contract, Polynomial.coeff_expand, Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
pos : ∀ (h : p ∣ n), f.coeff (n / p * p) = f.coeff n
neg : ∀ (h : ¬p ∣ n), 0 = f.coeff n
⊢ (if p ∣ n then f.coeff (n / p * p) else 0) = f.coeff n

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : p ∣ n
pos pos₁ : f.coeff n = f.coeff n
⊢ f.coeff (n / p * p) = f.coeff n

Tactic:
rw [Nat.div_mul_cancel h]

Premises used: Nat.div_mul_cancel
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
neg : ∀ (h : ¬p ∣ 0), 0 = f.coeff 0
neg₁ : ∀ (n : ℕ) (h : ¬p ∣ n + 1), 0 = f.coeff (n + 1)
⊢ 0 = f.coeff n

Tactic:
rcases n with - | n
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
h : ¬p ∣ 0
⊢ 0 = f.coeff 0

Tactic:
absurd (dvd_zero p) h

Premises used: dvd_zero, absurd
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
h : ¬p ∣ 0
⊢ 0 = f.coeff 0

Tactic:
exact absurd (dvd_zero p) h

Premises used: dvd_zero, absurd
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
⊢ coeff ((derivative : (a : R[X]) → R[X]) f) n = f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
have := coeff_derivative f n
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : coeff ((derivative : (a : R[X]) → R[X]) f) n = f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
⊢ f.coeff (n + 1) = 0 ∨ HAdd.hAdd (α := R) (↑n : R) 1 = 0

Tactic:
rw [hf, coeff_zero, zero_eq_mul] at this

Premises used: zero_eq_mul, Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : f.coeff (n + 1) = 0 ∨ HAdd.hAdd (α := R) (↑n : R) 1 = 0
neg : ∀ (h' : f.coeff (n + 1) = 0), 0 = f.coeff (n + 1)
neg₁ : HAdd.hAdd (α := R) (↑n : R) 1 = 0 → 0 = f.coeff (n + 1)
⊢ 0 = f.coeff (n + 1)

Tactic:
rcases this with h' | _
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : f.coeff (n + 1) = 0
neg neg₁ : Eq.{u + 1} (α := R) 0 0
⊢ 0 = f.coeff (n + 1)

Tactic:
rw [h']
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : HAdd.hAdd (α := R) (↑n : R) 1 = 0
⊢ p ∣ n.succ

Tactic:
rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h'

Premises used: Nat.cast_succ, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : p ∣ n.succ
⊢ 0 = f.coeff (n + 1)

Tactic:
absurd h' h

Premises used: absurd
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : p ∣ n.succ
⊢ 0 = f.coeff (n + 1)

Tactic:
exact absurd h' h

Premises used: absurd