no goals
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s / closedBall x δ = x⁻¹ • cthickening δ s
simp [div_eq_mul_inv, mul_comm, hs.mul_closedBall hδ]