case h
𝓕 : Type ?u.747165
𝕜 : Type ?u.747168
α : Type ?u.747171
ι : Type ?u.747174
κ : Type ?u.747177
E : Type u_1
F : Type ?u.747183
G : Type ?u.747186
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 ⁻¹' sphere a r ↔ c ∈ sphere (a / b) r
𝓕 : Type ?u.747165
𝕜 : Type ?u.747168
α : Type ?u.747171
ι : Type ?u.747174
κ : Type ?u.747177
E : Type u_1
F : Type ?u.747183
G : Type ?u.747186
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 ⁻¹' sphere a r = sphere (a / b) r
ext c
no goals
case h
𝓕 : Type ?u.747165
𝕜 : Type ?u.747168
α : Type ?u.747171
ι : Type ?u.747174
κ : Type ?u.747177
E : Type u_1
F : Type ?u.747183
G : Type ?u.747186
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 ⁻¹' sphere a r ↔ c ∈ sphere (a / b) r
simp only [Set.mem_preimage, mem_sphere_iff_norm', div_div_eq_mul_div, mul_comm]