G : Type ?u.30331
M : Type u_1
N : Type ?u.30337
α : Sort u_2
β : Sort ?u.30343
ι : Sort ?u.30346
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
this : (mulSupport fun x => (fun x => 1) x.down) ⊆ ↑∅
⊢ (∏ᶠ (x : α), 1) = 1
G : Type ?u.30331
M : Type u_1
N : Type ?u.30337
α : Sort u_2
β : Sort ?u.30343
ι : Sort ?u.30346
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
⊢ (∏ᶠ (x : α), 1) = 1
have : (mulSupport fun x : PLift α => (fun _ => 1 : α → M) x.down) ⊆ (∅ : Finset (PLift α)) :=
  fun x h => by simp at h
no goals
G : Type ?u.30331
M : Type u_1
N : Type ?u.30337
α : Sort u_2
β : Sort ?u.30343
ι : Sort ?u.30346
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
this : (mulSupport fun x => (fun x => 1) x.down) ⊆ ↑∅
⊢ (∏ᶠ (x : α), 1) = 1
rw [finprod_eq_prod_pLift_of_mulSupport_subset this, Finset.prod_empty]
no goals
G : Type ?u.30331
M : Type u_1
N : Type ?u.30337
α : Sort u_2
β : Sort ?u.30343
ι : Sort ?u.30346
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x : PLift α
h : x ∈ mulSupport fun x => (fun x => 1) x.down
⊢ x ∈ ↑∅
simp at h