no goals
𝕜 : Type ?u.218373
E : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
⊢ Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y
rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]