awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
rw : (if a = 0 then p.support.erase n else insert n p.support) = insert n p.support
rw₁ rw₂ : insert n p.support = insert n p.support
⊢ (p.update n a).support = insert n p.support

Tactic:
rw [support_update, if_neg ha]

Premises used: Polynomial.support_update, if_neg
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
classical : (if a = 0 then p.support.erase n else insert n p.support) = insert n p.support
classical₁ classical₂ : insert n p.support = insert n p.support
⊢ (p.update n a).support = insert n p.support

Tactic:
classical rw [support_update, if_neg ha]

Premises used: Polynomial.support_update, if_neg
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := Finset R) (coeffs 0) ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.zero, Finset.empty, Multiset.ofList, Polynomial.coeffs, List.pwFilter, List.foldr, Finset.image, rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

Tactic:
simp [coeffs, eq_comm, (Finset.mem_image)]

Premises used: Finset.mem_image, eq_comm, Polynomial.coeffs
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
simp_rw : ∀ x ∈ support.{u} (R := R) 1, Membership.mem (γ := Finset R) {1} (coeff 1 x)
⊢ Subset (α := Finset R) (coeffs 1) {1}

Tactic:
simp_rw [coeffs, Finset.image_subset_iff]

Premises used: Finset.image_subset_iff, Polynomial.coeffs
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ ∀ x ∈ support.{u} (R := R) 1, Membership.mem (γ := Finset R) {1} (coeff 1 x)

Tactic:
simp_all [coeff_one]

Premises used: Polynomial.coeff_one
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
simp_rw : Subset (α := Finset R) (image (fun (n : ℕ) ↦ coeff 1 n) (support.{u} (R := R) 1)) {1}
simp_rw₁ : ∀ x ∈ support.{u} (R := R) 1, Membership.mem (γ := Finset R) {1} (coeff 1 x)
⊢ Subset (α := Finset R) (coeffs 1) {1}

Tactic:
classical
  simp_rw [coeffs, Finset.image_subset_iff]
  simp_all [coeff_one]

Premises used: Polynomial.coeff_one, Finset.image_subset_iff, Polynomial.coeffs
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
simp : ∃ (a : ℕ), ¬p.coeff a = 0 ∧ p.coeff a = p.coeff n
⊢ p.coeff n ∈ p.coeffs

Tactic:
simp only [coeffs, mem_support_iff, Finset.mem_image, Ne]

Premises used: Finset.mem_image, Polynomial.mem_support_iff, Ne, Polynomial.coeffs
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ ∃ (a : ℕ), ¬p.coeff a = 0 ∧ p.coeff a = p.coeff n

Tactic:
⟨n, h, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ ∃ (a : ℕ), ¬p.coeff a = 0 ∧ p.coeff a = p.coeff n

Tactic:
exact ⟨n, h, rfl⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
simp : ∃ (a : ℕ), ¬p.coeff a = 0 ∧ p.coeff a = p.coeff n
⊢ p.coeff n ∈ p.coeffs

Tactic:
classical
  simp only [coeffs, mem_support_iff, Finset.mem_image, Ne]
  exact ⟨n, h, rfl⟩

Premises used: Finset.mem_image, Polynomial.mem_support_iff, Ne, Polynomial.coeffs
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p = 0
⊢ p.coeffs = ∅

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
refine : p.coeffs = ∅ → p = 0
⊢ p.coeffs = ∅ ↔ p = 0

Tactic:
refine ⟨?_, fun h ↦ by simp [h]⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
contrapose! : p ≠ 0 → p.coeffs.Nonempty
⊢ p.coeffs = ∅ → p = 0

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.support.Nonempty

Tactic:
rw [← support_nonempty] at h

Premises used: Polynomial.support_nonempty
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.support.Nonempty
obtain : ∀ (n : ℕ) (hn : n ∈ p.support), p.coeffs.Nonempty
⊢ p.coeffs.Nonempty

Tactic:
obtain ⟨n, hn⟩ := h
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ p.support
⊢ p.coeff n ≠ 0

Tactic:
rw [mem_support_iff] at hn

Premises used: Polynomial.mem_support_iff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : p.coeff n ≠ 0
⊢ p.coeffs.Nonempty

Tactic:
⟨p.coeff n, coeff_mem_coeffs hn⟩

