G : Type ?u.32897
M : Type u_2
N : Type ?u.32903
α : Sort u_1
β : Sort ?u.32909
ι : Sort ?u.32912
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ (∏ᶠ (i : α), f i) = ∏ᶠ (x : ?m.33452), 1

G : Type ?u.32897
M : Type u_2
N : Type ?u.32903
α : Sort u_1
β : Sort ?u.32909
ι : Sort ?u.32912
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ Sort ?u.33450
G : Type ?u.32897
M : Type u_2
N : Type ?u.32903
α : Sort u_1
β : Sort ?u.32909
ι : Sort ?u.32912
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ (∏ᶠ (i : α), f i) = 1
rw [← finprod_one]
case e_f
G : Type ?u.32897
M : Type u_2
N : Type ?u.32903
α : Sort u_1
β : Sort ?u.32909
ι : Sort ?u.32912
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ (fun i => f i) = fun x => 1
G : Type ?u.32897
M : Type u_2
N : Type ?u.32903
α : Sort u_1
β : Sort ?u.32909
ι : Sort ?u.32912
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ (∏ᶠ (i : α), f i) = ∏ᶠ (x : ?m.33452), 1

G : Type ?u.32897
M : Type u_2
N : Type ?u.32903
α : Sort u_1
β : Sort ?u.32909
ι : Sort ?u.32912
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ Sort ?u.33450
congr
no goals
case e_f
G : Type ?u.32897
M : Type u_2
N : Type ?u.32903
α : Sort u_1
β : Sort ?u.32909
ι : Sort ?u.32912
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ (fun i => f i) = fun x => 1
simp