no goals
R : Type ?u.860119
R' : Type ?u.860122
𝕜 : Type u_1
𝕜₂ : Type ?u.860128
𝕜₃ : Type ?u.860131
𝕝 : Type ?u.860134
E : Type u_2
E₂ : Type ?u.860140
E₃ : Type ?u.860143
F : Type ?u.860146
G : Type ?u.860149
ι : Type ?u.860152
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ ball (p ⊔ q) e r = ball p e r ∩ ball q e r
simp_rw [ball, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_lt_iff]