G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ ∃ i, i ∈ B ∧ id i ⊆ U
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ U ∈ 𝓝 1
rw [B.nhds_one_hasBasis.mem_iff]
no goals
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ ∃ i, i ∈ B ∧ id i ⊆ U
exact ⟨U, hU, rfl.subset⟩