no goals
α : Type u_2
β : Type ?u.324567
ι : Type ?u.324570
G : Type ?u.324573
M : Type u_1
N : Type ?u.324579
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
⊢ (∏ᶠ (i : α) (_ : i ∈ ∅), f i) = 1
simp