awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : hd.degree ≤ n ∧ ∀ a ∈ tl, a.degree ≤ n
⊢ hd.degree ≤ n

Tactic:
rcases hl with ⟨hhd, htl⟩
-- 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 : hd.degree ≤ n ∧ ∀ a ∈ tl, a.degree ≤ n
hhd : hd.degree ≤ n
⊢ ∀ a ∈ tl, a.degree ≤ n

Tactic:
rcases hl with ⟨hhd, htl⟩
-- 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
hhd : hd.degree ≤ n
htl : ∀ a ∈ tl, a.degree ≤ n
⊢ (hd + tl.sum).degree ≤ n

Tactic:
le_trans (degree_add_le hd tl.sum) (max_le hhd (ih htl))

Premises used: List.sum, max_le, Polynomial.degree_add_le, le_trans
-- 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
hhd : hd.degree ≤ n
htl : ∀ a ∈ tl, a.degree ≤ n
⊢ (hd + tl.sum).degree ≤ n

Tactic:
exact le_trans (degree_add_le hd tl.sum) (max_le hhd (ih htl))

Premises used: List.sum, max_le, Polynomial.degree_add_le, le_trans
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
n : WithBot ℕ
hl : ∀ p ∈ l, p.degree ≤ n
nil :
  ∀ (hl : ∀ (p : S[X]), Membership.mem (γ := List S[X]) [] p → p.degree ≤ n), degree.{u_1} (R := S) (List.sum []) ≤ n
cons :
  ∀ (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 :: tl).sum.degree ≤ n
⊢ l.sum.degree ≤ n

Tactic:
induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [List.mem_cons, forall_eq_or_imp] at hl
    rcases hl with ⟨hhd, htl⟩
    rw [List.sum_cons]
    exact le_trans (degree_add_le hd tl.sum) (max_le hhd (ih htl))

Premises used: forall_eq_or_imp, List.sum_cons, List.mem_cons
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
hl : ∀ p ∈ l, p.degree ≤ (List.map natDegree l).maximum
⊢ l.sum.degree ≤ (List.map natDegree l).maximum

Tactic:
apply degree_list_sum_le_of_forall_degree_le

Premises used: Polynomial.degree_list_sum_le_of_forall_degree_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
pos : ∀ (h : p = 0), p.degree ≤ (List.map natDegree l).maximum
neg : ∀ (h : ¬p = 0), p.degree ≤ (List.map natDegree l).maximum
⊢ p.degree ≤ (List.map natDegree l).maximum

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : p = 0
pos : ∀ (hp : 0 ∈ l), degree.{u_1} (R := S) 0 ≤ (List.map natDegree l).maximum
⊢ p.degree ≤ (List.map natDegree l).maximum

Tactic:
subst h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
hp : 0 ∈ l
⊢ degree.{u_1} (R := S) 0 ≤ (List.map natDegree l).maximum

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
neg : (↑p.natDegree : WithBot ℕ) ≤ (List.map natDegree l).maximum
⊢ p.degree ≤ (List.map natDegree l).maximum

Tactic:
rw [degree_eq_natDegree h]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
neg : (↑p.natDegree : ℕ) ∈ List.map natDegree l
⊢ (↑p.natDegree : WithBot ℕ) ≤ (List.map natDegree l).maximum

Tactic:
apply List.le_maximum_of_mem'

Premises used: List.le_maximum_of_mem'
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
neg : ∃ a ∈ l, a.natDegree = (↑p.natDegree : ℕ)
⊢ (↑p.natDegree : ℕ) ∈ List.map natDegree l

Tactic:
rw [List.mem_map]

Premises used: List.mem_map
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
h₁ : p ∈ l ∧ p.natDegree = (↑p.natDegree : ℕ)
⊢ ∃ a ∈ l, a.natDegree = (↑p.natDegree : ℕ)

Tactic:
use p
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ p ∈ l ∧ p.natDegree = (↑p.natDegree : ℕ)

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
⊢ l.prod.natDegree ≤ (List.map natDegree l).sum

