ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ (∀ (a : α), a ∈ m → 0 ≤ a) → 0 ≤ prod m
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
h : ∀ (a : α), a ∈ m → 0 ≤ a
⊢ 0 ≤ prod m
revert h
case refine'_1
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ (∀ (a : α), a ∈ 0 → 0 ≤ a) → 0 ≤ prod 0

case refine'_2
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (a : α), a ∈ s → 0 ≤ a) → 0 ≤ prod s) → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → 0 ≤ a_2) → 0 ≤ prod (a ::ₘ s)
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ (∀ (a : α), a ∈ m → 0 ≤ a) → 0 ≤ prod m
refine' m.induction_on _ _
case refine'_2
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → 0 ≤ a) → 0 ≤ prod s
ih : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → 0 ≤ a_1
⊢ 0 ≤ prod (a ::ₘ s)
case refine'_2
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (a : α), a ∈ s → 0 ≤ a) → 0 ≤ prod s) → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → 0 ≤ a_2) → 0 ≤ prod (a ::ₘ s)
intro a s hs ih
case refine'_2
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → 0 ≤ a) → 0 ≤ prod s
ih : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → 0 ≤ a_1
⊢ 0 ≤ a * prod s
case refine'_2
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → 0 ≤ a) → 0 ≤ prod s
ih : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → 0 ≤ a_1
⊢ 0 ≤ prod (a ::ₘ s)
rw [prod_cons]
no goals
case refine'_2
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → 0 ≤ a) → 0 ≤ prod s
ih : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → 0 ≤ a_1
⊢ 0 ≤ a * prod s
exact mul_nonneg (ih _ <| mem_cons_self _ _) (hs fun a ha => ih _ <| mem_cons_of_mem ha)
case refine'_1
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ 0 ≤ prod 0
case refine'_1
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ (∀ (a : α), a ∈ 0 → 0 ≤ a) → 0 ≤ prod 0
rintro -
case refine'_1
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ 0 ≤ 1
case refine'_1
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ 0 ≤ prod 0
rw [prod_zero]
no goals
case refine'_1
ι : Type ?u.134844
α : Type u_1
β : Type ?u.134850
γ : Type ?u.134853
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ 0 ≤ 1
exact zero_le_one