no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.11309
ι : Type ?u.11312
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
f : E →ₗ[𝕜] 𝕜
r : ℝ
⊢ Seminorm.ball (toSeminorm f) 0 r = {x | ‖↑f x‖ < r}
simp only [Seminorm.ball_zero_eq, toSeminorm_apply]