no goals
R : Type ?u.1017930
R' : Type ?u.1017933
𝕜 : Type u_2
𝕜₂ : Type ?u.1017939
𝕜₃ : Type ?u.1017942
𝕝 : Type ?u.1017945
E : Type u_1
E₂ : Type ?u.1017951
E₃ : Type ?u.1017954
F : Type ?u.1017957
G : Type ?u.1017960
ι : Type ?u.1017963
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
⊢ ball p 0 r = ↑p ⁻¹' Metric.ball 0 r
rw [ball_zero_eq, preimage_metric_ball]