-- Mathlib/Topology/Order.lean
theorem nhds_mkOfNhds_of_hasBasis {n : α → Filter α} {ι : α → Sort*} {p : ∀ a, ι a → Prop}
    {s : ∀ a, ι a → Set α} (hb : ∀ a, (n a).HasBasis (p a) (s a))
    (hpure : ∀ a i, p a i → a ∈ s a i) (hopen : ∀ a i, p a i → ∀ᶠ x in n a, s a i ∈ n x) (a : α) :
    @nhds α (.mkOfNhds n) a = n a

Proof state:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
⊢ U ∈ 𝓝 a

Tactic:
refine mem_nhds_iff.2 ⟨{x | U ∈ n x}, fun x hx ↦ hpure x hx, fun x hx ↦ ?_, hU⟩

Result:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : x ∈ {x | U ∈ n x}
⊢ {x | U ∈ n x} ∈ n x

Proof state:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : x ∈ {x | U ∈ n x}
⊢ {x | U ∈ n x} ∈ n x

Tactic:
rcases (hb x).mem_iff.1 hx with ⟨i, hpi, hi⟩

Result:
case a.intro.intro
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : x ∈ {x | U ∈ n x}
i : ι x
hpi : p x i
hi : s x i ⊆ U
⊢ {x | U ∈ n x} ∈ n x

Proof state:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
⊢ 𝓝 a = n a

Tactic:
let t : TopologicalSpace α := .mkOfNhds n

Result:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ 𝓝 a = n a

Proof state:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ n a ≤ 𝓝 a

Tactic:
exact (nhds_basis_opens a).ge_iff.2 fun U ⟨haU, hUo⟩ ↦ hUo a haU

Result:
no goals

Proof state:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
⊢ U ∈ 𝓝 a

Tactic:
replace hpure : pure ≤ n := fun x ↦ (hb x).ge_iff.2 (hpure x)

Result:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
⊢ U ∈ 𝓝 a

Proof state:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ 𝓝 a ≤ n a

Tactic:
intro U hU

Result:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
⊢ U ∈ 𝓝 a

Proof state:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ 𝓝 a = n a

Tactic:
apply le_antisymm

Result:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ 𝓝 a ≤ n a

case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ n a ≤ 𝓝 a

Proof state:
case a.intro.intro
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : x ∈ {x | U ∈ n x}
i : ι x
hpi : p x i
hi : s x i ⊆ U
⊢ {x | U ∈ n x} ∈ n x

Tactic:
exact (hopen x i hpi).mono fun y hy ↦ mem_of_superset hy hi

Result:
no goals