case h
R : Type ?u.1183264
R' : Type ?u.1183267
𝕜 : Type u_1
𝕜₂ : Type ?u.1183273
𝕜₃ : Type ?u.1183276
𝕝 : Type ?u.1183279
E : Type u_2
E₂ : Type ?u.1183285
E₃ : Type ?u.1183288
F : Type ?u.1183291
G : Type ?u.1183294
ι : Type ?u.1183297
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ x✝ ∈ k • ball p 0 r ↔ x✝ ∈ ball p 0 (‖k‖ * r)
R : Type ?u.1183264
R' : Type ?u.1183267
𝕜 : Type u_1
𝕜₂ : Type ?u.1183273
𝕜₃ : Type ?u.1183276
𝕝 : Type ?u.1183279
E : Type u_2
E₂ : Type ?u.1183285
E₃ : Type ?u.1183288
F : Type ?u.1183291
G : Type ?u.1183294
ι : Type ?u.1183297
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
⊢ k • ball p 0 r = ball p 0 (‖k‖ * r)
ext
no goals
case h
R : Type ?u.1183264
R' : Type ?u.1183267
𝕜 : Type u_1
𝕜₂ : Type ?u.1183273
𝕜₃ : Type ?u.1183276
𝕝 : Type ?u.1183279
E : Type u_2
E₂ : Type ?u.1183285
E₃ : Type ?u.1183288
F : Type ?u.1183291
G : Type ?u.1183294
ι : Type ?u.1183297
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ x✝ ∈ k • ball p 0 r ↔ x✝ ∈ ball p 0 (‖k‖ * r)
rw [mem_smul_set_iff_inv_smul_mem₀ hk, p.mem_ball_zero, p.mem_ball_zero, map_smul_eq_mul,
  norm_inv, ← div_eq_inv_mul, div_lt_iff (norm_pos_iff.2 hk), mul_comm]