awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : p = 0
h₁ : (p.cancelLeads q).natDegree = 0
⊢ (p.cancelLeads q).natDegree < q.natDegree

Tactic:
convert! hq
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : p = 0
⊢ (p.cancelLeads q).natDegree = 0

Tactic:
simp [hp, cancelLeads]

Premises used: Polynomial.cancelLeads
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
neg :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree
⊢ (p.cancelLeads q).natDegree < q.natDegree

Tactic:
rw [cancelLeads, sub_eq_add_neg, tsub_eq_zero_iff_le.mpr h, pow_zero, mul_one]

Premises used: Iff.mpr, Polynomial.cancelLeads, sub_eq_add_neg, tsub_eq_zero_iff_le, pow_zero, mul_one
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
pos :
  ∀
    (h0 :
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
              p) =
        0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
              p)).natDegree <
      q.natDegree
neg :
  ∀
    (h0 :
      ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
            -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
                p) =
          0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
              p)).natDegree <
      q.natDegree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree

Tactic:
by_cases h0 :
    C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0

Premises used: Polynomial.C, HMul.hMul, HSub.hSub, Polynomial.leadingCoeff, HPow.hPow, Polynomial.natDegree, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
      -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
          p) =
    0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    0

Tactic:
simp only [h0, natDegree_zero]

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
      -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
          p) =
    0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree

Tactic:
exact (le_of_eq (by simp only [h0, natDegree_zero])).trans_lt hq

Premises used: le_of_eq, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
neg :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree ≤
    q.natDegree
neg₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree ≠
    q.natDegree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree <
    q.natDegree

Tactic:
apply lt_of_le_of_ne

Premises used: lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
neg : q.natDegree - p.natDegree + p.natDegree ≤ q.natDegree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree ≤
    q.natDegree

Tactic:
compute_degree!
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
neg : q.natDegree ≤ q.natDegree
neg₁ : p.natDegree ≤ q.natDegree
neg₂ : q.natDegree ≤ q.natDegree
neg₃ neg₄ neg₅ : p.natDegree ≤ q.natDegree
⊢ q.natDegree - p.natDegree + p.natDegree ≤ q.natDegree

Tactic:
rwa [Nat.sub_add_cancel]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
neg :
  ∀
    (h0 :
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
            -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
                p)).natDegree =
        q.natDegree),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p) =
      0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree ≠
    q.natDegree

Tactic:
contrapose h0
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
neg :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (p * HPow.hPow (α := R[X]) X (p.natDegree + (q.natDegree - p.natDegree) - p.natDegree))).coeff
      (p.natDegree + (q.natDegree - p.natDegree)) =
    0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
      -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
          p) =
    0

Tactic:
rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h,
      add_comm _ p.natDegree]

Premises used: mul_assoc, tsub_add_cancel_of_le, Polynomial.leadingCoeff, add_comm, Polynomial.natDegree, Polynomial.leadingCoeff_eq_zero, Polynomial.X_pow_mul
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
neg : p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
          -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (p * HPow.hPow (α := R[X]) X (p.natDegree + (q.natDegree - p.natDegree) - p.natDegree))).coeff
      (p.natDegree + (q.natDegree - p.natDegree)) =
    0

Tactic:
simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add]

Premises used: Polynomial.coeff_mul_X_pow, Polynomial.coeff_C_mul, add_tsub_cancel_left, Polynomial.coeff_add, Polynomial.coeff_neg
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (q.natDegree - p.natDegree)) *
            p)).natDegree =
    q.natDegree
neg : p.leadingCoeff * q.coeff (q.natDegree - p.natDegree + p.natDegree) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₁ : p.leadingCoeff * q.coeff q.natDegree + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₂ : p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.coeff p.natDegree) = 0
neg₃ : p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0
neg₄ : q.leadingCoeff * p.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0
neg₅ neg₆ : Eq.{u_1 + 1} (α := R) 0 0
⊢ p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0

Tactic:
rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]

Premises used: add_neg_cancel, tsub_add_cancel_of_le, Polynomial.leadingCoeff, add_comm, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : CommRing R
p q r : R[X]
pq : p ∣ q
pr : p ∣ r
⊢ p ∣ q.cancelLeads r

Tactic:
dvd_sub (pr.trans (Dvd.intro_left _ rfl)) (pq.trans (Dvd.intro_left _ rfl))

Premises used: Polynomial.cancelLeads, Dvd.intro_left, dvd_sub, rfl, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
⊢ (p.cancelLeads q).natDegree < q.natDegree

Tactic:
natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm (mul_comm _ _) h hq

