no goals
R : Type ?u.882649
R' : Type ?u.882652
𝕜 : Type u_1
𝕜₂ : Type ?u.882658
𝕜₃ : Type ?u.882661
𝕝 : Type ?u.882664
E : Type u_2
E₂ : Type ?u.882670
E₃ : Type ?u.882673
F : Type ?u.882676
G : Type ?u.882679
ι : Type ?u.882682
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y✝ : E
r✝ : ℝ
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ x₁ - x₂ ∈ ball p y r ↔ x₁ ∈ ball p (x₂ + y) r
simp_rw [mem_ball, sub_sub]