case h
R : Type ?u.1261867
R' : Type ?u.1261870
𝕜 : Type u_1
𝕜₂ : Type ?u.1261876
𝕜₃ : Type ?u.1261879
𝕝 : Type ?u.1261882
E : Type u_2
E₂ : Type ?u.1261888
E₃ : Type ?u.1261891
F : Type ?u.1261894
G : Type ?u.1261897
ι : Type ?u.1261900
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝¹ : E
p : Seminorm 𝕜 E
r : ℝ
x x✝ : E
⊢ x✝ ∈ -ball p x r ↔ x✝ ∈ ball p (-x) r
R : Type ?u.1261867
R' : Type ?u.1261870
𝕜 : Type u_1
𝕜₂ : Type ?u.1261876
𝕜₃ : Type ?u.1261879
𝕝 : Type ?u.1261882
E : Type u_2
E₂ : Type ?u.1261888
E₃ : Type ?u.1261891
F : Type ?u.1261894
G : Type ?u.1261897
ι : Type ?u.1261900
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -ball p x r = ball p (-x) r
ext
no goals
case h
R : Type ?u.1261867
R' : Type ?u.1261870
𝕜 : Type u_1
𝕜₂ : Type ?u.1261876
𝕜₃ : Type ?u.1261879
𝕝 : Type ?u.1261882
E : Type u_2
E₂ : Type ?u.1261888
E₃ : Type ?u.1261891
F : Type ?u.1261894
G : Type ?u.1261897
ι : Type ?u.1261900
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝¹ : E
p : Seminorm 𝕜 E
r : ℝ
x x✝ : E
⊢ x✝ ∈ -ball p x r ↔ x✝ ∈ ball p (-x) r
rw [mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]