no goals
ι : Type u_1
α : Type ?u.18790
β : Type ?u.18793
M : Type ?u.18796
N : Type u_2
G : Type ?u.18802
k : Type ?u.18805
R : Type ?u.18808
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, 1 = 1
rw [prod_const_one]