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)) → Monic (Multiset.prod (Multiset.map f 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]
ht : ∀ (i : ι), i ∈ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f t))
revert 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]
⊢ (∀ (i : ι), i ∈ 0 → Monic (f i)) → Monic (Multiset.prod (Multiset.map f 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 : ι⦄ {s : Multiset ι},
    ((∀ (i : ι), i ∈ s → Monic (f i)) → Monic (Multiset.prod (Multiset.map f s))) →
      (∀ (i : ι), i ∈ a ::ₘ s → Monic (f i)) → Monic (Multiset.prod (Multiset.map f (a ::ₘ s)))
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)) → Monic (Multiset.prod (Multiset.map f t))
refine' t.induction_on _ _
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)) → Monic (Multiset.prod (Multiset.map f t))
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f (a ::ₘ 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 : ι⦄ {s : Multiset ι},
    ((∀ (i : ι), i ∈ s → Monic (f i)) → Monic (Multiset.prod (Multiset.map f s))) →
      (∀ (i : ι), i ∈ a ::ₘ s → Monic (f i)) → Monic (Multiset.prod (Multiset.map f (a ::ₘ s)))
intro a t ih ht
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)) → Monic (Multiset.prod (Multiset.map f t))
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (f a * 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)) → Monic (Multiset.prod (Multiset.map f t))
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f (a ::ₘ t)))
rw [Multiset.map_cons, Multiset.prod_cons]
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)) → Monic (Multiset.prod (Multiset.map f t))
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (f a * Multiset.prod (Multiset.map f t))
exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))
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]
⊢ (∀ (i : ι), i ∈ 0 → Monic (f i)) → Monic (Multiset.prod (Multiset.map f 0))
simp