[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
x : α
⊢ x ∈ (fun a => f (↑E.symm a)) ((fun x => ↑E (T x)) x)
[PROOFSTEP]
simpa using h₁ x
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ (fun a => f (↑E.symm a)) a ∩ (fun a => f (↑E.symm a)) b
⊢ x ∈ (fun a => f (↑E.symm a)) ((fun a b x h => ↑E (I (↑E.symm a) (↑E.symm b) x h)) a b x h)
[PROOFSTEP]
simpa using h₂ (E.symm a) (E.symm b) x h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ (fun a => f (↑E.symm a)) a ∩ (fun a => f (↑E.symm a)) b
⊢ (fun a => f (↑E.symm a)) ((fun a b x h => ↑E (I (↑E.symm a) (↑E.symm b) x h)) a b x h) ⊆
    (fun a => f (↑E.symm a)) a ∩ (fun a => f (↑E.symm a)) b
[PROOFSTEP]
simpa using h₃ (E.symm a) (E.symm b) x h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F✝ : Ctop α σ
E : σ ≃ τ
F : Ctop α σ
a : τ
⊢ f (ofEquiv E F) a = f F (↑E.symm a)
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
a : τ
f✝ : σ → Set α
top✝ : α → σ
top_mem✝ : ∀ (x : α), x ∈ f✝ (top✝ x)
inter✝ : (a b : σ) → (x : α) → x ∈ f✝ a ∩ f✝ b → σ
inter_mem✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), x ∈ f✝ (inter✝ a b x h)
inter_sub✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), f✝ (inter✝ a b x h) ⊆ f✝ a ∩ f✝ b
⊢ f
      (ofEquiv E
        { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝,
          inter_sub := inter_sub✝ })
      a =
    f { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝, inter_sub := inter_sub✝ }
      (↑E.symm a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
T : TopologicalSpace α
F : Realizer α
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
[PROOFSTEP]
have := toTopsp_isTopologicalBasis F.F
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
[PROOFSTEP]
rwa [F.eq] at this 
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
[PROOFSTEP]
have := @mem_nhds_toTopsp _ _ F.F s a
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
[PROOFSTEP]
rwa [F.eq] at this 
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ (¬a ∈ s → ∃ b, a ∈ f F.F b ∧ ∀ (z : α), z ∈ f F.F b → ¬z ∈ s) ↔
    (∀ (b : F.σ), a ∈ f F.F b → ∃ z, z ∈ f F.F b ∩ s) → a ∈ s
[PROOFSTEP]
haveI := Classical.propDecidable
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬a ∈ s → ∃ b, a ∈ f F.F b ∧ ∀ (z : α), z ∈ f F.F b → ¬z ∈ s) ↔
    (∀ (b : F.σ), a ∈ f F.F b → ∃ z, z ∈ f F.F b ∩ s) → a ∈ s
[PROOFSTEP]
rw [not_imp_comm]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬∃ b, a ∈ f F.F b ∧ ∀ (z : α), z ∈ f F.F b → ¬z ∈ s) → a ∈ s ↔
    (∀ (b : F.σ), a ∈ f F.F b → ∃ z, z ∈ f F.F b ∩ s) → a ∈ s
[PROOFSTEP]
simp [not_exists, not_and, not_forall, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
s : F.σ
a : α
m : a ∈ f F.F s
⊢ 𝓝 a ≤ 𝓟 (f F.F s)
[PROOFSTEP]
simpa using F.mem_nhds.2 ⟨s, m, Subset.refl _⟩
[GOAL]
α : Type u_1
β : Type u_2
σ✝ : Type u_3
τ : Type u_4
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
⊢ toTopsp F = T
[PROOFSTEP]
refine' eq_of_nhds_eq_nhds fun x ↦ _
[GOAL]
α : Type u_1
β : Type u_2
σ✝ : Type u_3
τ : Type u_4
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
x : α
⊢ 𝓝 x = 𝓝 x
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
β : Type u_2
σ✝ : Type u_3
τ : Type u_4
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x
[PROOFSTEP]
rw [mem_nhds_toTopsp, H]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s✝ : Set α
x✝ : ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s✝
s : F.σ
h : a ∈ f F.F s ∧ f F.F s ⊆ s✝
⊢ a ∈ f (Ctop.ofEquiv E F.F) (↑E s) ∧ f (Ctop.ofEquiv E F.F) (↑E s) ⊆ s✝
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s : Set α
x✝ : ∃ b, a ∈ f (Ctop.ofEquiv E F.F) b ∧ f (Ctop.ofEquiv E F.F) b ⊆ s
t : τ
h : a ∈ f (Ctop.ofEquiv E F.F) t ∧ f (Ctop.ofEquiv E F.F) t ⊆ s
⊢ a ∈ f F.F (↑E.symm t) ∧ f F.F (↑E.symm t) ⊆ s
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ f (ofEquiv F E).F s = f F.F (↑E.symm s)
[PROOFSTEP]
delta ofEquiv
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ f { σ := τ, F := Ctop.ofEquiv E F.F, eq := (_ : toTopsp (Ctop.ofEquiv E F.F) = inst✝) }.F s = f F.F (↑E.symm s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
⊢ { a // a ∈ ∅ ∧ 𝓝 a ⊓ f ≠ ⊥ }
[PROOFSTEP]
suffices : f = ⊥
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
this : f = ⊥
⊢ { a // a ∈ ∅ ∧ 𝓝 a ⊓ f ≠ ⊥ }
case this
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
⊢ f = ⊥
[PROOFSTEP]
exact absurd this h
[GOAL]
case this
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
⊢ f = ⊥
[PROOFSTEP]
rw [← F.eq, eq_bot_iff]
[GOAL]
case this
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : Filter.Realizer f
x : F.σ
h : f ≠ ⊥
hF : CFilter.f F.F x ⊆ ∅
⊢ CFilter.toFilter F.F ≤ ⊥
[PROOFSTEP]
exact λ s _ ↦ ⟨x, hF.trans s.empty_subset⟩
