case refine'_1
ι : Type u_1
α : Type ?u.33275
β : Type ?u.33278
M : Type ?u.33281
N : Type u_2
G : Type ?u.33287
k : Type ?u.33290
R : Type ?u.33293
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ ∀ (x : N), x ∈ Multiset.map f s.val → x ≤ n

case refine'_2
ι : Type u_1
α : Type ?u.33275
β : Type ?u.33278
M : Type ?u.33281
N : Type u_2
G : Type ?u.33287
k : Type ?u.33290
R : Type ?u.33293
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s
ι : Type u_1
α : Type ?u.33275
β : Type ?u.33278
M : Type ?u.33281
N : Type u_2
G : Type ?u.33287
k : Type ?u.33290
R : Type ?u.33293
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ Finset.prod s f ≤ n ^ card s
refine' (Multiset.prod_le_pow_card (s.val.map f) n _).trans _
no goals
case refine'_1
ι : Type u_1
α : Type ?u.33275
β : Type ?u.33278
M : Type ?u.33281
N : Type u_2
G : Type ?u.33287
k : Type ?u.33290
R : Type ?u.33293
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ ∀ (x : N), x ∈ Multiset.map f s.val → x ≤ n
simpa using h
case refine'_2
ι : Type u_1
α : Type ?u.33275
β : Type ?u.33278
M : Type ?u.33281
N : Type u_2
G : Type ?u.33287
k : Type ?u.33290
R : Type ?u.33293
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ n ^ ↑Multiset.card s.val ≤ n ^ card s
case refine'_2
ι : Type u_1
α : Type ?u.33275
β : Type ?u.33278
M : Type ?u.33281
N : Type u_2
G : Type ?u.33287
k : Type ?u.33290
R : Type ?u.33293
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s
simp
no goals
case refine'_2
ι : Type u_1
α : Type ?u.33275
β : Type ?u.33278
M : Type ?u.33281
N : Type u_2
G : Type ?u.33287
k : Type ?u.33290
R : Type ?u.33293
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ n ^ ↑Multiset.card s.val ≤ n ^ card s
rfl