awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
q : R[X]
n : ℕ
p : R[ℕ]
rcases :
  ∀ (q : R[ℕ]),
    ({ toFinsupp := p : R[X] } * { toFinsupp := q : R[X] }).coeff n =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        { toFinsupp := p : R[X] }.coeff x.1 * { toFinsupp := q : R[X] }.coeff x.2
⊢ ({ toFinsupp := p : R[X] } * q).coeff n =
    ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, { toFinsupp := p : R[X] }.coeff x.1 * q.coeff x.2

Tactic:
rcases q with ⟨q⟩
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[ℕ]
simp_rw :
  Eq (α := R) ((p * q : (a : ℕ) → R) n : R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((p : (a : ℕ) → R) x.1 : R) ((q : (a : ℕ) → R) x.2 : R) :
      R)
⊢ ({ toFinsupp := p : R[X] } * { toFinsupp := q : R[X] }).coeff n =
    ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      { toFinsupp := p : R[X] }.coeff x.1 * { toFinsupp := q : R[X] }.coeff x.2

Tactic:
simp_rw [← ofFinsupp_mul, coeff]

Premises used: Polynomial.coeff, Polynomial.ofFinsupp_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[ℕ]
⊢ Eq (α := R) ((p * q : (a : ℕ) → R) n : R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((p : (a : ℕ) → R) x.1 : R) ((q : (a : ℕ) → R) x.2 : R) :
      R)

Tactic:
AddMonoidAlgebra.mul_apply_antidiagonal p q n _ Finset.mem_antidiagonal

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, AddMonoidAlgebra.mul_apply_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[ℕ]
⊢ Eq (α := R) ((p * q : (a : ℕ) → R) n : R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((p : (a : ℕ) → R) x.1 : R) ((q : (a : ℕ) → R) x.2 : R) :
      R)

Tactic:
exact AddMonoidAlgebra.mul_apply_antidiagonal p q n _ Finset.mem_antidiagonal

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, AddMonoidAlgebra.mul_apply_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (p * q).coeff 0 = p.coeff 0 * q.coeff 0

Tactic:
simp [coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p q : R[X]
rw :
  ∑ x ∈ map { toFun := fun (i : ℕ) ↦ (i, 1 - i), inj' := ⋯ } (range (HAdd.hAdd (α := ℕ) 1 1)),
      p.coeff x.1 * q.coeff x.2 =
    p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0
⊢ (p * q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0

Tactic:
rw [coeff_mul, Nat.antidiagonal_eq_map]

Premises used: Finset.Nat.antidiagonal_eq_map, Polynomial.coeff_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ ∑ x ∈ map { toFun := fun (i : ℕ) ↦ (i, 1 - i), inj' := ⋯ } (range (HAdd.hAdd (α := ℕ) 1 1)),
      p.coeff x.1 * q.coeff x.2 =
    p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0

Tactic:
simp [sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
x : R
⊢ (constantCoeff : (a : R[X]) → R) ((C : (a : R) → R[X]) x : R[X]) = x

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
x : R
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) x : R[X]) ↔ IsUnit x

Tactic:
⟨fun h => (congr_arg IsUnit coeff_C_zero).mp (h.map <| @constantCoeff R _), fun h => h.map C⟩

Premises used: Polynomial.C, IsUnit, Eq.mp, congr_arg, Polynomial.constantCoeff, Iff.intro, IsUnit.map, Polynomial.coeff_C_zero
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (p * X).coeff 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (X * p).coeff 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
x : R
k n : ℕ
rw : (if k = n then x else 0) = if n = k then x else 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n = if n = k then x else 0

Tactic:
rw [C_mul_X_pow_eq_monomial, coeff_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
x : R
k n : ℕ
⊢ (if k = n then x else 0) = if n = k then x else 0

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
x : R
n : ℕ
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1)).coeff n =
    if n = 1 then x else 0
rw₁ rw₂ : (if n = 1 then x else 0) = if n = 1 then x else 0
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) x : R[X]) X).coeff n = if n = 1 then x else 0

Tactic:
rw [← pow_one X, coeff_C_mul_X_pow]

