case h
𝓕 : Type ?u.743408
𝕜 : Type ?u.743411
α : Type ?u.743414
ι : Type ?u.743417
κ : Type ?u.743420
E : Type u_1
F : Type ?u.743426
G : Type ?u.743429
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b✝ b₁ b₂ : E
r✝ r₁ r₂ : ℝ
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x x_1 => x * x_1) b ⁻¹' ball a r ↔ c ∈ ball (a / b) r
𝓕 : Type ?u.743408
𝕜 : Type ?u.743411
α : Type ?u.743414
ι : Type ?u.743417
κ : Type ?u.743420
E : Type u_1
F : Type ?u.743426
G : Type ?u.743429
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b✝ b₁ b₂ : E
r✝ r₁ r₂ : ℝ
a b : E
r : ℝ
⊢ (fun x x_1 => x * x_1) b ⁻¹' ball a r = ball (a / b) r
ext c
no goals
case h
𝓕 : Type ?u.743408
𝕜 : Type ?u.743411
α : Type ?u.743414
ι : Type ?u.743417
κ : Type ?u.743420
E : Type u_1
F : Type ?u.743426
G : Type ?u.743429
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b✝ b₁ b₂ : E
r✝ r₁ r₂ : ℝ
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x x_1 => x * x_1) b ⁻¹' ball a r ↔ c ∈ ball (a / b) r
simp only [dist_eq_norm_div, Set.mem_preimage, mem_ball, div_div_eq_mul_div, mul_comm]