-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.mem_nhds_iff {a : α} {s : Set α} {b : Set (Set α)}
    (hb : IsTopologicalBasis b) : s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Proof state:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]

Result:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ ⋃ i ∈ {s | a ∈ s ∧ s ∈ b}, (𝓟 i).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

case h
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ DirectedOn (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) {s | a ∈ s ∧ s ∈ b}

case ne
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ {s | a ∈ s ∧ s ∈ b}.Nonempty

Proof state:
case ne.intro.intro
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
i : Set α
h1 : i ∈ b
h2 : a ∈ i
⊢ {s | a ∈ s ∧ s ∈ b}.Nonempty

Tactic:
exact ⟨i, h2, h1⟩

Result:
no goals

Proof state:
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
⊢ ∃ z ∈ {s | a ∈ s ∧ s ∈ b}, (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) t z

Tactic:
let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩

Result:
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
u : Set α
hu₁ : u ∈ b
hu₂ : a ∈ u
hu₃ : u ⊆ s ∩ t
⊢ ∃ z ∈ {s | a ∈ s ∧ s ∈ b}, (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) t z

Proof state:
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
u : Set α
hu₁ : u ∈ b
hu₂ : a ∈ u
hu₃ : u ⊆ s ∩ t
⊢ ∃ z ∈ {s | a ∈ s ∧ s ∈ b}, (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) t z

Tactic:
exact ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),
  le_principal_iff.2 (hu₃.trans inter_subset_right)⟩

Result:
no goals

Proof state:
case h
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ DirectedOn (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) {s | a ∈ s ∧ s ∈ b}

Tactic:
rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩

Result:
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
⊢ ∃ z ∈ {s | a ∈ s ∧ s ∈ b}, (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun x1 x2 => x1 ≥ x2) t z

Proof state:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ ⋃ i ∈ {s | a ∈ s ∧ s ∈ b}, (𝓟 i).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
simp [and_assoc, and_left_comm]

Result:
no goals

Proof state:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Result:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Proof state:
case ne
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ {s | a ∈ s ∧ s ∈ b}.Nonempty

Tactic:
rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩

Result:
case ne.intro.intro
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
i : Set α
h1 : i ∈ b
h2 : a ∈ i
⊢ {s | a ∈ s ∧ s ∈ b}.Nonempty