-- Mathlib/Topology/Order.lean
theorem nhds_generateFrom {g : Set (Set α)} {a : α} :
    @nhds α (generateFrom g) a = ⨅ s ∈ { s | a ∈ s ∧ s ∈ g }, 𝓟 s

Proof state:
case intro.inter
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
hs : a ∈ s✝ → ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s✝
ht : a ∈ t✝ → ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 (s✝ ∩ t✝)

Tactic:
exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal

Result:
no goals

Proof state:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ ∀ i ∈ {s | a ∈ s ∧ IsOpen s}, ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 i

Tactic:
rintro s ⟨ha, hs⟩

Result:
case intro
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen s
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s

Proof state:
case intro.sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, GenerateOpen g s
hS : ∀ s ∈ S✝, a ∈ s → ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 (⋃₀ S✝)

Tactic:
let ⟨t, htS, hat⟩ := ha

Result:
case intro.sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, GenerateOpen g s
hS : ∀ s ∈ S✝, a ∈ s → ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
t : Set α
htS : t ∈ S✝
hat : a ∈ t
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 (⋃₀ S✝)

Proof state:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ ⨅ s ∈ {s | a ∈ s ∧ IsOpen s}, 𝓟 s = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s

Tactic:
refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) <| le_iInf₂ ?_

Result:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ ∀ i ∈ {s | a ∈ s ∧ IsOpen s}, ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 i

Proof state:
case intro.sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, GenerateOpen g s
hS : ∀ s ∈ S✝, a ∈ s → ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
t : Set α
htS : t ∈ S✝
hat : a ∈ t
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 (⋃₀ S✝)

Tactic:
exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)

Result:
no goals

Proof state:
case intro.basic
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ : Set α
hs : s✝ ∈ g
ha : a ∈ s✝
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s✝

Tactic:
exact iInf₂_le _ ⟨ha, hs⟩

Result:
no goals

Proof state:
case intro.univ
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ univ
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 univ

Tactic:
exact le_top.trans_eq principal_univ.symm

Result:
no goals

Proof state:
α : Type u
g : Set (Set α)
a : α
⊢ 𝓝 a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s

Tactic:
letI := generateFrom g

Result:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ 𝓝 a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s

Proof state:
case intro
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen s
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s

Tactic:
induction hs with
| basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
| univ => exact le_top.trans_eq principal_univ.symm
| inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
| sUnion _ _ hS =>
  let ⟨t, htS, hat⟩ := ha
  exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)

Result:
no goals

Proof state:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ 𝓝 a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s

Tactic:
rw [nhds_def]

Result:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ ⨅ s ∈ {s | a ∈ s ∧ IsOpen s}, 𝓟 s = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s