α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Set G
hs : s ∈ 𝓝 1
this : (fun p => p.fst * p.snd⁻¹) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v / w ∈ s
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Set G
hs : s ∈ 𝓝 1
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v / w ∈ s
have : (fun p : G × G => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 ((1, 1) : G × G) :=
  continuousAt_fst.mul continuousAt_snd.inv (by simpa)
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Set G
hs : s ∈ 𝓝 1
this : (fun p => p.fst * p.snd⁻¹) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v / w ∈ s
simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] using
  this
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Set G
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 ((fun x => x.fst * x.snd⁻¹) (1, 1))
simpa