no goals
α : Type u_3
β : Type ?u.16880
A : Type ?u.16883
B : Type ?u.16886
M : Type u_1
N : Type u_2
P : Type ?u.16895
R : Type ?u.16898
S : Type ?u.16901
G : Type ?u.16904
M₀ : Type ?u.16907
G₀ : Type ?u.16910
ι : Sort ?u.16913
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M × N
⊢ mulSupport f = (mulSupport fun x => (f x).fst) ∪ mulSupport fun x => (f x).snd
simp only [← mulSupport_prod_mk, Prod.mk.eta]