awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)
have hd₁ : ∀ (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
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ Eq.{u_1 + 1} (α := S) (leadingCoeff (∑ k ∈ s, f k)) (∑ k ∈ s, (f k).leadingCoeff)
have some : natDegree.{u_1} (R := S) (∑ k ∈ s, f k) = d
Tactic: suffices (∑ k ∈ s, f k).natDegree = d by simp_all [leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
have some : natDegree.{u_1} (R := S) (∑ k ∈ s, f k) ≤ d
Tactic: apply natDegree_eq_of_le_of_coeff_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ natDegree.{u_1} (R := S) (∑ k ∈ s, f k) = d
have some₁ : Ne.{u_1 + 1} (α := S) (coeff (∑ k ∈ s, f k) d) 0
Tactic: apply natDegree_eq_of_le_of_coeff_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
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 :: tl).sum.degree ≤ n
have hl₁ : hd.degree ≤ n ∧ ∀ a ∈ tl, a.degree ≤ n
Tactic: simp only [List.mem_cons, forall_eq_or_imp] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
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 :: tl).sum.degree ≤ n
have hhd : hd.degree ≤ n
Tactic: rcases hl with ⟨hhd, htl⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
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
⊢ (hd :: tl).sum.degree ≤ n
have htl : ∀ a ∈ tl, a.degree ≤ n
Tactic: rcases hl with ⟨hhd, htl⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
n : WithBot ℕ
hl : ∀ p ∈ l, p.degree ≤ n
⊢ l.sum.degree ≤ n
have nil : ∀ (hl : ∀ (p : S[X]), Membership.mem (γ := List S[X]) [] p → p.degree ≤ n), degree.{u_1} (R := S) (List.sum []) ≤ 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))
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ l.sum.degree ≤ n
have 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
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))
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
⊢ l.sum.degree ≤ (List.map natDegree l).maximum
have hl : ∀ p ∈ l, p.degree ≤ (List.map natDegree l).maximum
Tactic: apply degree_list_sum_le_of_forall_degree_le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
⊢ p.degree ≤ (List.map natDegree l).maximum
have pos : ∀ (h : p = 0), p.degree ≤ (List.map natDegree l).maximum
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ p.degree ≤ (List.map natDegree l).maximum
have neg : ∀ (h : ¬p = 0), p.degree ≤ (List.map natDegree l).maximum
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : p = 0
⊢ p.degree ≤ (List.map natDegree l).maximum
have pos : ∀ (hp : 0 ∈ l), degree.{u_1} (R := S) 0 ≤ (List.map natDegree l).maximum
Tactic: subst h
Cleared hypotheses: p, hp, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ p.degree ≤ (List.map natDegree l).maximum
have neg : (↑p.natDegree : WithBot ℕ) ≤ (List.map natDegree l).maximum
Tactic: rw [degree_eq_natDegree h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ (↑p.natDegree : WithBot ℕ) ≤ (List.map natDegree l).maximum
have neg : (↑p.natDegree : ℕ) ∈ List.map natDegree l
Tactic: apply List.le_maximum_of_mem'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ (↑p.natDegree : ℕ) ∈ List.map natDegree l
have neg : ∃ a ∈ l, a.natDegree = (↑p.natDegree : ℕ)
Tactic: rw [List.mem_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ ∃ a ∈ l, a.natDegree = (↑p.natDegree : ℕ)
have h₁ : p ∈ l ∧ p.natDegree = (↑p.natDegree : ℕ)
Tactic: use p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
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
⊢ (hd :: tl).prod.coeff ((hd :: tl).length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) (hd :: tl))
have hl' : ∀ p ∈ tl, p.natDegree ≤ n
Tactic: have hl' : ∀ p ∈ tl, natDegree p ≤ n := fun p hp => hl p (List.mem_cons_of_mem _ hp)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ (hd :: tl).prod.coeff ((hd :: tl).length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) (hd :: tl))
have cons : (hd * tl.prod).coeff ((tl.length + 1) * n) = hd.coeff n * List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
Tactic: simp only [List.prod_cons, List.map, List.length]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ (hd * tl.prod).coeff ((tl.length + 1) * n) = hd.coeff n * List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) tl)
have cons : (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)
Tactic: rw [add_mul, one_mul, add_comm, ← IH hl', mul_comm tl.length]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
have refine : (List.map natDegree tl).sum ≤ n * tl.length
Tactic: refine (natDegree_list_prod_le _).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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 ≤ n * tl.length
have rw : (List.map natDegree tl).sum ≤ (List.map natDegree tl).length * n
Tactic: rw [← tl.length_map natDegree, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
have refine : ∀ x ∈ List.map natDegree tl, x ≤ n
Tactic: refine List.sum_le_card_nsmul _ _ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
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
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)
have h : 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'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
S : Type u_1
inst : Semiring S
l : List S[X]
n : ℕ
hl : ∀ p ∈ l, p.natDegree ≤ n
⊢ l.prod.coeff (l.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) l)
have 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) []))
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
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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) []))
⊢ l.prod.coeff (l.length * n) = List.prod (List.map (fun (p : S[X]) ↦ p.coeff n) l)
have 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))
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
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
h : (Multiset.map leadingCoeff t).prod ≠ 0
⊢ t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
have 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
Tactic: induction t using Multiset.induction_on with | empty => simp | cons a t ih => ?_
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
have cons : ∀ (h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0),
  (a * t.prod).leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
