case h
R : Type ?u.840053
R' : Type ?u.840056
𝕜 : Type u_1
𝕜₂ : Type ?u.840062
𝕜₃ : Type ?u.840065
𝕝 : Type ?u.840068
E : Type u_2
E₂ : Type ?u.840074
E₃ : Type ?u.840077
F : Type ?u.840080
G : Type ?u.840083
ι : Type ?u.840086
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝¹ y : E
r✝ : ℝ
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ x✝ ∈ ball (c • p) x r ↔ x✝ ∈ ball p x (r / ↑c)
R : Type ?u.840053
R' : Type ?u.840056
𝕜 : Type u_1
𝕜₂ : Type ?u.840062
𝕜₃ : Type ?u.840065
𝕝 : Type ?u.840068
E : Type u_2
E₂ : Type ?u.840074
E₃ : Type ?u.840077
F : Type ?u.840080
G : Type ?u.840083
ι : Type ?u.840086
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝ y : E
r✝ : ℝ
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x : E
⊢ ball (c • p) x r = ball p x (r / ↑c)
ext
no goals
case h
R : Type ?u.840053
R' : Type ?u.840056
𝕜 : Type u_1
𝕜₂ : Type ?u.840062
𝕜₃ : Type ?u.840065
𝕝 : Type ?u.840068
E : Type u_2
E₂ : Type ?u.840074
E₃ : Type ?u.840077
F : Type ?u.840080
G : Type ?u.840083
ι : Type ?u.840086
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝¹ y : E
r✝ : ℝ
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ x✝ ∈ ball (c • p) x r ↔ x✝ ∈ ball p x (r / ↑c)
rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
  lt_div_iff (NNReal.coe_pos.mpr hc)]