case inl
ι : Type u_3
α : Type ?u.6427
β : Type ?u.6430
M : Type u_2
N : Type u_1
G : Type ?u.6439
k : Type ?u.6442
R : Type ?u.6445
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
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
hs : ∀ (i : ι), i ∈ ∅ → p (g i)
⊢ f (∏ i in ∅, g i) ≤ ∏ i in ∅, f (g i)

case inr
ι : Type u_3
α : Type ?u.6427
β : Type ?u.6430
M : Type u_2
N : Type u_1
G : Type ?u.6439
k : Type ?u.6442
R : Type ?u.6445
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
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 : ∀ (i : ι), i ∈ s → p (g i)
hs_nonempty : Finset.Nonempty s
⊢ f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι : Type u_3
α : Type ?u.6427
β : Type ?u.6430
M : Type u_2
N : Type u_1
G : Type ?u.6439
k : Type ?u.6442
R : Type ?u.6445
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
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 : ∀ (i : ι), i ∈ s → p (g i)
⊢ f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
no goals
case inl
ι : Type u_3
α : Type ?u.6427
β : Type ?u.6430
M : Type u_2
N : Type u_1
G : Type ?u.6439
k : Type ?u.6442
R : Type ?u.6445
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
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
hs : ∀ (i : ι), i ∈ ∅ → p (g i)
⊢ f (∏ i in ∅, g i) ≤ ∏ i in ∅, f (g i)
simp [h_one]
no goals
case inr
ι : Type u_3
α : Type ?u.6427
β : Type ?u.6430
M : Type u_2
N : Type u_1
G : Type ?u.6439
k : Type ?u.6442
R : Type ?u.6445
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
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 : ∀ (i : ι), i ∈ s → p (g i)
hs_nonempty : Finset.Nonempty s
⊢ f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs