no goals
ι : Type u_1
α : Type ?u.16280
β : Type ?u.16283
M : Type ?u.16286
N : Type u_2
G : Type ?u.16292
k : Type ?u.16295
R : Type ?u.16298
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : ∀ (i : ι), i ∈ s → 1 ≤ f i
⊢ 1 ≤ ∏ i in s, 1
rw [prod_const_one]