case h
𝓕 : Type ?u.1010449
𝕜 : Type ?u.1010452
α : Type ?u.1010455
ι : Type ?u.1010458
κ : Type ?u.1010461
E : Type u_1
F : Type ?u.1010467
G : Type ?u.1010470
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x✝ : E
⊢ x✝ ∈ a • ball b r ↔ x✝ ∈ ball (a • b) r
𝓕 : Type ?u.1010449
𝕜 : Type ?u.1010452
α : Type ?u.1010455
ι : Type ?u.1010458
κ : Type ?u.1010461
E : Type u_1
F : Type ?u.1010467
G : Type ?u.1010470
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ a • ball b r = ball (a • b) r
ext
no goals
case h
𝓕 : Type ?u.1010449
𝕜 : Type ?u.1010452
α : Type ?u.1010455
ι : Type ?u.1010458
κ : Type ?u.1010461
E : Type u_1
F : Type ?u.1010467
G : Type ?u.1010470
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x✝ : E
⊢ x✝ ∈ a • ball b r ↔ x✝ ∈ ball (a • b) r
simp [mem_ball, Set.mem_smul_set, dist_eq_norm_div, _root_.div_eq_inv_mul,
  ← eq_inv_mul_iff_mul_eq, mul_assoc]