case intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
ι : Type u_1
p : ι → Prop
t : ι → Set α
s : Set α
inst✝ : DiscreteTopology ↑s
x : α
hb : HasBasis (𝓝 x) p t
hx : x ∈ s
i : ι
hi : p i
hix : t i ∩ s ⊆ {x}
⊢ ∃ i, p i ∧ t i ∩ s = {x}
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
ι : Type u_1
p : ι → Prop
t : ι → Set α
s : Set α
inst✝ : DiscreteTopology ↑s
x : α
hb : HasBasis (𝓝 x) p t
hx : x ∈ s
⊢ ∃ i, p i ∧ t i ∩ s = {x}
rcases (nhdsWithin_hasBasis hb s).mem_iff.1 (singleton_mem_nhdsWithin_of_mem_discrete hx) with
  ⟨i, hi, hix⟩
no goals
case intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
ι : Type u_1
p : ι → Prop
t : ι → Set α
s : Set α
inst✝ : DiscreteTopology ↑s
x : α
hb : HasBasis (𝓝 x) p t
hx : x ∈ s
i : ι
hi : p i
hix : t i ∩ s ⊆ {x}
⊢ ∃ i, p i ∧ t i ∩ s = {x}
exact ⟨i, hi, hix.antisymm <| singleton_subset_iff.2 ⟨mem_of_mem_nhds <| hb.mem_of_mem hi, hx⟩⟩