no goals
α : Type u_1
β : Type u_2
A : Type ?u.17516
B : Type ?u.17519
M : Type u_3
N : Type ?u.17525
P : Type ?u.17528
R : Type ?u.17531
S : Type ?u.17534
G : Type ?u.17537
M₀ : Type ?u.17540
G₀ : Type ?u.17543
ι : Sort ?u.17546
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α × β → M
a : α
x : β
hx : x ∈ mulSupport fun b => f (a, b)
⊢ (a, x) ∈ mulSupport f ∧ (a, x).snd = x
simpa using hx