no goals
ι : Type u_1
α : Type ?u.135473
β : Type ?u.135476
M : Type u_2
N : Type ?u.135482
G : Type ?u.135485
k : Type ?u.135488
R : Type ?u.135491
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : ∀ (i : ι), i ∈ s → 1 < f i
hs : Finset.Nonempty s
⊢ 1 ≤ ∏ i in s, 1
rw [prod_const_one]