Tactic: simp only [Multiset.map_cons, Multiset.prod_cons] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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 * t.prod).leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
have cons : a.leadingCoeff * t.prod.leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
Tactic: rw [Polynomial.leadingCoeff_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ (a * t.prod).leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
have cons₁ : a.leadingCoeff * t.prod.leadingCoeff ≠ 0
Tactic: rw [Polynomial.leadingCoeff_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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 * t.prod.leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
have cons : (Multiset.map leadingCoeff t).prod ≠ 0
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0
have cons₁ : (Multiset.map leadingCoeff t).prod ≠ 0
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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)
have 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)
Tactic: refine Multiset.induction_on t ?_ fun a t ih ht => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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)
⊢ ∀ (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)
have 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))
Tactic: refine Multiset.induction_on t ?_ fun a t ih ht => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ (a ::ₘ t).prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) (a ::ₘ t))
have 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
Tactic: rw [Multiset.map_cons, Multiset.prod_cons] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ (a * t.prod).natDegree = (a.natDegree ::ₘ Multiset.map (fun (f : R[X]) ↦ f.natDegree) t).sum
have refine_2 : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0
Tactic: rw [Multiset.sum_cons, Polynomial.natDegree_mul', ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ (a * t.prod).natDegree = (a.natDegree ::ₘ Multiset.map (fun (f : R[X]) ↦ f.natDegree) t).sum
have refine_2₁ : a.leadingCoeff * t.prod.leadingCoeff ≠ 0
Tactic: rw [Multiset.sum_cons, Polynomial.natDegree_mul', ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0
have refine_2 : (Multiset.map leadingCoeff t).prod ≠ 0
Tactic: rwa [Polynomial.leadingCoeff_multiset_prod']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
h_1 : Nontrivial R
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum
have h₁ : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0
Tactic: apply natDegree_multiset_prod'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
inst_1 : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod.degree = (Multiset.map degree t).sum
have this : t.prod ≠ 0
Tactic: have : t.prod ≠ 0 := Monic.ne_zero <| by simpa using monic_multiset_prod_of_monic _ _ h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
inst_1 : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ t.prod.degree = (Multiset.map degree t).sum
have rw : (↑t.prod.natDegree : WithBot ℕ) = (Multiset.map degree t).sum
Tactic: rw [degree_eq_natDegree this, natDegree_multiset_prod_of_monic _ h, Nat.cast_multiset_sum,
    Multiset.map_map, Function.comp_def,
    Multiset.map_congr rfl (fun f hf => (degree_eq_natDegree (h f hf).ne_zero).symm)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
inst_1 : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
rw : (↑t.prod.natDegree : WithBot ℕ) = (Multiset.map degree t).sum
⊢ t.prod.degree = (Multiset.map degree t).sum
have rw₁ : (↑(Multiset.map natDegree t).sum : WithBot ℕ) = (Multiset.map degree t).sum
Tactic: rw [degree_eq_natDegree this, natDegree_multiset_prod_of_monic _ h, Nat.cast_multiset_sum,
    Multiset.map_map, Function.comp_def,
    Multiset.map_congr rfl (fun f hf => (degree_eq_natDegree (h f hf).ne_zero).symm)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
inst_1 : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
rw : (↑t.prod.natDegree : WithBot ℕ) = (Multiset.map degree t).sum
rw₁ : (↑(Multiset.map natDegree t).sum : WithBot ℕ) = (Multiset.map degree t).sum
⊢ t.prod.degree = (Multiset.map degree t).sum
have rw₂ : Multiset.sum (Multiset.map Nat.cast (Multiset.map natDegree t)) = (Multiset.map degree t).sum
Tactic: rw [degree_eq_natDegree this, natDegree_multiset_prod_of_monic _ h, Nat.cast_multiset_sum,
    Multiset.map_map, Function.comp_def,
    Multiset.map_congr rfl (fun f hf => (degree_eq_natDegree (h f hf).ne_zero).symm)]