case refine'_1
ι : Type u_3
α : Type ?u.59
β : Type ?u.62
M : Type u_2
N : Type u_1
G : Type ?u.71
k : Type ?u.74
R : Type ?u.77
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ Multiset.map (fun i => g i) s.val ≠ ∅

case refine'_2
ι : Type u_3
α : Type ?u.59
β : Type ?u.62
M : Type u_2
N : Type u_1
G : Type ?u.71
k : Type ?u.74
R : Type ?u.77
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ ∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a

case refine'_3
ι : Type u_3
α : Type ?u.59
β : Type ?u.62
M : Type u_2
N : Type u_1
G : Type ?u.71
k : Type ?u.74
R : Type ?u.77
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
ι : Type u_3
α : Type ?u.59
β : Type ?u.62
M : Type u_2
N : Type u_1
G : Type ?u.71
k : Type ?u.74
R : Type ?u.77
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
refine' le_trans (Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ _ _) _
case refine'_3
ι : Type u_3
α : Type ?u.59
β : Type ?u.62
M : Type u_2
N : Type u_1
G : Type ?u.71
k : Type ?u.74
R : Type ?u.77
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
case refine'_3
ι : Type u_3
α : Type ?u.59
β : Type ?u.62
M : Type u_2
N : Type u_1
G : Type ?u.71
k : Type ?u.74
R : Type ?u.77
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
rw [Multiset.map_map]
no goals
case refine'_3
ι : Type u_3
α : Type ?u.59
β : Type ?u.62
M : Type u_2
N : Type u_1
G : Type ?u.71
k : Type ?u.74
R : Type ?u.77
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
rfl
no goals
case refine'_1
ι : Type u_3
α : Type ?u.59
β : Type ?u.62
M : Type u_2
N : Type u_1
G : Type ?u.71
k : Type ?u.74
R : Type ?u.77
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ Multiset.map (fun i => g i) s.val ≠ ∅
simp [hs_nonempty.ne_empty]
no goals
case refine'_2
ι : Type u_3
α : Type ?u.59
β : Type ?u.62
M : Type u_2
N : Type u_1
G : Type ?u.71
k : Type ?u.74
R : Type ?u.77
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ ∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a
exact Multiset.forall_mem_map_iff.mpr hs