no goals
α : Type u_1
β : Type ?u.15742
A : Type ?u.15745
B : Type ?u.15748
M : Type u_3
N : Type u_2
P : Type ?u.15757
R : Type ?u.15760
S : Type ?u.15763
G : Type ?u.15766
M₀ : Type ?u.15769
G₀ : Type ?u.15772
ι : Sort ?u.15775
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
g : α → N
x : α
⊢ (x ∈ mulSupport fun x => (f x, g x)) ↔ x ∈ mulSupport f ∪ mulSupport g
simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne.def]