α : Type u_1
β : Type ?u.8619
σ : Type ?u.8622
τ : Type ?u.8625
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
α : Type u_1
β : Type ?u.8619
σ : Type ?u.8622
τ : Type ?u.8625
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
haveI := Classical.propDecidable
α : Type u_1
β : Type ?u.8619
σ : Type ?u.8622
τ : Type ?u.8625
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
α : Type u_1
β : Type ?u.8619
σ : Type ?u.8622
τ : Type ?u.8625
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
rw [not_imp_comm]
no goals
α : Type u_1
β : Type ?u.8619
σ : Type ?u.8622
τ : Type ?u.8625
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
simp [not_exists, not_and, not_forall, and_comm]