case h₀.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ (fun x => FilterBasis.filter (B x)) x
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
⊢ n ∈ pure x

case h₁.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
⊢ ∃ t, t ∈ FilterBasis.filter (B x) ∧ t ⊆ n ∧ ∀ (a' : α), a' ∈ t → n ∈ FilterBasis.filter (B a')
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
⊢ 𝓝 a = FilterBasis.filter (B a)
rw [TopologicalSpace.nhds_mkOfNhds] <;> intro x n hn <;>
  obtain ⟨m, hm₁, hm₂⟩ := (B x).mem_filter_iff.mp hn
no goals
case h₀.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ (fun x => FilterBasis.filter (B x)) x
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
⊢ n ∈ pure x
exact hm₂ (h₀ _ _ hm₁)
case h₁.intro.intro.intro.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
n₁ : Set α
hn₁ : n₁ ∈ B x
hn₂ : n₁ ⊆ m
hn₃ : ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ m
⊢ ∃ t, t ∈ FilterBasis.filter (B x) ∧ t ⊆ n ∧ ∀ (a' : α), a' ∈ t → n ∈ FilterBasis.filter (B a')
case h₁.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
⊢ ∃ t, t ∈ FilterBasis.filter (B x) ∧ t ⊆ n ∧ ∀ (a' : α), a' ∈ t → n ∈ FilterBasis.filter (B a')
obtain ⟨n₁, hn₁, hn₂, hn₃⟩ := h₁ x m hm₁
case h₁.intro.intro.intro.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
n₁ : Set α
hn₁ : n₁ ∈ B x
hn₂ : n₁ ⊆ m
hn₃ : ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ m
x' : α
hx' : x' ∈ n₁
⊢ n ∈ FilterBasis.filter (B x')
case h₁.intro.intro.intro.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
n₁ : Set α
hn₁ : n₁ ∈ B x
hn₂ : n₁ ⊆ m
hn₃ : ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ m
⊢ ∃ t, t ∈ FilterBasis.filter (B x) ∧ t ⊆ n ∧ ∀ (a' : α), a' ∈ t → n ∈ FilterBasis.filter (B a')
refine'
  ⟨n₁, (B x).mem_filter_of_mem hn₁, hn₂.trans hm₂, fun x' hx' => (B x').mem_filter_iff.mp _⟩
case h₁.intro.intro.intro.intro.intro.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
n₁ : Set α
hn₁ : n₁ ∈ B x
hn₂ : n₁ ⊆ m
hn₃ : ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ m
x' : α
hx' : x' ∈ n₁
n₂ : Set α
hn₄ : n₂ ∈ B x'
hn₅ : n₂ ⊆ m
⊢ n ∈ FilterBasis.filter (B x')
case h₁.intro.intro.intro.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
n₁ : Set α
hn₁ : n₁ ∈ B x
hn₂ : n₁ ⊆ m
hn₃ : ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ m
x' : α
hx' : x' ∈ n₁
⊢ n ∈ FilterBasis.filter (B x')
obtain ⟨n₂, hn₄, hn₅⟩ := hn₃ x' hx'
no goals
case h₁.intro.intro.intro.intro.intro.intro.intro
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α) (n : Set α), n ∈ B x → x ∈ n
h₁ : ∀ (x : α) (n : Set α), n ∈ B x → ∃ n₁, n₁ ∈ B x ∧ n₁ ⊆ n ∧ ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ n
x : α
n : Set α
hn : n ∈ FilterBasis.filter (B x)
m : Set α
hm₁ : m ∈ B x
hm₂ : m ⊆ n
n₁ : Set α
hn₁ : n₁ ∈ B x
hn₂ : n₁ ⊆ m
hn₃ : ∀ (x' : α), x' ∈ n₁ → ∃ n₂, n₂ ∈ B x' ∧ n₂ ⊆ m
x' : α
hx' : x' ∈ n₁
n₂ : Set α
hn₄ : n₂ ∈ B x'
hn₅ : n₂ ⊆ m
⊢ n ∈ FilterBasis.filter (B x')
exact ⟨n₂, hn₄, hn₅.trans hm₂⟩