Premises used: mul_comm, Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm
-- Module: Mathlib.Algebra.Polynomial.Cardinal
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
rw : max (#R) (lift.{u, 0} #ℕ) = max #R ℵ₀
⊢ #(AddMonoidAlgebra R ℕ) = max #R ℵ₀

Tactic:
rw [AddMonoidAlgebra, mk_finsupp_lift_of_infinite, lift_uzero, max_comm]

Premises used: Cardinal.mk_finsupp_lift_of_infinite, Cardinal.lift_uzero, AddMonoidAlgebra, max_comm
-- Module: Mathlib.Algebra.Polynomial.Cardinal
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ max (#R) (lift.{u, 0} #ℕ) = max #R ℵ₀

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Cardinal
Goal:
R : Type u
inst : Semiring R
inl : Subsingleton R → #R[X] ≤ max #R ℵ₀
inr : Nontrivial R → #R[X] ≤ max #R ℵ₀
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Polynomial.Cardinal
Goal:
R : Type u
inst : Semiring R
h : Subsingleton R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
(mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)

Premises used: Eq.trans_le, le_max_of_le_right, Cardinal.mk_eq_one, Cardinal.one_le_aleph0
-- Module: Mathlib.Algebra.Polynomial.Cardinal
Goal:
R : Type u
inst : Semiring R
h : Subsingleton R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)

Premises used: Eq.trans_le, le_max_of_le_right, Cardinal.mk_eq_one, Cardinal.one_le_aleph0
-- Module: Mathlib.Algebra.Polynomial.Cardinal
Goal:
R : Type u
inst : Semiring R
h : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
cardinalMk_eq_max.le

Premises used: Eq.le, Polynomial.cardinalMk_eq_max
-- Module: Mathlib.Algebra.Polynomial.Cardinal
Goal:
R : Type u
inst : Semiring R
h : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
exact cardinalMk_eq_max.le

Premises used: Eq.le, Polynomial.cardinalMk_eq_max
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rcases :
  ∀ (toFinsupp : R[ℕ]),
    ({ toFinsupp := toFinsupp : R[X] } + q).coeff n = { toFinsupp := toFinsupp : R[X] }.coeff n + q.coeff n
⊢ (p + q).coeff n = p.coeff n + q.coeff n

Tactic:
rcases p with ⟨⟩
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
q : R[X]
n : ℕ
toFinsupp : R[ℕ]
rcases :
  ∀ (toFinsupp_1 : R[ℕ]),
    ({ toFinsupp := toFinsupp : R[X] } + { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
      { toFinsupp := toFinsupp : R[X] }.coeff n + { toFinsupp := toFinsupp_1 : R[X] }.coeff n
⊢ ({ toFinsupp := toFinsupp : R[X] } + q).coeff n = { toFinsupp := toFinsupp : R[X] }.coeff n + q.coeff n

Tactic:
rcases q with ⟨⟩
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
simp_rw :
  (toFinsupp + toFinsupp_1 : (a : ℕ) → R) n =
    HAdd.hAdd (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R)
⊢ ({ toFinsupp := toFinsupp : R[X] } + { toFinsupp := toFinsupp_1 : R[X] }).coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n + { toFinsupp := toFinsupp_1 : R[X] }.coeff n

Tactic:
simp_rw [← ofFinsupp_add, coeff]

Premises used: Polynomial.ofFinsupp_add, Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
⊢ (toFinsupp + toFinsupp_1 : (a : ℕ) → R) n =
    HAdd.hAdd (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R)

Tactic:
Finsupp.add_apply _ _ _

Premises used: Finsupp.add_apply
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
⊢ (toFinsupp + toFinsupp_1 : (a : ℕ) → R) n =
    HAdd.hAdd (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R)

Tactic:
exact Finsupp.add_apply _ _ _

Premises used: Finsupp.add_apply
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
r : S
p : R[X]
n : ℕ
⊢ (r • p).coeff n = r • p.coeff n

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : i ∈ (r • p).support
rw : ∀ (hi : (r • p).coeff i ≠ 0), p.coeff i ≠ 0
⊢ i ∈ p.support

Tactic:
rw [mem_support_iff] at hi ⊢

Premises used: Polynomial.mem_support_iff
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : (r • p).coeff i ≠ 0
contrapose : ∀ (hi : p.coeff i = 0), (r • p).coeff i = 0
⊢ p.coeff i ≠ 0

Tactic:
contrapose hi
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : p.coeff i = 0
⊢ (r • p).coeff i = 0

Tactic:
simp [hi]
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p q : R[X]
rw : #(p * q).toFinsupp.support = #(p.toFinsupp * q.toFinsupp).support
rw₁ rw₂ : #(p.toFinsupp * q.toFinsupp).support = #(p.toFinsupp * q.toFinsupp).support
⊢ #(p * q).support = #(p.toFinsupp * q.toFinsupp).support

Tactic:
rw [← support_toFinsupp, toFinsupp_mul]

Premises used: Polynomial.toFinsupp_mul, Polynomial.support_toFinsupp
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ #(p.toFinsupp * q.toFinsupp).support ≤ #(p.toFinsupp.support + q.toFinsupp.support)

Tactic:
Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp)

Premises used: Polynomial.toFinsupp, Finset.card_le_card, AddMonoidAlgebra.support_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ #(p.toFinsupp.support + q.toFinsupp.support) ≤ #p.support * #q.support

Tactic:
Finset.card_image₂_le ..

Premises used: Finset.card_image₂_le, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p q : R[X]
calc : #(p * q).support = #(p.toFinsupp * q.toFinsupp).support
⊢ #(p * q).support ≤ #p.support * #q.support

Tactic:
calc #(p * q).support
    _ = #(p.toFinsupp * q.toFinsupp).support := by rw [← support_toFinsupp, toFinsupp_mul]
    _ ≤ #(p.toFinsupp.support + q.toFinsupp.support) :=
      Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp)
    _ ≤ #p.support * #q.support := Finset.card_image₂_le ..

Premises used: Polynomial.toFinsupp, HMul.hMul, Finset.card_image₂_le, Finset.card_le_card, Finsupp.support, AddMonoidAlgebra.support_mul, HAdd.hAdd, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R_1 : Type u
S : Type v
a b : R_1
n m : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : AddCommMonoid M
inst_4 : Module R A
inst_5 : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
rw :
  ∑ n ∈ p.support, (f n : (a : A) → M) ((c • p).coeff n) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) c : R)
      (p.sum fun (x1 : ℕ) (x2 : A) ↦ (f x1 : (a : A) → M) x2)