Tactic:
l.apply_prod_le_sum_map _ natDegree_one.le fun _ _ => natDegree_mul_le

Premises used: List.apply_prod_le_sum_map, Eq.le, Polynomial.natDegree_one, Polynomial.natDegree_mul_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
⊢ l.prod.degree ≤ (List.map degree l).sum

Tactic:
l.apply_prod_le_sum_map _ degree_one_le degree_mul_le

Premises used: Polynomial.degree_mul_le, List.apply_prod_le_sum_map, Polynomial.degree_one_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hl : ∀ (p : S[X]), Membership.mem (γ := List S[X]) [] p → p.natDegree ≤ n
⊢ Eq.{u_1 + 1} (α := S) (coeff (List.prod []) (List.length.{u_1} (α := S[X]) [] * n))
    (List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) []))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
⊢ ∀ p ∈ tl, p.natDegree ≤ n

Tactic:
have hl' : ∀ p ∈ tl, natDegree p ≤ n := fun p hp => hl p (List.mem_cons_of_mem _ hp)
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
cons : (hd * tl.prod).coeff ((tl.length + 1) * n) = hd.coeff n * List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
⊢ (hd :: tl).prod.coeff ((hd :: tl).length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) (hd :: tl))

Tactic:
simp only [List.prod_cons, List.map, List.length]

Premises used: List.map, List.prod_cons, List.length
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
cons : (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)
⊢ (hd * tl.prod).coeff ((tl.length + 1) * n) = hd.coeff n * List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)

Tactic:
rw [add_mul, one_mul, add_comm, ← IH hl', mul_comm tl.length]

Premises used: add_mul, add_comm, mul_comm, List.length, one_mul
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ tl.prod.natDegree ≤ n * tl.length

Tactic:
(natDegree_list_prod_le _).trans ?_

Premises used: LE.le.trans, Polynomial.natDegree_list_prod_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
refine : (List.map natDegree tl).sum ≤ n * tl.length
⊢ tl.prod.natDegree ≤ n * tl.length

Tactic:
refine (natDegree_list_prod_le _).trans ?_

Premises used: LE.le.trans, Polynomial.natDegree_list_prod_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
rw : (List.map natDegree tl).sum ≤ (List.map natDegree tl).length * n
⊢ (List.map natDegree tl).sum ≤ n * tl.length

Tactic:
rw [← tl.length_map natDegree, mul_comm]

Premises used: List.length_map, mul_comm, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (List.map natDegree tl).sum ≤ (List.map natDegree tl).length * n

Tactic:
List.sum_le_card_nsmul _ _ ?_

Premises used: List.sum_le_card_nsmul
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
refine : ∀ x ∈ List.map natDegree tl, x ≤ n
⊢ (List.map natDegree tl).sum ≤ (List.map natDegree tl).length * n

Tactic:
refine List.sum_le_card_nsmul _ _ ?_

Premises used: List.sum_le_card_nsmul
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ ∀ x ∈ List.map natDegree tl, x ≤ n

Tactic:
simpa using hl'
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ tl.prod.natDegree ≤ n * tl.length

Tactic:
have h : natDegree tl.prod ≤ n * tl.length := by
      refine (natDegree_list_prod_le _).trans ?_
      rw [← tl.length_map natDegree, mul_comm]
      refine List.sum_le_card_nsmul _ _ ?_
      simpa using hl'
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
h : tl.prod.natDegree ≤ n * tl.length
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)

Tactic:
coeff_mul_add_eq_of_natDegree_le (hl _ List.mem_cons_self) h

Premises used: Polynomial.coeff_mul_add_eq_of_natDegree_le, List.mem_cons_self
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH :
  ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
    tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
h : tl.prod.natDegree ≤ n * tl.length
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)

Tactic:
exact coeff_mul_add_eq_of_natDegree_le (hl _ List.mem_cons_self) h

