exact hx y (by simp only [Function.mem_support, ne_eq] at hxy ⊢; exact hxy)
case left
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).1 ∈ s
no goals