no goals
R : Type ?u.1026847
R' : Type ?u.1026850
𝕜 : Type u_2
𝕜₂ : Type ?u.1026856
𝕜₃ : Type ?u.1026859
𝕝 : Type ?u.1026862
E : Type u_1
E₂ : Type ?u.1026868
E₃ : Type ?u.1026871
F : Type ?u.1026874
G : Type ?u.1026877
ι : Type ?u.1026880
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
⊢ closedBall p 0 r = ↑p ⁻¹' Metric.closedBall 0 r
rw [closedBall_zero_eq, preimage_metric_closedBall]