case intro.intro.intro
ι : Type ?u.166179
α : Type ?u.166182
X : Type ?u.166185
M : Type u_1
N : Type ?u.166191
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
ι : Type ?u.166179
α : Type ?u.166182
X : Type ?u.166185
M : Type u_1
N : Type ?u.166191
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
rcases exists_open_nhds_one_split hU with ⟨V, Vo, V1, hV⟩
case intro.intro.intro
ι : Type ?u.166179
α : Type ?u.166182
X : Type ?u.166185
M : Type u_1
N : Type ?u.166191
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
⊢ V * V ⊆ U
case intro.intro.intro
ι : Type ?u.166179
α : Type ?u.166182
X : Type ?u.166185
M : Type u_1
N : Type ?u.166191
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
use V, Vo, V1
case intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.166179
α : Type ?u.166182
X : Type ?u.166185
M : Type u_1
N : Type ?u.166191
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
x y : M
hx : x ∈ V
hy : y ∈ V
⊢ (fun x x_1 => x * x_1) x y ∈ U
case intro.intro.intro
ι : Type ?u.166179
α : Type ?u.166182
X : Type ?u.166185
M : Type u_1
N : Type ?u.166191
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
⊢ V * V ⊆ U
rintro _ ⟨x, y, hx, hy, rfl⟩
no goals
case intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.166179
α : Type ?u.166182
X : Type ?u.166185
M : Type u_1
N : Type ?u.166191
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
x y : M
hx : x ∈ V
hy : y ∈ V
⊢ (fun x x_1 => x * x_1) x y ∈ U
exact hV _ hx _ hy