R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
h : ∀ (i : ι), i ∈ t → Monic (f i)
⊢ nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
revert h
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ 0 → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f 0)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) 0)

case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ nextCoeff (Multiset.prod (Multiset.map f (a ::ₘ t))) =
    Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) (a ::ₘ t))
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
refine' Multiset.induction_on t _ fun a t ih ht => _
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff 1 = 0
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ 0 → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f 0)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) 0)
simp only [Multiset.not_mem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero,
  Multiset.prod_zero, Multiset.sum_zero, not_false_iff, forall_true_iff]
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff (↑C 1) = 0
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff 1 = 0
rw [← C_1]
no goals
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff (↑C 1) = 0
rw [nextCoeff_C_eq_zero]
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ ∀ (i : ι), i ∈ t → Monic (f i)

case refine'_2.hp
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (f a)

case refine'_2.hq
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f t))
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ nextCoeff (Multiset.prod (Multiset.map f (a ::ₘ t))) =
    Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) (a ::ₘ t))
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
  Monic.nextCoeff_mul, ih]
no goals
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ ∀ (i : ι), i ∈ t → Monic (f i)

case refine'_2.hp
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (f a)

case refine'_2.hq
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f t))
exacts [fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _),
  monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)]