no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.172235
δ' : Type ?u.172238
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
inst✝¹ : UniformSpace δ
inst✝ : UniformSpace δ'
f : α × β → γ
⊢ UniformContinuous₂ (curry f) ↔ UniformContinuous f
rw [UniformContinuous₂, uncurry_curry]