α : Type u_1
β : Type ?u.167207
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap (unop ∘ (fun x => x.snd / x.fst) ∘ fun p => (op p.fst, op p.snd)) (𝓝 1) = comap (fun x => x.fst⁻¹ * x.snd) (𝓝 1)
α : Type u_1
β : Type ?u.167207
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (fun x => x.fst⁻¹ * x.snd) (𝓝 1)
rw [← comap_uniformity_mulOpposite, uniformity_eq_comap_nhds_one, ← op_one, ← comap_unop_nhds,
  comap_comap, comap_comap]