no goals
ι : Type u_1
α : Type ?u.136627
β : Type ?u.136630
M : Type u_2
N : Type ?u.136636
G : Type ?u.136639
k : Type ?u.136642
R : Type ?u.136645
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : ∀ (i : ι), i ∈ s → f i < 1
hs : Finset.Nonempty s
⊢ ∏ i in s, 1 ≤ 1
rw [prod_const_one]