Premises used: Polynomial.coeff_mem_coeffs, Polynomial.coeff, Exists.intro, Finset.Nonempty
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : p.coeff n ≠ 0
⊢ p.coeffs.Nonempty

Tactic:
exact ⟨p.coeff n, coeff_mem_coeffs hn⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.coeffs.Nonempty ↔ p ≠ 0

Tactic:
simp [Finset.nonempty_iff_ne_empty]

Premises used: Finset.nonempty_iff_ne_empty
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
c : R
hc : c ≠ 0
rw : Eq (α := Finset R) (image (fun (n_1 : ℕ) ↦ coeff ((monomial n : (a : R) → R[X]) c) n_1) {n}) {c}
⊢ Eq (α := Finset R) (coeffs ((monomial n : (a : R) → R[X]) c)) {c}

Tactic:
rw [coeffs, support_monomial n hc]

Premises used: Polynomial.support_monomial, Polynomial.coeffs
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ Eq (α := Finset R) (image (fun (n_1 : ℕ) ↦ coeff ((monomial n : (a : R) → R[X]) c) n_1) {n}) {c}

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
a : ℤ
b : R[ℕ]
⊢ { toFinsupp := a • b : R[X] } = a • { toFinsupp := b : R[X] }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
a : ℤ
b : R[X]
⊢ (a • b).toFinsupp = a • b.toFinsupp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
z : ℤ
⊢ Eq.{u + 1} (α := R[X]) { toFinsupp := (↑z : R[ℕ]) } (↑z : R[X])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
z : ℤ
⊢ Eq.{u + 1} (α := R[ℕ]) (toFinsupp (↑z : R[X])) (↑z : R[ℕ])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
rcases : ∀ (toFinsupp : R[ℕ]), (-{ toFinsupp := toFinsupp : R[X] }).coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
⊢ (-p).coeff n = -p.coeff n

Tactic:
rcases p with ⟨⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp : R[ℕ]
rw : { toFinsupp := -toFinsupp : R[X] }.coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
rw₁ : (-toFinsupp : (a : ℕ) → R) n = -{ toFinsupp := toFinsupp : R[X] }.coeff n
rw₂ : Eq (α := R) ((-toFinsupp : (a : ℕ) → R) n : R) (-(toFinsupp : (a : ℕ) → R) n : R)
rw₃ rw₄ : Eq (α := R) (-(toFinsupp : (a : ℕ) → R) n : R) (-(toFinsupp : (a : ℕ) → R) n : R)
⊢ (-{ toFinsupp := toFinsupp : R[X] }).coeff n = -{ toFinsupp := toFinsupp : R[X] }.coeff n

Tactic:
rw [← ofFinsupp_neg, coeff, coeff, Finsupp.neg_apply]

Premises used: Polynomial.coeff, Polynomial.ofFinsupp_neg, Finsupp.neg_apply
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring 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.Basic
Goal:
R : Type u
inst : Ring 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.Basic
Goal:
R : Type u
inst : Ring R
n : ℕ
toFinsupp toFinsupp_1 : R[ℕ]
rw :
  { toFinsupp := toFinsupp - toFinsupp_1 : R[X] }.coeff n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
rw₁ :
  (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
    { toFinsupp := toFinsupp : R[X] }.coeff n - { toFinsupp := toFinsupp_1 : R[X] }.coeff n
rw₂ :
  (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
    HSub.hSub (α := R) ((toFinsupp : (a : ℕ) → R) n : R) ({ toFinsupp := toFinsupp_1 : R[X] }.coeff n)
rw₃ :
  (toFinsupp - toFinsupp_1 : (a : ℕ) → R) n =
    HSub.hSub (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R)
rw₄ rw₅ :
  HSub.hSub (α := R) (β := R) ((toFinsupp : (a : ℕ) → R) n : R) ((toFinsupp_1 : (a : ℕ) → R) n : R) =
    HSub.hSub (α := 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:
rw [← ofFinsupp_sub, coeff, coeff, coeff, Finsupp.sub_apply]

Premises used: Finsupp.sub_apply, Polynomial.ofFinsupp_sub, Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
n : ℕ
a : R
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X])
      ((monomial n : (a : R) → R[X]) a : R[X]) =
    0
rw₁ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (-a + a) : R[X]) (0 : R[X])
rw₂ : Eq.{u + 1} (α := R[X]) ((monomial n : (a : R) → R[X]) 0) 0
rw₃ rw₄ : Eq.{u + 1} (α := R[X]) 0 0
⊢ Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (-a) : R[X]) (-(monomial n : (a : R) → R[X]) a : R[X])