⊢ ((c • p).sum fun (x1 : ℕ) (x2 : A) ↦ (f x1 : (a : A) → M) x2) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) c : R)
      (p.sum fun (x1 : ℕ) (x2 : A) ↦ (f x1 : (a : A) → M) x2)

Tactic:
rw [sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)]

Premises used: LinearMap.map_zero, Polynomial.sum_eq_of_subset, Polynomial.support_smul, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R_1 : Type u
S : Type v
a b : R_1
n m : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : AddCommMonoid M
inst_4 : Module R A
inst_5 : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ ∑ n ∈ p.support, (f n : (a : A) → M) ((c • p).coeff n) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) c : R)
      (p.sum fun (x1 : ℕ) (x2 : A) ↦ (f x1 : (a : A) → M) x2)

Tactic:
simp only [sum_def, Finset.smul_sum, coeff_smul, map_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, Polynomial.coeff_smul, Polynomial.sum_def, Finset.smul_sum, map_smul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
n : ℕ
f : R[X]
⊢ (lcoeff R n : (a : R[X]) → R) f = f.coeff n

Tactic:
rfl

Premises used: Polynomial.coeff, rfl
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s : Finset ι
f : ι → R[X]
n : ℕ
⊢ Eq.{u + 1} (α := R) (coeff (∑ b ∈ s, f b) n) (∑ b ∈ s, (f b).coeff n)

Tactic:
map_sum (lcoeff R n) _ _

Premises used: map_sum, Polynomial.coeff, Polynomial.lcoeff
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
l : List R[X]
n : ℕ
⊢ l.sum.coeff n = List.sum (List.map (⇑(lcoeff R n) : (a : R[X]) → R) l)

Tactic:
map_list_sum (lcoeff R n) _

Premises used: Polynomial.coeff, map_list_sum, Polynomial.lcoeff
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
simp_rw :
  Eq (α := R) (List.sum (List.map (⇑(lcoeff R n) : (a : R[X]) → R) (List.map f l)))
    (List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l))
simp_rw₁ :
  Eq (α := R) (List.sum (List.map ((⇑(lcoeff R n) : (a : R[X]) → R) ∘ f) l))
    (List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l))
simp_rw₂ :
  Eq.{u + 1} (α := R) (List.sum (List.map (fun (x : ι) ↦ (lcoeff R n : (a : R[X]) → R) (f x)) l))
    (List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l))
⊢ (List.map f l).sum.coeff n = List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l)

Tactic:
simp_rw [coeff_list_sum, List.map_map, Function.comp_def, lcoeff_apply]

Premises used: List.map_map, Polynomial.lcoeff_apply, Function.comp_def, Polynomial.coeff_list_sum
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
n : ℕ
f : ℕ → R → S[X]
⊢ (p.sum f).coeff n = p.sum fun (a : ℕ) (b : R) ↦ (f a b).coeff n

Tactic:
simp [Polynomial.sum]

Premises used: Polynomial.sum
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rcases :
  ∀ (p : R[ℕ]),
    ({ toFinsupp := p : R[X] } * q).coeff n =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, { toFinsupp := p : R[X] }.coeff x.1 * q.coeff x.2
⊢ (p * q).coeff n = ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2

Tactic:
rcases p with ⟨p⟩