case intro.intro
ι : Type ?u.161653
α : Type ?u.161656
X : Type ?u.161659
M : Type u_1
N : Type ?u.161665
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
ι : Type ?u.161653
α : Type ?u.161656
X : Type ?u.161659
M : Type u_1
N : Type ?u.161665
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
rcases exists_nhds_one_split hu with ⟨W, W1, h⟩
case intro.intro.intro.intro
ι : Type ?u.161653
α : Type ?u.161656
X : Type ?u.161659
M : Type u_1
N : Type ?u.161665
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
case intro.intro
ι : Type ?u.161653
α : Type ?u.161656
X : Type ?u.161659
M : Type u_1
N : Type ?u.161665
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩
case intro.intro.intro.intro
ι : Type ?u.161653
α : Type ?u.161656
X : Type ?u.161659
M : Type u_1
N : Type ?u.161665
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
⊢ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
case intro.intro.intro.intro
ι : Type ?u.161653
α : Type ?u.161656
X : Type ?u.161659
M : Type u_1
N : Type ?u.161665
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
use V, V1
case intro.intro.intro.intro
ι : Type ?u.161653
α : Type ?u.161656
X : Type ?u.161659
M : Type u_1
N : Type ?u.161665
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * w * s * t ∈ u
case intro.intro.intro.intro
ι : Type ?u.161653
α : Type ?u.161656
X : Type ?u.161659
M : Type u_1
N : Type ?u.161665
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
⊢ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
intro v w s t v_in w_in s_in t_in
no goals
case intro.intro.intro.intro
ι : Type ?u.161653
α : Type ?u.161656
X : Type ?u.161659
M : Type u_1
N : Type ?u.161665
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * w * s * t ∈ u
simpa only [mul_assoc] using h _ (h' v v_in w w_in) _ (h' s s_in t t_in)