Tactic:
rw [eq_neg_iff_add_eq_zero, ← map_add, neg_add_cancel, monomial_zero_right]

Premises used: map_add, neg_add_cancel, Polynomial.monomial_zero_right, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
inst : Ring R
n : ℕ
rw :
  (monomial n : (a : R) → R[X]) (a + -b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X])
      ((monomial n : (a : R) → R[X]) (-b) : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
rw₂ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) (-(monomial n : (a : R) → R[X]) b : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])
rw₃ rw₄ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) (-(monomial n : (a : R) → R[X]) b : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) (-(monomial n : (a : R) → R[X]) b : R[X])
⊢ (monomial n : (a : R) → R[X]) (a - b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])

Tactic:
rw [sub_eq_add_neg, map_add, monomial_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, map_add, Polynomial.monomial_neg
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
rcases : ∀ (toFinsupp : R[ℕ]), (-{ toFinsupp := toFinsupp : R[X] }).support = { toFinsupp := toFinsupp : R[X] }.support
⊢ (-p).support = p.support

Tactic:
rcases p with ⟨⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
toFinsupp : R[ℕ]
rw : { toFinsupp := -toFinsupp : R[X] }.support = { toFinsupp := toFinsupp : R[X] }.support
rw₁ : (-toFinsupp).support = { toFinsupp := toFinsupp : R[X] }.support
rw₂ : (-toFinsupp).support = toFinsupp.support
rw₃ rw₄ : toFinsupp.support = toFinsupp.support
⊢ (-{ toFinsupp := toFinsupp : R[X] }).support = { toFinsupp := toFinsupp : R[X] }.support

Tactic:
rw [← ofFinsupp_neg, support, support, Finsupp.support_neg]

Premises used: Polynomial.ofFinsupp_neg, Finsupp.support_neg, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
n : ℤ
⊢ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) (↑n : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
inst : Ring R
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) (-a) : R[X]) (-(C : (a : R) → R[X]) a : R[X])

Tactic:
map_neg C a

Premises used: Polynomial.C, map_neg
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
inst : Ring R
⊢ (C : (a : R) → R[X]) (a - b) =
    HSub.hSub (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b : R[X])

Tactic:
map_sub C a b

Premises used: Polynomial.C, map_sub
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
⊢ Nontrivial.{u} R[ℕ]

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
⊢ Nontrivial.{u} R[ℕ]

Tactic:
have h : Nontrivial R[ℕ] := by infer_instance
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
h : Nontrivial.{u} R[ℕ]
rcases : ∀ (x y : R[ℕ]) (hxy : x ≠ y), Nontrivial.{u} R[X]
⊢ Nontrivial.{u} R[X]

Tactic:
rcases h.exists_pair_ne with ⟨x, y, hxy⟩

Premises used: Nontrivial.exists_pair_ne
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
h : Nontrivial.{u} R[ℕ]
x y : R[ℕ]
hxy : x ≠ y
⊢ Nontrivial.{u} R[X]

Tactic:
⟨⟨⟨x⟩, ⟨y⟩, ?_⟩⟩

Premises used: Nontrivial.mk, Exists.intro, Polynomial.ofFinsupp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
h : Nontrivial.{u} R[ℕ]
x y : R[ℕ]
hxy : x ≠ y
refine : { toFinsupp := x : R[X] } ≠ { toFinsupp := y }
⊢ Nontrivial.{u} R[X]

Tactic:
refine ⟨⟨⟨x⟩, ⟨y⟩, ?_⟩⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
h : Nontrivial.{u} R[ℕ]
x y : R[ℕ]
hxy : x ≠ y
⊢ { toFinsupp := x : R[X] } ≠ { toFinsupp := y }

