case h
ι : Type ?u.120163
α : Type u_1
β : Type ?u.120169
γ : Type ?u.120172
inst✝ : OrderedCommMonoid α
s t : Multiset α
a n : α
a✝ : List α
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x ≤ n
⊢ prod (Quotient.mk (List.isSetoid α) a✝) ≤ n ^ ↑card (Quotient.mk (List.isSetoid α) a✝)
ι : Type ?u.120163
α : Type u_1
β : Type ?u.120169
γ : Type ?u.120172
inst✝ : OrderedCommMonoid α
s✝ t : Multiset α
a : α
s : Multiset α
n : α
h : ∀ (x : α), x ∈ s → x ≤ n
⊢ prod s ≤ n ^ ↑card s
induction s using Quotient.inductionOn
no goals
case h
ι : Type ?u.120163
α : Type u_1
β : Type ?u.120169
γ : Type ?u.120172
inst✝ : OrderedCommMonoid α
s t : Multiset α
a n : α
a✝ : List α
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x ≤ n
⊢ prod (Quotient.mk (List.isSetoid α) a✝) ≤ n ^ ↑card (Quotient.mk (List.isSetoid α) a✝)
simpa using List.prod_le_pow_card _ _ h