case h.e'_4
ι : Type u_1
α : Type ?u.152557
β : Type ?u.152560
M : Type ?u.152563
N : Type ?u.152566
G : Type ?u.152569
k : Type ?u.152572
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, 1 = 1
ι : Type u_1
α : Type ?u.152557
β : Type ?u.152560
M : Type ?u.152563
N : Type ?u.152566
G : Type ?u.152569
k : Type ?u.152572
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, f i ≤ 1
convert ← prod_le_prod h0 h1
no goals
case h.e'_4
ι : Type u_1
α : Type ?u.152557
β : Type ?u.152560
M : Type ?u.152563
N : Type ?u.152566
G : Type ?u.152569
k : Type ?u.152572
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, 1 = 1
exact Finset.prod_const_one