Tactic:
simp [hxy]
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ ¬Eq.{u + 1} (α := R) (coeff X 1) (coeff 0 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : NoZeroDivisors R
⊢ NoZeroDivisors.{u} R[X]

Tactic:
(toFinsuppIso R).injective.noZeroDivisors _ (map_zero _) (map_mul _)

Premises used: RingEquiv.injective, map_zero, map_mul, Polynomial.toFinsuppIso, Function.Injective.noZeroDivisors
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
⊢ IsLeftCancelMulZero.{u} R[X]

Tactic:
(toFinsuppIso R).injective.isLeftCancelMulZero _ (map_zero _) (map_mul _)

Premises used: RingEquiv.injective, map_zero, map_mul, Polynomial.toFinsuppIso, Function.Injective.isLeftCancelMulZero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsRightCancelMulZero R
⊢ IsRightCancelMulZero.{u} R[X]

Tactic:
(toFinsuppIso R).injective.isRightCancelMulZero _ (map_zero _) (map_mul _)

Premises used: RingEquiv.injective, map_zero, map_mul, Polynomial.toFinsuppIso, Function.Injective.isRightCancelMulZero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : DivisionSemiring R
q : ℚ≥0
f : R[X]
rw : q • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) q 1) : R[X]) f
rw₁ : q • f = HSMul.hSMul (β := R[X]) q ((C : (a : R) → R[X]) 1) * f
rw₂ : q • f = HSMul.hSMul (β := R[X]) q 1 * f
rw₃ rw₄ : q • f = q • f
⊢ q • f = (C : (a : R) → R[X]) (↑q : R) * f

Tactic:
rw [← NNRat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]

Premises used: Polynomial.C_1, smul_one_mul, Polynomial.smul_C, NNRat.smul_one_eq_cast
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : DivisionRing R
a : ℚ
f : R[X]
rw : a • f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) a 1) : R[X]) f
rw₁ : a • f = HSMul.hSMul (β := R[X]) a ((C : (a : R) → R[X]) 1) * f
rw₂ : a • f = HSMul.hSMul (β := R[X]) a 1 * f
rw₃ rw₄ : a • f = a • f
⊢ a • f = (C : (a : R) → R[X]) (↑a : R) * f

Tactic:
rw [← Rat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]

Premises used: Polynomial.C_1, Rat.smul_one_eq_cast, smul_one_mul, Polynomial.smul_C
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Nontrivial.{u} R[X] ↔ Nontrivial R

Tactic:
⟨fun h =>
    let ⟨_r, _s, hrs⟩ := @exists_pair_ne _ h
    Nontrivial.of_polynomial_ne hrs,
    fun h => @Polynomial.nontrivial _ _ h⟩

Premises used: Nontrivial, _private.0.Polynomial.nontrivial_iff.match_1, Polynomial.nontrivial, Polynomial, Polynomial.Nontrivial.of_polynomial_ne, Iff.intro, exists_pair_ne
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : CommRing R
⊢ Eq.{u + 1} (α := R[X])
    (Multiset.prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0))
    1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : CommRing R
⊢ ∀ (a b : Multiset R),
    Multiset.prod
        (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) (a + b)) =
      HMul.hMul (α := R[X])
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) a))
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) b))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basis
Goal:
R : Type u
inst : Semiring R
⊢ Eq (α := (a : ℕ) → R[X]) (⇑(basisMonomials R) : (a : ℕ) → R[X]) fun (s : ℕ) ↦ (monomial s : (a : R) → R[X]) 1

Tactic:
funext fun _ => ofFinsupp_single _ _

Premises used: Polynomial.ofFinsupp_single, funext, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
h0 : natDegree.{u_1} (R := S) 0 ≤ 0
hadd : ∀ (x y : S[X]), (x + y).natDegree ≤ max x.natDegree y.natDegree
⊢ l.sum.natDegree ≤ List.foldr max 0 (List.map natDegree l)

Tactic:
apply List.sum_le_foldr_max natDegree

Premises used: Polynomial.natDegree, List.sum_le_foldr_max
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
⊢ natDegree.{u_1} (R := S) 0 ≤ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
⊢ ∀ (x y : S[X]), (x + y).natDegree ≤ max x.natDegree y.natDegree

Tactic:
natDegree_add_le

Premises used: Polynomial.natDegree_add_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
⊢ ∀ (x y : S[X]), (x + y).natDegree ≤ max x.natDegree y.natDegree

Tactic:
exact natDegree_add_le

Premises used: Polynomial.natDegree_add_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : Multiset S[X]
⊢ ∀ (a : List S[X]), (Multiset.sum ⟦a⟧).natDegree ≤ foldr max 0 (Multiset.map natDegree ⟦a⟧)

