case h₀
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ pure ≤ N B

case h₁
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G) (s : Set G), s ∈ N B a → ∃ t, t ∈ N B a ∧ t ⊆ s ∧ ∀ (a' : G), a' ∈ t → s ∈ N B a'
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ 𝓝 x₀ = N B x₀
rw [TopologicalSpace.nhds_mkOfNhds]
case h₀
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : U ∈ N B x
⊢ U ∈ pure x
case h₀
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ pure ≤ N B
intro x U U_in
case h₀
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : ∃ i, i ∈ B ∧ (fun y => x * y) '' i ⊆ U
⊢ U ∈ pure x
case h₀
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : U ∈ N B x
⊢ U ∈ pure x
rw [(B.hasBasis x).mem_iff] at U_in
case h₀.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
⊢ U ∈ pure x
case h₀
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : ∃ i, i ∈ B ∧ (fun y => x * y) '' i ⊆ U
⊢ U ∈ pure x
rcases U_in with ⟨V, V_in, H⟩
no goals
case h₀.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
⊢ U ∈ pure x
simpa [mem_pure] using H (mem_image_of_mem _ (GroupFilterBasis.one V_in))
case h₁
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : U ∈ N B x
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
case h₁
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G) (s : Set G), s ∈ N B a → ∃ t, t ∈ N B a ∧ t ⊆ s ∧ ∀ (a' : G), a' ∈ t → s ∈ N B a'
intro x U U_in
case h₁
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : ∃ i, i ∈ B ∧ (fun y => x * y) '' i ⊆ U
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
case h₁
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : U ∈ N B x
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
rw [(B.hasBasis x).mem_iff] at U_in
case h₁.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
case h₁
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : ∃ i, i ∈ B ∧ (fun y => x * y) '' i ⊆ U
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
rcases U_in with ⟨V, V_in, H⟩
case h₁.intro.intro.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
case h₁.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
rcases GroupFilterBasis.mul V_in with ⟨W, W_in, hW⟩
case h₁.intro.intro.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ (fun y => x * y) '' W ⊆ U ∧ ∀ (a' : G), a' ∈ (fun y => x * y) '' W → U ∈ N B a'
case h₁.intro.intro.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
use (fun y ↦ x * y) '' W, image_mem_map (FilterBasis.mem_filter_of_mem _ W_in)
case h₁.intro.intro.intro.intro.left
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ (fun y => x * y) '' W ⊆ U

case h₁.intro.intro.intro.intro.right
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ ∀ (a' : G), a' ∈ (fun y => x * y) '' W → U ∈ N B a'
case h₁.intro.intro.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ (fun y => x * y) '' W ⊆ U ∧ ∀ (a' : G), a' ∈ (fun y => x * y) '' W → U ∈ N B a'
constructor
case h₁.intro.intro.intro.intro.left
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : V ⊆ (fun y => x * y) ⁻¹' U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ W ⊆ (fun y => x * y) ⁻¹' U
case h₁.intro.intro.intro.intro.left
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ (fun y => x * y) '' W ⊆ U
rw [image_subset_iff] at H⊢
no goals
case h₁.intro.intro.intro.intro.left
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : V ⊆ (fun y => x * y) ⁻¹' U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ W ⊆ (fun y => x * y) ⁻¹' U
exact ((B.prod_subset_self W_in).trans hW).trans H
case h₁.intro.intro.intro.intro.right.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ U ∈ N B ((fun y => x * y) t)
case h₁.intro.intro.intro.intro.right
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ ∀ (a' : G), a' ∈ (fun y => x * y) '' W → U ∈ N B a'
rintro y ⟨t, tW, rfl⟩
case h₁.intro.intro.intro.intro.right.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ ∃ i, i ∈ B ∧ (fun y => (fun y => x * y) t * y) '' i ⊆ U
case h₁.intro.intro.intro.intro.right.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ U ∈ N B ((fun y => x * y) t)
rw [(B.hasBasis _).mem_iff]
case h₁.intro.intro.intro.intro.right.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ (fun y => (fun y => x * y) t * y) '' W ⊆ U
case h₁.intro.intro.intro.intro.right.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ ∃ i, i ∈ B ∧ (fun y => (fun y => x * y) t * y) '' i ⊆ U
use W, W_in
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ (fun y => (fun y => x * y) t * y) '' W ⊆ (fun y => x * y) '' V
case h₁.intro.intro.intro.intro.right.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ (fun y => (fun y => x * y) t * y) '' W ⊆ U
apply Subset.trans _ H
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ (fun y => (fun y => x * y) t * y) '' W ⊆ (fun y => x * y) '' V
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ (fun y => (fun y => x * y) t * y) '' W ⊆ (fun y => x * y) '' V
clear H
case intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
w : G
wW : w ∈ W
⊢ (fun y => (fun y => x * y) t * y) w ∈ (fun y => x * y) '' V
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ (fun y => (fun y => x * y) t * y) '' W ⊆ (fun y => x * y) '' V
rintro z ⟨w, wW, rfl⟩
no goals
case intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
w : G
wW : w ∈ W
⊢ (fun y => (fun y => x * y) t * y) w ∈ (fun y => x * y) '' V
exact ⟨t * w, hW (mul_mem_mul tW wW), by simp [mul_assoc]⟩
no goals
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
w : G
wW : w ∈ W
⊢ (fun y => x * y) (t * w) = (fun y => (fun y => x * y) t * y) w
simp [mul_assoc]