Premises used: pow_one, Polynomial.coeff_C_mul_X_pow, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
p : R[X]
rcases :
  ∀ (p : R[ℕ]),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) { toFinsupp := p : R[X] }).coeff n =
      a * { toFinsupp := p : R[X] }.coeff n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff n = a * p.coeff n

Tactic:
rcases p with ⟨p⟩
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
p : R[ℕ]
simp_rw : (AddMonoidAlgebra.single 0 a * p : (a : ℕ) → R) n = HMul.hMul (β := R) a ((p : (a : ℕ) → R) n : R)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) { toFinsupp := p : R[X] }).coeff n =
    a * { toFinsupp := p : R[X] }.coeff n

Tactic:
simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]

Premises used: Polynomial.ofFinsupp_single, Polynomial.coeff, Polynomial.ofFinsupp_mul, Polynomial.monomial_zero_left
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
p : R[ℕ]
⊢ (AddMonoidAlgebra.single 0 a * p : (a : ℕ) → R) n = HMul.hMul (β := R) a ((p : (a : ℕ) → R) n : R)

Tactic:
AddMonoidAlgebra.single_zero_mul_apply p a n

Premises used: AddMonoidAlgebra.single_zero_mul_apply
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
p : R[ℕ]
⊢ (AddMonoidAlgebra.single 0 a * p : (a : ℕ) → R) n = HMul.hMul (β := R) a ((p : (a : ℕ) → R) n : R)

Tactic:
exact AddMonoidAlgebra.single_zero_mul_apply p a n

Premises used: AddMonoidAlgebra.single_zero_mul_apply
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
a : R
f : R[X]
a₁ : ∀ (n : ℕ), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f).coeff n = (a • f).coeff n
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f = a • f

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
a : R
f : R[X]
n : ℕ
a₁ : a * f.coeff n = (a • f).coeff n
a₂ : a * f.coeff n = a • f.coeff n
a₃ a₄ : a * f.coeff n = a * f.coeff n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f).coeff n = (a • f).coeff n

Tactic:
rw [coeff_C_mul, coeff_smul, smul_eq_mul]

Premises used: Polynomial.coeff_C_mul, Polynomial.coeff_smul, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
rcases :
  ∀ (p : R[ℕ]),
    (HMul.hMul (β := R[X]) { toFinsupp := p : R[X] } ((C : (a : R) → R[X]) a : R[X])).coeff n =
      { toFinsupp := p : R[X] }.coeff n * a
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff n = p.coeff n * a

Tactic:
rcases p with ⟨p⟩
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
p : R[ℕ]
simp_rw : (p * AddMonoidAlgebra.single 0 a : (a : ℕ) → R) n = HMul.hMul (α := R) ((p : (a : ℕ) → R) n : R) a
⊢ (HMul.hMul (β := R[X]) { toFinsupp := p : R[X] } ((C : (a : R) → R[X]) a : R[X])).coeff n =
    { toFinsupp := p : R[X] }.coeff n * a

Tactic:
simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]

Premises used: Polynomial.ofFinsupp_single, Polynomial.coeff, Polynomial.ofFinsupp_mul, Polynomial.monomial_zero_left
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
p : R[ℕ]
⊢ (p * AddMonoidAlgebra.single 0 a : (a : ℕ) → R) n = HMul.hMul (α := R) ((p : (a : ℕ) → R) n : R) a

Tactic:
AddMonoidAlgebra.mul_single_zero_apply p a n

Premises used: AddMonoidAlgebra.mul_single_zero_apply
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
p : R[ℕ]
⊢ (p * AddMonoidAlgebra.single 0 a : (a : ℕ) → R) n = HMul.hMul (α := R) ((p : (a : ℕ) → R) n : R) a

Tactic:
exact AddMonoidAlgebra.mul_single_zero_apply p a n

Premises used: AddMonoidAlgebra.mul_single_zero_apply
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
a k : ℕ
⊢ (p * (↑a : R[X])).coeff k = p.coeff k * (↑a : R)

Tactic:
coeff_mul_C _ _ _

