case h
𝓕 : Type ?u.1003367
𝕜 : Type ?u.1003370
α : Type ?u.1003373
ι : Type ?u.1003376
κ : Type ?u.1003379
E : Type u_1
F : Type ?u.1003385
G : Type ?u.1003388
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x✝ : E
⊢ x✝ ∈ a • closedBall b r ↔ x✝ ∈ closedBall (a • b) r
𝓕 : Type ?u.1003367
𝕜 : Type ?u.1003370
α : Type ?u.1003373
ι : Type ?u.1003376
κ : Type ?u.1003379
E : Type u_1
F : Type ?u.1003385
G : Type ?u.1003388
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ a • closedBall b r = closedBall (a • b) r
ext
no goals
case h
𝓕 : Type ?u.1003367
𝕜 : Type ?u.1003370
α : Type ?u.1003373
ι : Type ?u.1003376
κ : Type ?u.1003379
E : Type u_1
F : Type ?u.1003385
G : Type ?u.1003388
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x✝ : E
⊢ x✝ ∈ a • closedBall b r ↔ x✝ ∈ closedBall (a • b) r
simp [mem_closedBall, Set.mem_smul_set, dist_eq_norm_div, _root_.div_eq_inv_mul, ←
  eq_inv_mul_iff_mul_eq, mul_assoc]