no goals
α : Type u_1
β : Type u_2
γ : Type ?u.69629
δ : Type ?u.69632
ε : Type ?u.69635
ι : Type ?u.69638
f : α →. β
x✝¹ x✝ : α × β
⊢ x✝ ∈ prodMap (PFun.id α) (PFun.id β) x✝¹ ↔ x✝ ∈ PFun.id (α × β) x✝¹
simp [eq_comm]