Premises used: Polynomial.coeff_mul_C, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
a k : ℕ
⊢ ((↑a : R[X]) * p).coeff k = (↑a : R) * p.coeff k

Tactic:
coeff_C_mul _

Premises used: Polynomial.coeff_C_mul, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
a k : ℕ
inst_1 : a.AtLeastTwo
⊢ (p * OfNat.ofNat a).coeff k = p.coeff k * OfNat.ofNat a

Tactic:
coeff_mul_C _ _ _

Premises used: Polynomial.coeff_mul_C, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
a k : ℕ
inst_1 : a.AtLeastTwo
⊢ (OfNat.ofNat a * p).coeff k = OfNat.ofNat a * p.coeff k

Tactic:
coeff_C_mul _

Premises used: Polynomial.coeff_C_mul, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
S : Type v
inst : Ring S
p : S[X]
a : ℤ
k : ℕ
⊢ (p * (↑a : S[X])).coeff k = p.coeff k * (↑a : S)

Tactic:
coeff_mul_C _ _ _

Premises used: Polynomial.coeff_mul_C, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
S : Type v
inst : Ring S
p : S[X]
a : ℤ
k : ℕ
⊢ ((↑a : S[X]) * p).coeff k = (↑a : S) * p.coeff k

Tactic:
coeff_C_mul _

Premises used: Polynomial.coeff_C_mul, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
k n : ℕ
⊢ (HPow.hPow (α := R[X]) X k).coeff n = if n = k then 1 else 0

Tactic:
simp only [one_mul, map_one, ← coeff_C_mul_X_pow]

Premises used: map_one, Polynomial.coeff_C_mul_X_pow, one_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).coeff n = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
apply :
  {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support =
    {k, m}

Tactic:
apply subset_antisymm (support_binomial' k m x y)

Premises used: Polynomial.support_binomial', subset_antisymm
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
apply :
  {k, m, n} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support =
    {k, m, n}

Tactic:
apply subset_antisymm (support_trinomial' k m n x y z)

Premises used: Polynomial.support_trinomial', subset_antisymm
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
rw : card (α := ℕ) {k, m} = 2
rw₁ : card (α := ℕ) {m} + 1 = 2
rw₂ rw₃ : HAdd.hAdd (α := ℕ) 1 1 = 2
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support =
    2

Tactic:
rw [support_binomial h hx hy, card_insert_of_notMem (mt mem_singleton.mp h), card_singleton]

Premises used: Finset.mem_singleton, mt, Finset.card_insert_of_notMem, Iff.mp, Polynomial.support_binomial, Finset.card_singleton
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw : card (α := ℕ) {k, m, n} = 3
rw₁ : card (α := ℕ) {m, n} + 1 = 3
rw₂ : card (α := ℕ) {n} + 1 + 1 = 3
rw₃ rw₄ : HAdd.hAdd (α := ℕ) 1 1 + 1 = 3
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support =
    3

Tactic:
rw [support_trinomial hkm hmn hx hy hz,
    card_insert_of_notMem
      (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
    card_insert_of_notMem (mt mem_singleton.mp hmn.ne), card_singleton]

Premises used: Finset.mem_singleton, Polynomial.support_trinomial, mt, Finset.mem_insert, not_or_intro, Finset.card_insert_of_notMem, Iff.mp, LT.lt.trans, LT.lt.ne, Finset.card_singleton
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h₀ :
  ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n),
    b ≠ (d, n) → p.coeff b.1 * (HPow.hPow (α := R[X]) X n).coeff b.2 = 0
h₁ :
  (d, n) ∉ @antidiagonal _ Nat.instAddMonoid _ (d + n) →
    p.coeff (d, n).1 * (HPow.hPow (α := R[X]) X n).coeff (d, n).2 = 0
⊢ (p * HPow.hPow (α := R[X]) X n).coeff (d + n) = p.coeff d

Tactic:
rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]

Premises used: Polynomial.coeff_X_pow, Polynomial.coeff_mul, Prod.mk, if_pos, Finset.sum_eq_single, mul_one, rfl
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n)
h2 : (i, j) ≠ (d, n)
h₀ : ¬(i, j).2 = n
⊢ p.coeff (i, j).1 * (HPow.hPow (α := R[X]) X n).coeff (i, j).2 = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Premises used: Polynomial.coeff_X_pow, MulZeroClass.mul_zero, if_neg
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).2 = n

