α : Type u_1
β : Type ?u.178136
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
x y : α
this : Embedding fun a => a * (y / x)
⊢ ((x, y) ∈ ⋂ (U : Set α) (_ : U ∈ 𝓝 1), (fun x => x.snd / x.fst) ⁻¹' U) ↔
    x / y ∈ (fun a => a * (y / x)) ⁻¹' closure ((fun a => a * (y / x)) '' {1})
α : Type u_1
β : Type ?u.178136
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
x y : α
this : Embedding fun a => a * (y / x)
⊢ (x, y) ∈ ⋂₀ (𝓤 α).sets ↔ x / y ∈ closure {1}
rw [this.closure_eq_preimage_closure_image, uniformity_eq_comap_nhds_one α, sInter_comap_sets]
no goals
α : Type u_1
β : Type ?u.178136
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
x y : α
this : Embedding fun a => a * (y / x)
⊢ ((x, y) ∈ ⋂ (U : Set α) (_ : U ∈ 𝓝 1), (fun x => x.snd / x.fst) ⁻¹' U) ↔
    x / y ∈ (fun a => a * (y / x)) ⁻¹' closure ((fun a => a * (y / x)) '' {1})
simp [mem_closure_iff_nhds, inter_singleton_nonempty, sub_eq_add_neg, add_assoc]