Tactic:
simpa using natDegree_list_sum_le

Premises used: Polynomial.natDegree_list_sum_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
s : Finset ι
S : Type u_1
inst : Semiring S
f : ι → S[X]
⊢ natDegree.{u_1} (R := S) (∑ i ∈ s, f i) ≤ Finset.fold max 0 (natDegree ∘ f) s

Tactic:
simpa using natDegree_multiset_sum_le (s.val.map f)

Premises used: Multiset.map, Finset.val, Polynomial.natDegree_multiset_sum_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
s : Finset ι
S : Type u_1
inst : Semiring S
n : ℕ
f : ι → S[X]
h : ∀ i ∈ s, (f i).natDegree ≤ n
⊢ 0 ≤ n ∧ ∀ x ∈ s, (natDegree ∘ f) x ≤ n

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
d : WithBot ℕ
hd : ∀ k ∈ s, (f k).degree = d
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
none :
  ∀ (hd : ∀ k ∈ s, (f k).degree = Option.none),
    Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)
some :
  ∀ (d : ℕ) (hd : ∀ k ∈ s, (f k).degree = Option.some d),
    Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)
⊢ Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)

Tactic:
obtain _ | d := d
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
hd : ∀ k ∈ s, (f k).degree = none
⊢ Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)

Tactic:
simp_all [WithBot.none_eq_bot]

Premises used: WithBot.none_eq_bot
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
d : ℕ
hd : ∀ k ∈ s, (f k).degree = some d
⊢ ∀ (k : ι) (hk : k ∈ s), (f k).natDegree = d

Tactic:
replace hd k (hk : k ∈ s) : (f k).natDegree = d := natDegree_eq_of_degree_eq_some <| hd k hk
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
d : ℕ
hd : ∀ (k : ι) (hk : k ∈ s), (f k).natDegree = d
this : natDegree.{u_1} (R := S) (∑ k ∈ s, f k) = d
⊢ Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)

Tactic:
simp_all [leadingCoeff]

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
d : ℕ
hd : ∀ (k : ι) (hk : k ∈ s), (f k).natDegree = d
some : natDegree.{u_1} (R := S) (∑ k ∈ s, f k) = d
⊢ Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)

Tactic:
suffices (∑ k ∈ s, f k).natDegree = d by simp_all [leadingCoeff]
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
d : ℕ
hd : ∀ (k : ι) (hk : k ∈ s), (f k).natDegree = d
some : natDegree.{u_1} (R := S) (∑ k ∈ s, f k) ≤ d
some₁ : Ne.{u_1 + 1} (α := S) (coeff (∑ k ∈ s, f k) d) 0
⊢ natDegree.{u_1} (R := S) (∑ k ∈ s, f k) = d

Tactic:
apply natDegree_eq_of_le_of_coeff_ne_zero

Premises used: Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
d : ℕ
hd : ∀ (k : ι) (hk : k ∈ s), (f k).natDegree = d
⊢ natDegree.{u_1} (R := S) (∑ k ∈ s, f k) ≤ d

Tactic:
aesop (add safe natDegree_sum_le_of_forall_le)

Premises used: Polynomial.natDegree_sum_le_of_forall_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
ι : Type w
S : Type u_1
inst : Semiring S
f : ι → S[X]
s : Finset ι
hf : Ne.{u_1 + 1} (α := S) (∑ k ∈ s, (f k).leadingCoeff) 0
d : ℕ
hd : ∀ (k : ι) (hk : k ∈ s), (f k).natDegree = d
⊢ Ne.{u_1 + 1} (α := S) (coeff (∑ k ∈ s, f k) d) 0

Tactic:
simp_all [leadingCoeff]

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : WithBot ℕ
hl : ∀ (p : S[X]), Membership.mem (γ := List S[X]) [] p → p.degree ≤ n
⊢ degree.{u_1} (R := S) (List.sum []) ≤ n

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : WithBot ℕ
hd : S[X]
tl : List S[X]
ih : ∀ (hl : ∀ p ∈ tl, p.degree ≤ n), tl.sum.degree ≤ n
hl : ∀ p ∈ hd :: tl, p.degree ≤ n
⊢ hd.degree ≤ n ∧ ∀ a ∈ tl, a.degree ≤ n

Tactic:
simp only [List.mem_cons, forall_eq_or_imp] at hl

Premises used: forall_eq_or_imp, List.mem_cons