ι : Type ?u.130494
α : Type u_1
β : Type ?u.130500
γ : Type ?u.130503
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ prod (map (Function.const α a) s) ≤ prod s
ι : Type ?u.130494
α : Type u_1
β : Type ?u.130500
γ : Type ?u.130503
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ a ^ ↑card s ≤ prod s
rw [← Multiset.prod_replicate, ← Multiset.map_const]
no goals
ι : Type ?u.130494
α : Type u_1
β : Type ?u.130500
γ : Type ?u.130503
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ prod (map (Function.const α a) s) ≤ prod s
exact prod_map_le_prod _ h