Premises used: Polynomial.coeff_mul_add_eq_of_natDegree_le, List.mem_cons_self
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
n : ℕ
hl : ∀ p ∈ l, p.natDegree ≤ n
nil :
  ∀ (hl : ∀ (p : S[X]), Membership.mem (γ := List S[X]) [] p → p.natDegree ≤ n),
    Eq.{u_1 + 1} (α := S) (coeff (List.prod []) (List.length.{u_1} (α := S[X]) [] * n))
      (List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) []))
cons :
  ∀ (hd : S[X]) (tl : List S[X])
    (IH :
      ∀ (hl : ∀ p ∈ tl, p.natDegree ≤ n),
        tl.prod.coeff (tl.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl))
    (hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n),
    (hd :: tl).prod.coeff ((hd :: tl).length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) (hd :: tl))
⊢ l.prod.coeff (l.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) l)

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH =>
    have hl' : ∀ p ∈ tl, natDegree p ≤ n := fun p hp => hl p (List.mem_cons_of_mem _ hp)
    simp only [List.prod_cons, List.map, List.length]
    rw [add_mul, one_mul, add_comm, ← IH hl', mul_comm tl.length]
    have h : natDegree tl.prod ≤ n * tl.length := by
      refine (natDegree_list_prod_le _).trans ?_
      rw [← tl.length_map natDegree, mul_comm]
      refine List.sum_le_card_nsmul _ _ ?_
      simpa using hl'
    exact coeff_mul_add_eq_of_natDegree_le (hl _ List.mem_cons_self) h

Premises used: add_mul, List.map, add_comm, List.prod_cons, List.length, one_mul
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), (prod ⟦a⟧).natDegree ≤ (Multiset.map natDegree ⟦a⟧).sum

Tactic:
simpa using natDegree_list_prod_le

Premises used: Polynomial.natDegree_list_prod_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
⊢ natDegree.{u} (R := R) (∏ i ∈ s, f i) ≤ ∑ i ∈ s, (f i).natDegree

Tactic:
simpa using natDegree_multiset_prod_le (s.1.map f)

Premises used: Multiset.map, Finset.val, Polynomial.natDegree_multiset_prod_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), (prod ⟦a⟧).degree ≤ (Multiset.map degree ⟦a⟧).sum

Tactic:
simpa using degree_list_prod_le

Premises used: Polynomial.degree_list_prod_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
⊢ degree.{u} (R := R) (∏ i ∈ s, f i) ≤ ∑ i ∈ s, (f i).degree

Tactic:
simpa only [Multiset.map_map] using degree_multiset_prod_le (s.1.map f)