Tactic:
grind [mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ @antidiagonal _ Nat.instAddMonoid _ (d + n) →
    p.coeff (d, n).1 * (HPow.hPow (α := R[X]) X n).coeff (d, n).2 = 0

Tactic:
grind [mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
rw : (p * HPow.hPow (α := R[X]) X n).coeff (d + n) = p.coeff d
rw₁ rw₂ : p.coeff d = p.coeff d
⊢ (HPow.hPow (α := R[X]) X n * p).coeff (d + n) = p.coeff d

Tactic:
rw [(commute_X_pow p n).eq, coeff_mul_X_pow]

Premises used: Polynomial.coeff_mul_X_pow, Polynomial.commute_X_pow, Commute.eq
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
pos : ∀ (h : n ≤ d), (p * HPow.hPow (α := R[X]) X n).coeff d = p.coeff (d - n)
neg : ∀ (h : ¬n ≤ d), (p * HPow.hPow (α := R[X]) X n).coeff d = 0
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = if n ≤ d then p.coeff (d - n) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
pos : (p * HPow.hPow (α := R[X]) X n).coeff (d - n + n) = p.coeff (d - n + n - n)
pos₁ : p.coeff (d - n) = p.coeff (d - n + n - n)
pos₂ pos₃ : p.coeff (d - n) = p.coeff (d - n)
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = p.coeff (d - n)

Tactic:
rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]

Premises used: Polynomial.coeff_mul_X_pow, tsub_add_cancel_of_le, add_tsub_cancel_right
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = 0

Tactic:
(coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Premises used: Finset.sum_eq_zero, Polynomial.coeff_mul, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
neg :
  ∀ (x : ℕ × ℕ) (hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d),
    p.coeff x.1 * (HPow.hPow (α := R[X]) X n).coeff x.2 = 0
⊢ (p * HPow.hPow (α := R[X]) X n).coeff d = 0

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Premises used: Finset.sum_eq_zero, Polynomial.coeff_mul, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
neg : ¬x.2 = n
⊢ p.coeff x.1 * (HPow.hPow (α := R[X]) X n).coeff x.2 = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Premises used: Polynomial.coeff_X_pow, MulZeroClass.mul_zero, if_neg
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
⊢ ¬x.2 = n

Tactic:
((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne

Premises used: not_le, le_of_add_le_right, Eq.le, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
⊢ ¬x.2 = n

Tactic:
exact ((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne

Premises used: not_le, le_of_add_le_right, Eq.le, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
rw : (p * HPow.hPow (α := R[X]) X n).coeff d = if n ≤ d then p.coeff (d - n) else 0
rw₁ rw₂ : (if n ≤ d then p.coeff (d - n) else 0) = if n ≤ d then p.coeff (d - n) else 0
⊢ (HPow.hPow (α := R[X]) X n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0

Tactic:
rw [(commute_X_pow p n).eq, coeff_mul_X_pow']

Premises used: Polynomial.coeff_mul_X_pow', Polynomial.commute_X_pow, Commute.eq
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p * X).coeff (n + 1) = p.coeff n

Tactic:
simpa only [pow_one] using coeff_mul_X_pow p 1 n

Premises used: Polynomial.coeff_mul_X_pow, pow_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw : (p * X).coeff (n + 1) = p.coeff n
rw₁ rw₂ : p.coeff n = p.coeff n
⊢ (X * p).coeff (n + 1) = p.coeff n

Tactic:
rw [(commute_X p).eq, coeff_mul_X]

Premises used: Polynomial.coeff_mul_X, Polynomial.commute_X, Commute.eq
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).coeff (d + n) = p.coeff d * r
rw₁ :
  (p * HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
rw₂ :
  (HMul.hMul (β := R[X]) (p * HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r
rw₃ : (p * HPow.hPow (α := R[X]) X n).coeff (d + n) * r = p.coeff d * r
rw₄ rw₅ : p.coeff d * r = p.coeff d * r
⊢ (HMul.hMul (β := R[X]) p ((monomial n : (a : R) → R[X]) r : R[X])).coeff (d + n) = p.coeff d * r

Tactic:
rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]

Premises used: Polynomial.coeff_mul_X_pow, mul_assoc, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.coeff_mul_C, Polynomial.X_pow_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n d : ℕ
r : R
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * p).coeff (d + n) = r * p.coeff d
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * p)).coeff (d + n) = r * p.coeff d
rw₂ : r * (HPow.hPow (α := R[X]) X n * p).coeff (d + n) = r * p.coeff d
rw₃ : r * (p * HPow.hPow (α := R[X]) X n).coeff (d + n) = r * p.coeff d
rw₄ rw₅ : r * p.coeff d = r * p.coeff d
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) p).coeff (d + n) = r * p.coeff d

Tactic:
rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]

Premises used: Polynomial.coeff_mul_X_pow, mul_assoc, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.coeff_C_mul, Polynomial.X_pow_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
d : ℕ
r : R
⊢ (HMul.hMul (β := R[X]) p ((monomial 0 : (a : R) → R[X]) r : R[X])).coeff d = p.coeff d * r

Tactic:
coeff_mul_monomial p 0 d r

Premises used: Polynomial.coeff_mul_monomial, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
d : ℕ
r : R
⊢ (HMul.hMul (α := R[X]) ((monomial 0 : (a : R) → R[X]) r : R[X]) p).coeff d = r * p.coeff d

Tactic:
coeff_monomial_mul p 0 d r

Premises used: OfNat.ofNat, Polynomial.coeff_monomial_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
H : p * HPow.hPow (α := R[X]) X n = 0
⊢ p = 0

Tactic:
ext fun k => (coeff_mul_X_pow p n k).symm.trans <| ext_iff.1 H (k + n)

Premises used: Polynomial.ext, Polynomial.coeff_mul_X_pow, Polynomial.ext_iff, HAdd.hAdd, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
suffices : IsLeftRegular (HPow.hPow (α := R[X]) X n)
⊢ IsRegular (HPow.hPow (α := R[X]) X n)

Tactic:
suffices IsLeftRegular (X ^ n : R[X]) from
    ⟨this, this.right_of_commute (fun p => commute_X_pow p n)⟩
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
P Q : R[X]
X : ∀ (hPQ : HPow.hPow (α := R[X]) Polynomial.X n * P = HPow.hPow (α := R[X]) Polynomial.X n * Q), P = Q
⊢ Eq.{u + 1} (α := R[X]) ((fun (x : R[X]) ↦ HPow.hPow (α := R[X]) Polynomial.X n * x) P)
      ((fun (x : R[X]) ↦ HPow.hPow (α := R[X]) Polynomial.X n * x) Q) →
    P = Q

Tactic:
(hPQ : X ^ n * P = X ^ n * Q)
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
P Q : R[X]
hPQ : HPow.hPow (α := R[X]) X n * P = HPow.hPow (α := R[X]) X n * Q
a : ∀ (i : ℕ), P.coeff i = Q.coeff i
⊢ P = Q

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
P Q : R[X]
hPQ : HPow.hPow (α := R[X]) X n * P = HPow.hPow (α := R[X]) X n * Q
i : ℕ
a : (HPow.hPow (α := R[X]) X n * P).coeff (i + n) = Q.coeff i
a₁ : (HPow.hPow (α := R[X]) X n * Q).coeff (i + n) = Q.coeff i
a₂ a₃ : Q.coeff i = Q.coeff i
⊢ P.coeff i = Q.coeff i

Tactic:
rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]

Premises used: Polynomial.coeff_X_pow_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
⊢ IsRegular.{u} (R := R[X]) X

Tactic:
pow_one (X : R[X]) ▸ isRegular_X_pow 1

Premises used: Eq.rec, Polynomial.isRegular_X_pow, pow_one, OfNat.ofNat, Polynomial.X