ι : Type ?u.155162
α : Type ?u.155165
X : Type ?u.155168
M : Type u_1
N : Type ?u.155174
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
this : (fun a => a.fst * a.snd) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ s
ι : Type ?u.155162
α : Type ?u.155165
X : Type ?u.155168
M : Type u_1
N : Type ?u.155174
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ s
have : (fun a : M × M => a.1 * a.2) ⁻¹' s ∈ 𝓝 ((1, 1) : M × M) :=
  tendsto_mul (by simpa only [one_mul] using hs)
no goals
ι : Type ?u.155162
α : Type ?u.155165
X : Type ?u.155168
M : Type u_1
N : Type ?u.155174
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
this : (fun a => a.fst * a.snd) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ s
simpa only [prod_subset_iff] using exists_nhds_square this
no goals
ι : Type ?u.155162
α : Type ?u.155165
X : Type ?u.155168
M : Type u_1
N : Type ?u.155174
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 (1 * 1)
simpa only [one_mul] using hs