Premises used: Multiset.map, Finset.val, Polynomial.degree_multiset_prod_le, Multiset.map_map
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
h : Ne.{u + 1} (α := R) (prod (Multiset.map (α := R[X]) leadingCoeff 0)) 0
⊢ Eq.{u + 1} (α := R) (leadingCoeff (prod 0)) (prod (Multiset.map (α := R[X]) leadingCoeff 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : ∀ (h : (Multiset.map leadingCoeff t).prod ≠ 0), t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : (Multiset.map leadingCoeff (a ::ₘ t)).prod ≠ 0
⊢ (a ::ₘ t).prod.leadingCoeff = (Multiset.map leadingCoeff (a ::ₘ t)).prod

Tactic:
?_
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
h : (Multiset.map leadingCoeff t).prod ≠ 0
cons :
  ∀ (a : R[X]) (t : Multiset R[X])
    (ih : ∀ (h : (Multiset.map leadingCoeff t).prod ≠ 0), t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod)
    (h : (Multiset.map leadingCoeff (a ::ₘ t)).prod ≠ 0),
    (a ::ₘ t).prod.leadingCoeff = (Multiset.map leadingCoeff (a ::ₘ t)).prod
⊢ t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod

Tactic:
induction t using Multiset.induction_on with | empty => simp | cons a t ih => ?_
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : ∀ (h : (Multiset.map leadingCoeff t).prod ≠ 0), t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : (Multiset.map leadingCoeff (a ::ₘ t)).prod ≠ 0
cons :
  ∀ (h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0),
    (a * t.prod).leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
⊢ (a ::ₘ t).prod.leadingCoeff = (Multiset.map leadingCoeff (a ::ₘ t)).prod

Tactic:
simp only [Multiset.map_cons, Multiset.prod_cons] at h ⊢

Premises used: Multiset.map_cons, Multiset.prod_cons
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : ∀ (h : (Multiset.map leadingCoeff t).prod ≠ 0), t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
cons : a.leadingCoeff * t.prod.leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
cons₁ : a.leadingCoeff * t.prod.leadingCoeff ≠ 0
⊢ (a * t.prod).leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod

Tactic:
rw [Polynomial.leadingCoeff_mul']

Premises used: Polynomial.leadingCoeff_mul'
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : ∀ (h : (Multiset.map leadingCoeff t).prod ≠ 0), t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
cons : (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : ∀ (h : (Multiset.map leadingCoeff t).prod ≠ 0), t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ ¬(Multiset.map leadingCoeff t).prod = 0

Tactic:
apply right_ne_zero_of_mul h

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : ∀ (h : (Multiset.map leadingCoeff t).prod ≠ 0), t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
cons : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
cons₁ : (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : ∀ (h : (Multiset.map leadingCoeff t).prod ≠ 0), t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0

Tactic:
h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : ∀ (h : (Multiset.map leadingCoeff t).prod ≠ 0), t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0

Tactic:
exact h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
h : Ne.{u + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
⊢ (Multiset.map leadingCoeff (Multiset.map f s.val)).prod ≠ 0

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
h : Ne.{u + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
⊢ Eq.{u + 1} (α := R) (leadingCoeff (∏ i ∈ s, f i)) (∏ i ∈ s, (f i).leadingCoeff)

Tactic:
simpa using leadingCoeff_multiset_prod' (s.1.map f) (by simpa using h)

Premises used: Polynomial.leadingCoeff_multiset_prod', Multiset.map, Finset.val
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0
revert :
  ∀ (h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0),
    t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t)
⊢ t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t)

Tactic:
revert h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
⊢ ∀ (h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0),
    t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t)

Tactic:
Multiset.induction_on t ?_ fun a t ih ht => ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
refine_1 :
  ∀ (h : Ne.{u + 1} (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) 0)) 0),
    natDegree.{u} (R := R) (prod 0) = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) 0)
refine_2 :
  ∀ (a : R[X]) (t : Multiset R[X])
    (ih :
      ∀ (h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0),
        t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t))
    (ht : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) (a ::ₘ t))) 0),
    (a ::ₘ t).prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) (a ::ₘ t))
⊢ ∀ (h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0),
    t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t)

Tactic:
refine Multiset.induction_on t ?_ fun a t ih ht => ?_
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
⊢ ∀ (h : Ne.{u + 1} (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) 0)) 0),
    natDegree.{u} (R := R) (prod 0) = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  ∀ (h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0),
    t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t)
ht : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) (a ::ₘ t))) 0
refine_2 :
  ∀ (ht : a.leadingCoeff * prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t) ≠ 0),
    (a * t.prod).natDegree = (a.natDegree ::ₘ Multiset.map (fun (f : R[X]) ↦ f.natDegree) t).sum
⊢ (a ::ₘ t).prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) (a ::ₘ t))

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons] at ht ⊢

Premises used: Multiset.map_cons, Multiset.prod_cons
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  ∀ (h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0),
    t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t)
ht : a.leadingCoeff * prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t) ≠ 0
refine_2 : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0
refine_2₁ : a.leadingCoeff * t.prod.leadingCoeff ≠ 0
⊢ (a * t.prod).natDegree = (a.natDegree ::ₘ Multiset.map (fun (f : R[X]) ↦ f.natDegree) t).sum

Tactic:
rw [Multiset.sum_cons, Polynomial.natDegree_mul', ih]

Premises used: Polynomial.natDegree_mul', Multiset.sum_cons
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  ∀ (h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0),
    t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t)
ht : a.leadingCoeff * prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t) ≠ 0
⊢ Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0

Tactic:
apply right_ne_zero_of_mul ht

Premises used: right_ne_zero_of_mul