compact_t2_open_filters.lean

import topology.separation

open_locale filter topological_space

variables {α : Type*} [topological_space α]

def nhds_principal (s : set α) : filter α :=
⨅ (s' ∈ {t : set α | s ⊆ t ∧ is_open t}), 𝓟 s'

notation `𝓝'` := nhds_principal

def filter.is_open (f : filter α) : Prop := ∀ s ∈ f, ∃ (u ∈ f), is_open u ∧ u ⊆ s

lemma filter.is_open.le_iff {f g : filter α} (hf : f.is_open) (hg : g.is_open) :
  f ≤ g ↔ ∀ (V ∈ g), is_open V → ∃ (U ∈ f), is_open U ∧ U ⊆ V :=
begin
  split,
  { intros h V hV hVo,
    exact ⟨V, h hV, hVo, rfl.subset⟩, },
  { intros h s hs,
    obtain ⟨V, hV, hVo, hVs⟩ := hg _ hs,
    obtain ⟨U, hU, hUo, hUV⟩ := h V hV hVo,
    exact filter.mem_of_superset hU (hUV.trans hVs), },
end

lemma filter.is_open.ext {f g : filter α} (hf : f.is_open) (hg : g.is_open)
  (h : ∀ (u : set α), is_open u → (u ∈ f ↔ u ∈ g)) : f = g :=
begin
  apply le_antisymm,
  rw hf.le_iff hg, intros u hu huo, use u, simp [h u huo, *],
  rw hg.le_iff hf, intros u hu huo, use u, simp [(h u huo).symm, *],
end

lemma nhds_principal_basis_opens (s : set α) :
  (𝓝' s).has_basis (λ (s' : set α), s ⊆ s' ∧ is_open s') (λ s', s') :=
begin
  rw nhds_principal,
  apply filter.has_basis_binfi_principal,
  { rintro s' ⟨has, hs⟩ t' ⟨hat, ht⟩,
    refine ⟨s' ∩ t', ⟨set.subset_inter has hat, is_open.inter hs ht⟩,
      set.inter_subset_left _ _, set.inter_subset_right _ _⟩ },
  { exact ⟨set.univ, set.subset_univ _, is_open_univ⟩, }
end

lemma le_nhds_principal_iff {f} {s : set α} :
  f ≤ 𝓝' s ↔ ∀ s' : set α, s ⊆ s' → is_open s' → s' ∈ f :=
by simp [nhds_principal]

lemma nhds_principal_le_of_le {f} {s s' : set α} (h : s ⊆ s') (o : is_open s')
  (sf : 𝓟 s' ≤ f) : 𝓝' s ≤ f :=
by { rw nhds_principal, exact infi_le_of_le s' (infi_le_of_le ⟨h, o⟩ sf) }

lemma mem_nhds_principal_iff {s s' : set α} :
  s' ∈ 𝓝' s ↔ ∃ t ⊆ s', is_open t ∧ s ⊆ t :=
(nhds_principal_basis_opens s).mem_iff.trans
⟨λ ⟨t, ⟨hat, ht⟩, hts⟩, ⟨t, hts, ht, hat⟩, λ ⟨t, hts, ht, hat⟩, ⟨t, ⟨hat, ht⟩, hts⟩⟩

@[simp]
lemma mem_nhds_principal_iff_of_is_open {s s' : set α} (hs' : is_open s') :
  s' ∈ 𝓝' s ↔ s ⊆ s' :=
begin
  rw mem_nhds_principal_iff,
  split,
  { rintro ⟨t, ht, hto, h⟩,
    exact h.trans ht, },
  { intro h,
    refine ⟨s', rfl.subset, hs', h⟩, },
end

@[simp] lemma nhds_principal.is_open (s : set α) : (𝓝' s).is_open :=
begin
  intros s',
  simp [mem_nhds_principal_iff],
  intros t ht hto hst,
  exact ⟨t, ⟨t, rfl.subset, hto, hst⟩, hto, ht⟩,
end

lemma filter.is_open.le_nhds_principal_of_is_open {f : filter α} (hf : f.is_open) (s : set α) (hs : is_open s) :
  f ≤ 𝓝' s ↔ s ∈ f :=
begin
  rw hf.le_iff (nhds_principal.is_open _),
  split,
  { intro h,
    obtain ⟨U, hU, hUo, h⟩ := h s (by simp [hs]) hs,
    exact filter.mem_of_superset hU h, },
  { intros hf V hV hVo,
    simp [hVo] at hV,
    exact ⟨s, hf, hs, hV⟩ },
end

@[mono]
lemma nhds_principal.mono {s t : set α} (h : s ⊆ t) : 𝓝' s ≤ 𝓝' t :=
begin
  intros s',
  simp [mem_nhds_principal_iff],
  intros t' ht' ht'o htt',
  exact ⟨t', ht', ht'o, h.trans htt'⟩,
end

lemma nhds_eq_nhds_principal {a : α} : 𝓝 a = 𝓝' {a} :=
by { ext s, simp [mem_nhds_iff, mem_nhds_principal_iff] }

@[simp] lemma nhds.is_open (x : α) : (𝓝 x).is_open :=
by simp [nhds_eq_nhds_principal]

lemma nhds_le_nhds_principal_of_mem {s : set α} {a : α} (h : a ∈ s) : 
  𝓝 a ≤ 𝓝' s :=
begin
  rw nhds_eq_nhds_principal,
  mono,
  rwa set.singleton_subset_iff,
end

lemma nhds_principal_eq_supr (s : set α) :
  𝓝' s = ⨆ a ∈ s, 𝓝 a :=
begin
  ext u,
  simp,
  split,
  { intros h x hx,
    revert h u,
    change 𝓝 x ≤ _,
    exact nhds_le_nhds_principal_of_mem hx, },
  { intro h,
    simp [mem_nhds_iff] at h,
    choose f h h' h'' using h,
    simp [mem_nhds_principal_iff],
    use ⋃ i (h : i ∈ s), f i h,
    split,
    { simp [h], },
    split,
    { apply is_open_Union,
      intro x,
      apply is_open_Union,
      apply h', },
    { intros x hx,
      simp,
      exact ⟨x, hx, h'' _ _⟩, } },
end

lemma subset_of_mem_nhds_principal {s s' : set α} (h : s' ∈ 𝓝' s) : s ⊆ s' :=
begin
  rw mem_nhds_principal_iff at h,
  obtain ⟨t, ht, hto, hst⟩ := h,
  exact hst.trans ht,
end

lemma nhds_principal_union {s s' : set α} : 𝓝' (s ∪ s') = 𝓝' s ⊔ 𝓝' s' :=
begin
  ext t,
  simp [mem_nhds_principal_iff],
  split,
  { rintro ⟨a, ha, hoa, ha', ha''⟩,
    exact ⟨⟨a, ha, hoa, ha'⟩, ⟨a, ha, hoa, ha''⟩⟩, },
  { rintro ⟨⟨a, ha, hoa, ha'⟩, ⟨b, hb, hob, hb'⟩⟩,
    exact ⟨a ∪ b, set.union_subset ha hb, is_open.union hoa hob,
      set.subset_union_of_subset_left ha' b, set.subset_union_of_subset_right hb' a⟩, },
end

lemma nhds_principal_Union {ι : Type*} (s : ι → set α) : 𝓝' (⋃ i, s i) = ⨆ i, 𝓝' (s i) :=
begin
  ext t,
  simp [mem_nhds_principal_iff],
  split,
  { rintro ⟨t',ht',hto',h⟩ i,
    exact ⟨_, ht', hto', h _⟩, },
  { intro h,
    choose f h' h'' h''' using h,
    use ⋃ i, f i,
    split,
    { intro x,
      simp,
      intro i,
      apply h', },
    split,
    { exact is_open_Union h'', },
    { intro i,
      refine (h''' i).trans (set.subset_Union f i), }, },
end

@[simp] lemma nhds_principal_empty : 𝓝' (∅ : set α) = ⊥ :=
begin
  ext,
  simp [mem_nhds_principal_iff],
  use ∅,
  simp,
end

@[simp] lemma nhds_principal_univ : 𝓝' (set.univ : set α) = ⊤ :=
begin
  rw ← top_le_iff,
  intro u,
  simp [mem_nhds_principal_iff, set.univ_subset_iff],
end

lemma filter.is_open.sup {f g : filter α} (hf : f.is_open) (hg : g.is_open) :
  (f ⊔ g).is_open :=
begin
  intros u,
  simp,
  intros huf hug,
  obtain ⟨c, hc, hco, hca⟩ := hf _ huf,
  obtain ⟨d, hd, hdo, hdb⟩ := hg _ hug,
  refine ⟨c ∪ d, ⟨_, _⟩, hco.union hdo, set.union_subset hca hdb⟩,
  exact filter.mem_of_superset hc (set.subset_union_left c d),
  exact filter.mem_of_superset hd (set.subset_union_right c d),
end

lemma filter.is_open.supr {ι : Type*} {f : ι → filter α} (hf : ∀ i, (f i).is_open) :
  (⨆ i, f i).is_open :=
begin
  intro u,
  simp,
  intro hu,
  have : ∀ i, ∃ v ∈ f i, is_open v ∧ v ⊆ u := λ i, hf i _ (hu i),
  choose g h h' h'' using this,
  refine ⟨⋃ i, g i, _, _, _⟩,
  { intro i,
    exact filter.mem_of_superset (h i) (set.subset_Union g i) },
  { exact is_open_Union h' },
  { simp [h''] },
end

lemma filter.mem_inf_of_open {f g : filter α} (hf : f.is_open) (hg : g.is_open) {s : set α} :
  s ∈ f ⊓ g ↔ ∃ (u v : set α), is_open u ∧ u ∈ f ∧ is_open v ∧ v ∈ g ∧ u ∩ v ⊆ s :=
begin
  split,
  { intro h,
    rw filter.mem_inf_iff at h,
    obtain ⟨a, ha, b, hb, rfl⟩ := h,
    obtain ⟨c, hc, hco, hca⟩ := hf _ ha,
    obtain ⟨d, hd, hdo, hdb⟩ := hg _ hb,
    exact ⟨c, d, hco, hc, hdo, hd, set.inter_subset_inter hca hdb⟩, },
  { rintro ⟨u, v, huo, hu, hvo, hv, h⟩,
    rw filter.mem_inf_iff,
    refine ⟨u ∪ s, _, v ∪ s, _, _⟩,
    exact filter.mem_of_superset hu (set.subset_union_left _ _),
    exact filter.mem_of_superset hv (set.subset_union_left _ _),
    ext x,
    split, simp { contextual := tt },
    simp, rintro (h1|h1) (h2|h2); try { assumption }, exact h ⟨h1, h2⟩, },
end

lemma filter.is_open.inf {f g : filter α} (hf : f.is_open) (hg : g.is_open) :
  (f ⊓ g).is_open :=
begin
  intros u h,
  rw filter.mem_inf_of_open hf hg at h,
  obtain ⟨u, v, huo, hu, hvo, hv, h⟩ := h,
  refine ⟨u ∩ v, _, huo.inter hvo, h⟩,
  rw filter.mem_inf_of_open hf hg,
  refine ⟨u, v, huo, hu, hvo, hv, rfl.subset⟩,
end

@[simp] lemma filter.top_is_open : (⊤ : filter α).is_open :=
by { intro u, simp { contextual := tt } }

@[simp] lemma filter.bot_is_open : (⊥ : filter α).is_open :=
by { intro u, simp, use ∅, simp, }

lemma filter.is_open.infi_finite {ι : Type*} (f : ι → filter α) (t : finset ι)
  (hf : ∀ i ∈ t, (f i).is_open) :
  (⨅ (i ∈ t), f i).is_open :=
begin
  classical,
  induction t using finset.induction with k t hkt h,
  { simp, },
  { rw [finset.infi_insert],
    apply filter.is_open.inf,
    { apply hf, simp, },
    { apply h,
      intros i hi,
      apply hf,
      simp [hi], } },
end

-- true in more generality of course
lemma filter.infi_le_binfi {ι : Type*} (f : ι → filter α) (t : finset ι) :
  (⨅ (a : ι), f a) ≤ (⨅ (a : ι) (H : a ∈ t), f a) :=
begin
  classical,
  induction t using finset.induction with k t hkt h,
  { simp, },
  { rw [finset.infi_insert],
    simp [h],
    apply infi_le f k, },
end

-- true for `directed (≥) f` too
lemma filter.is_open.infi_of_is_chain {ι : Type*} (f : ι → filter α)
  (hf : ∀ i, (f i).is_open) (hd : is_chain (≤) (set.range f)) :
  (⨅ i, f i).is_open :=
begin
  classical,
  intros u hu,
  rw filter.mem_infi_finite at hu,
  obtain ⟨t, hu⟩ := hu,
  by_cases ht : t.nonempty,
  { rw [← finset.inf_eq_infi, ← finset.inf'_eq_inf ht] at hu,
    have : ∃ i, i ∈ t ∧ t.inf' ht (λ (a : ι), f a) = f i,
    { clear hu u hf,
      induction t using finset.induction with k t hkt h,
      { simpa using ht, },
      by_cases ht' : t.nonempty,
      { obtain ⟨j, hj, h⟩ := h ht',
        obtain (hk|hk) := hd.total (set.mem_range_self k : f k ∈ set.range f) (set.mem_range_self j : f j ∈ set.range f),
        { use k,
          simp [finset.inf'_insert ht'],
          intros,
          apply hk.trans,
          rw ← h,
          apply finset.inf'_le _ H, },
        { use j,
          simp [hj, finset.inf'_insert ht'],
          rw ← h,
          simp,
          refine le_trans _ hk,
          apply finset.inf'_le _ hj, }, },
      { simp at ht',
        subst t,
        simp, } },
    obtain ⟨i, hi, hinf⟩ := this,
    rw hinf at hu,
    obtain ⟨v, hv, hvo, hvu⟩ := hf i _ hu,
    refine ⟨v, _, hvo, hvu⟩,
    rw [finset.inf'_eq_inf, finset.inf_eq_infi] at hinf,
    have := filter.infi_le_binfi f t,
    rw hinf at this,
    exact this hv, },
  { simp at ht,
    subst t,
    simp at hu,
    subst u,
    use set.univ,
    simp, },
end


lemma filter.directed_nhds_principal {ι : Type*} (f : ι → set α)
  (h : directed (⊇) f) : directed (≥) (λ i, 𝓝' (f i)) :=
begin
  intros i j,
  obtain ⟨k, hi, hj⟩ := h i j,
  use k,
  exact ⟨nhds_principal.mono hi, nhds_principal.mono hj⟩,
end

lemma filter.mem_infi_of_directed_of_open {ι : Type*} [nonempty ι] (f : ι → set α)
  (hfd : directed (⊇) f) (s : set α) (hs : is_open s) :
  s ∈ (⨅ i, 𝓝' (f i)) ↔ ∃ i, f i ⊆ s :=
begin
  rw filter.mem_infi_of_directed (filter.directed_nhds_principal f hfd),
  simp [hs],
end

lemma filter.is_open.infi_of_directed {ι : Type*} (f : ι → filter α)
  (hf : ∀ i, (f i).is_open) (hd : directed (≥) f) :
  (⨅ i, f i).is_open :=
begin
  casesI is_empty_or_nonempty ι,
  { simp [infi_of_empty], },
  intros s hs,
  rw [filter.mem_infi_of_directed hd] at hs,
  obtain ⟨i, hs⟩ := hs,
  obtain ⟨v, hv, hvo, hvs⟩ := hf i _ hs,
  refine ⟨v, _, hvo, hvs⟩,
  have : (⨅ (i : ι), f i) ≤ f i := infi_le _ _,
  exact this hv,
end

lemma filter.is_open.infi_nhds_principal_of_directed {ι : Type*} (f : ι → set α)
  (hd : directed (⊇) f) :
  (⨅ i, 𝓝' (f i)).is_open :=
begin
  apply filter.is_open.infi_of_directed,
  simp,
  apply filter.directed_nhds_principal _ hd,
end

lemma filter.infi_le_of_directed {ι ι' : Type*} [nonempty ι] (f : ι → set α) (g : ι' → set α)
  (hg : ∀ j, is_open (g j)) (hfd : directed (⊇) f) :
  (⨅ i, 𝓝' (f i)) ≤ (⨅ j, 𝓝' (g j)) ↔ ∀ j, ∃ i, f i ⊆ g j :=
begin
  simp,
  have : ∀ j, (⨅ (i : ι), 𝓝' (f i)) ≤ 𝓝' (g j) ↔ g j ∈ ⨅ (i : ι), 𝓝' (f i),
  { intro,
    rw ←filter.is_open.le_nhds_principal_of_is_open,
    apply filter.is_open.infi_of_directed, simp,
    { apply filter.directed_nhds_principal _ hfd, },
    apply hg, },
  simp [this],
  have : ∀ j, g j ∈ (⨅ (i : ι), 𝓝' (f i)) ↔ ∃ i, f i ⊆ g j,
  { intro j,
    rw filter.mem_infi_of_directed_of_open f hfd _ (hg _), },
  simp [this],
end

lemma filter.opens_directed (f : filter α) :
  directed (⊇) (λ (u : {u : set α | is_open u ∧ u ∈ f}), (u : set α)) :=
begin
  rintro ⟨u, hu, huf⟩ ⟨v, hv, hvf⟩,
  refine ⟨⟨u ∩ v, hu.inter hv, filter.inter_mem huf hvf⟩, set.inter_subset_left _ _, set.inter_subset_right _ _⟩,
end

-- presheaf reconstruction
lemma filter.is_open.eq_infi {f : filter α} (hf : f.is_open) :
  f = ⨅ (u : {u : set α | is_open u ∧ u ∈ f}), 𝓝' u :=
begin
  apply le_antisymm,
  { simp,
    intros s hs hsf,
    rw hf.le_iff (nhds_principal.is_open _),
    intros V hV hVo,
    simp [hVo] at hV,
    exact ⟨s, hsf, hs, hV⟩, },
  { rw filter.is_open.le_iff _ hf,
    swap,
    { apply filter.is_open.infi_of_directed,
      { rintro ⟨u, hu, huf⟩, simp, },
      { apply filter.directed_nhds_principal,
        apply filter.opens_directed, } },
    intros V hV hVo,
    refine ⟨V, _, hVo, rfl.subset⟩,
    have : (⨅ (u : {u : set α | is_open u ∧ u ∈ f}), 𝓝' u.1) ≤ _ := infi_le _ ⟨V, hVo, hV⟩,
    have Vmem : V ∈ 𝓝' V := by simp [hVo],
    exact this Vmem, },
end


lemma eq_inter_open_of_t1 [t1_space α] (s : set α) :
  s = ⋂ (t ∈ {t : set α | s ⊆ t ∧ is_open t}), t :=
begin
  ext x,
  simp,
  split,
  { intros hx t ht hto,
    exact ht hx, },
  { intro h,
    by_contra h',
    have := λ (y : s), t1_space_iff_exists_open.mp ‹_› (y : α) x (by { rintro rfl, simpa [y.2] using h' }),
    choose f hop hx hy using this,
    specialize h (⋃ s, f s) _ (is_open_Union hop),
    { intros y hy,
      simp,
      exact ⟨y, hy, hx _⟩, },
    simp at h,
    obtain ⟨z, hz, h⟩ := h,
    exact hy _ h, },
end

lemma eq_inter_nhds_principal_of_t1 [t1_space α] (s : set α) :
  s = ⋂ (t ∈ 𝓝' s), t :=
begin
  nth_rewrite 0 eq_inter_open_of_t1 s,
  ext x,
  simp [mem_nhds_principal_iff],
  split,
  { intros h t t' ht ho hs,
    exact ht (h t' hs ho), },
  { intros h t ht ho,
    exact h _ _ rfl.subset ho ht, },
end

lemma nhds_principal_le_iff [t1_space α] {s s' : set α} :
  𝓝' s ≤ 𝓝' s' ↔ s ⊆ s' :=
begin
  refine ⟨_, nhds_principal.mono⟩,
  intros h x hx,
  rw eq_inter_open_of_t1 s',
  simp,
  intros u hu huo,
  specialize @h u,
  simp [mem_nhds_principal_iff] at h,
  specialize h u rfl.subset huo hu,
  obtain ⟨t, ht, hto, ht'⟩ := h,
  exact ht (ht' hx),
end

lemma nhds_le_nhds_principal_iff [t1_space α] {a : α} {s : set α} :
  𝓝 a ≤ 𝓝' s ↔ a ∈ s :=
by simp [nhds_eq_nhds_principal, nhds_principal_le_iff]

lemma nhds_principal_inter_le [t1_space α] {s s' : set α} : 𝓝' (s ∩ s') ≤ 𝓝' s ⊓ 𝓝' s' :=
by simp [nhds_principal_le_iff]

lemma nhds_principal_Inter_le [t1_space α] {ι : Type*} (s : ι → set α) : 𝓝' (⋂ i, s i) ≤ ⨅ i, 𝓝' (s i) :=
by simp [nhds_principal_le_iff, set.Inter_subset s]  

lemma supr_pts_le (f : filter α) :
  (⨆ (a : α) (h : 𝓝 a ≤ f), 𝓝 a) ≤ f :=
by simp

lemma nhds_principal_pts_le (f : filter α) :
  𝓝' {a : α | 𝓝 a ≤ f} ≤ f :=
begin
  rw nhds_principal_eq_supr,
  apply supr_pts_le,
end

lemma filter.is_open.le_nhds_principal_of_mem
  {f : filter α} (h : f.is_open) {s : set α} (hs : s ∈ f) :
  f ≤ 𝓝' s :=
begin
  intros u,
  simp [mem_nhds_principal_iff],
  intros v hv ho hsv,
  exact filter.mem_of_superset hs (hsv.trans hv),
end

lemma filter.eq_of_forall_ge_iff_of_open {f g : filter α} (hf : f.is_open) (hg : g.is_open)
  (h : ∀ (y : filter α), y.is_open → (f ≤ y ↔ g ≤ y)) : f = g :=
begin
  have h1 := h f hf,
  have h2 := h g hg,
  simp at h1 h2,
  apply le_antisymm; assumption,
end

lemma filter.eq_of_forall_le_iff_of_open {f g : filter α} (hf : f.is_open) (hg : g.is_open)
  (h : ∀ (y : filter α), y.is_open → (y ≤ f ↔ y ≤ g)) : f = g :=
begin
  have h1 := h f hf,
  have h2 := h g hg,
  simp at h1 h2,
  apply le_antisymm; assumption,
end

lemma nhds_principal_inter_eq_of_open {s s' : set α} (hs : is_open s) (hs' : is_open s') : 𝓝' (s ∩ s') = 𝓝' s ⊓ 𝓝' s' :=
begin
  apply filter.eq_of_forall_le_iff_of_open,
  exact (nhds_principal.is_open _),
  exact (nhds_principal.is_open _).inf (nhds_principal.is_open _),
  intros c hc,
  have hc' := hc,
  rw filter.is_open.eq_infi hc at ⊢ hc',
  simp,
  rw filter.is_open.le_nhds_principal_of_is_open hc' _ hs,
  rw filter.is_open.le_nhds_principal_of_is_open hc' _ hs',
  rw filter.is_open.le_nhds_principal_of_is_open hc' _ (hs.inter hs'),
  simp,
end

@[simp] protected lemma finset.forall_coe {α : Type*} (s : finset α) (p : s → Prop) :
  (∀ (x : s), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩ := subtype.forall

lemma nhds_principal_Inter_finite {ι : Type*} (s : ι → set α) (t : finset ι) (h : ∀ i, i ∈ t → is_open (s i)) :
  𝓝' (⋂ (i ∈ t), s i) = ⨅ (i ∈ t), 𝓝' (s i) :=
begin
  classical,
  induction t using finset.induction with k t hkt ih,
  { simp, },
  { rw [finset.infi_insert],
    have h1 : is_open (s k) := h k (by simp),
    have h2 : is_open (⋂ (x : ι) (h : x ∈ t), s x),
    { convert_to is_open (⋂ (x : t), s x.1),
      ext, simp,
      apply is_open_Inter,
      intro, apply h, simp, },
    simp [nhds_principal_inter_eq_of_open h1 h2],
    rw [ih],
    intros, apply h, simp [*], },
end

/-
lemma nhds_principal_inter_eq_of_closed {s s' : set α} (hs : is_closed s) (hs' : is_closed s') : 𝓝' (s ∩ s') = 𝓝' s ⊓ 𝓝' s' :=
begin
end
-/

/-
-- not true:
lemma nhds_principal_inter_of_t1 {s s' : set α} : 𝓝' (s ∩ s') = 𝓝' s ⊓ 𝓝' s' :=
begin
  apply filter.is_open.ext, simp, apply filter.is_open.inf; simp,
  intros u hu,
  simp [hu],
  simp [filter.mem_inf_of_open],
  split,
  { intro h,
    use u,
    simp [*],
},
end
-/

--example : 𝓝' ({0} ∩ set.Ioo 0 1 : set ℝ) ≠ 𝓝' {0} ⊓ 𝓝' (set.Ioo 0 1)

lemma filter.is_open.inf_eq_bot_iff {f g : filter α} (hf : f.is_open) (hg : g.is_open) :
  f ⊓ g = ⊥ ↔ ∃ (U ∈ f) (V ∈ g), is_open U ∧ is_open V ∧ U ∩ V = ∅ :=
begin
  rw filter.inf_eq_bot_iff,
  split,
  { rintro ⟨U, hU, V, hV, h⟩,
    obtain ⟨U', hU', hUo', hUs⟩ := hf _ hU,
    obtain ⟨V', hV', hVo', hVs⟩ := hg _ hV,
    refine ⟨U', hU', V', hV', hUo', hVo', _⟩,
    rw ← set.subset_empty_iff,
    refine (set.inter_subset_inter hUs hVs).trans _,
    simp [h], },
  { rintro ⟨U, hU, V, hV, hUo, hVo, h⟩,
    exact ⟨U, hU, V, hV, h⟩ }
end

lemma filter_split (f : filter α) (s : set α) : f = (f ⊓ 𝓝' s) ⊔ (f ⊓ 𝓝' sᶜ) :=
begin
  transitivity f ⊓ (𝓝' s ⊔ 𝓝' sᶜ),
  { rw ← nhds_principal_union,
    simp, },
  exact inf_sup_left,
end

lemma filter_le_nhds_principal_of_eq_bot {f : filter α} (hf : f.is_open) (s : set α) :
  f ⊓ 𝓝' sᶜ = ⊥ → f ≤ 𝓝' s :=
begin
  rw filter.is_open.inf_eq_bot_iff hf (nhds_principal.is_open _),
  rintro ⟨U, hU, V, hV, hUo, hVo, h⟩,
  rw ← set.subset_compl_iff_disjoint at h,
  refine le_trans (hf.le_nhds_principal_of_mem hU) _,
  mono,
  refine h.trans _,
  simp [hVo] at hV,
  rwa set.compl_subset_comm,
end

/-
lemma filter_le_nhds_principal_iff [t1_space α] {f : filter α} (hf : f.is_open) (s : set α) :
  f ≤ 𝓝' s ↔ f ⊓ 𝓝' sᶜ = ⊥ :=
begin
  refine ⟨_, filter_le_nhds_principal_of_eq_bot hf s⟩,
--  have hinf : (f ⊓ 𝓝' sᶜ).is_open := hf.inf (nhds_principal.is_open sᶜ),

  { intro h,
    rw filter.is_open.inf_eq_bot_iff hf (nhds_principal.is_open sᶜ),
    rw hf.le_iff (nhds_principal.is_open s) at h,
    replace h := λ (V : set α) (hV : is_open V) (hs : s ⊆ V), h V ((mem_nhds_principal_iff_of_is_open hV).mpr hs) hV,
    choose g hg hg' hg'' using h,
--    rw nhds_principal_eq_supr,
    ext u,
    simp,
    simp [filter.mem_inf_iff],
    have := eq_inter_nhds_principal_of_t1 u,
    rw mem_nhds_principal_iff_of_is_open hinf,
    rw le_nhds_principal_iff at h,
--    rw mem_nhds_principal_iff_of_is_open hinf,
    simp [mem_nhds_principal_iff],
    by_contra h',
    push_neg at h',
    sorry,
  },
end-/

-- ultrafilters for open filters
structure gen_pt (α : Type*) [topological_space α] :=
(f : filter α)
(is_open : f.is_open)
(ne_bot : f.ne_bot)
(minimal : ∀ (f' : filter α), f'.is_open → f'.ne_bot → f' ≤ f → f ≤ f')

lemma gen_pt.inf_neq_bot_or (p : gen_pt α) (s : set α) : p.f ⊓ 𝓝' s ≠ ⊥ ∨ p.f ⊓ 𝓝' sᶜ ≠ ⊥ :=
begin
  by_contra h,
  push_neg at h,
  have := filter_split p.f s,
  rw [h.1, h.2] at this,
  simp at this,
  exact p.ne_bot.ne this,
end

lemma gen_pt.le_or_le_compl (p : gen_pt α) (s : set α) : p.f ≤ 𝓝' s ∨ p.f ≤ 𝓝' sᶜ :=
begin
  rw or_iff_not_imp_left,
  intro h,
  replace h := mt (filter_le_nhds_principal_of_eq_bot p.is_open s) h,
  have := p.minimal (p.f ⊓ 𝓝' sᶜ) (p.is_open.inf (nhds_principal.is_open _)) ⟨h⟩,
  simpa using this,
end

lemma gen_pt.exists_le [compact_space α] (p : gen_pt α) : ∃ (x : α), p.f ≤ 𝓝 x :=
begin
  by_contra h,
  push_neg at h,
  simp only [p.is_open.le_iff (nhds.is_open _), exists_prop, not_forall, not_exists, not_and] at h,
/-  have : ∀ (x : α), ∃ (u : set α), is_open u ∧ u ∈ 𝓝 x ∧ p.f ⊓ 𝓝' u = ⊥,
  { intro x,
    obtain ⟨v, hv, hvo, h⟩ := h x,
    refine ⟨v, hvo, hv, _⟩,
    apply le_antisymm, swap, simp,
    rw (p.is_open.inf (nhds_principal.is_open _)).le_iff filter.bot_is_open,
    simp,
    intros u huo,
    have := λ hx, h u hx huo,
    simp [set.not_subset] at this,
    by_cases huf : u ∈ p.f,
    { specialize this huf,
    },
    ext w, simp,
    
    apply or_iff_not_imp_left.mp (gen_pt.le_or_le_compl p v),
  },-/
  have : ∀ x, ∃ (u : set α), is_open u ∧ u ∈ 𝓝 x ∧ p.f ≤ 𝓝' uᶜ,
  { intro x,
    obtain ⟨v, hv, hvo, h⟩ := h x,
    refine ⟨v, hvo, hv, _⟩,
    apply or_iff_not_imp_left.mp (gen_pt.le_or_le_compl p v),
    simp [p.is_open.le_iff (nhds_principal.is_open _)],
    use v,
    simp [hvo, rfl.subset],
    exact h, },
  choose g h h' h'' using this,
--  have : ∀ x, x ∈ f x := λ x, mem_of_mem_nhds (h x),
  obtain ⟨t, ht⟩ := compact_space.elim_nhds_subcover g h',
  have : p.f ≤ ⨅ (x ∈ t), 𝓝' (g x)ᶜ,
  { simp,
    intros,
    apply h'', },
  have : p.f ≤ 𝓝' (⋂ (i ∈ t), (g i)ᶜ),
  { simp [p.is_open.le_iff (nhds_principal.is_open _)],
    intros V hV hVo,
    simp [hVo] at hV,
    
  },
  have : p.f ≤ 𝓝' (⋃ (i ∈ t), (g i))ᶜ,
  { convert this,
    simp, },
  simp [ht] at this,
  exact p.ne_bot.ne this,
end

lemma exists_gen_pt (f : filter α) (hf : f.is_open) [hfn : f.ne_bot] : ∃ p : gen_pt α, p.f ≤ f :=
begin
  let τ                := {f' : filter α | f'.is_open ∧ f'.ne_bot ∧ f' ≤ f},
  let r : τ → τ → Prop := λt₁ t₂, t₂.val ≤ t₁.val,
  haveI                := filter.nonempty_of_ne_bot f,
  let top : τ          := ⟨f, hf, hfn, le_refl f⟩,
  let sup : Π (c:set τ), is_chain r c → τ,
  { intros c hc,
    refine ⟨⨅a:{a:τ | a ∈ insert top c}, a.1, _, _, _⟩,
    { apply filter.is_open.infi_of_is_chain,
      { rintro ⟨⟨f, hf⟩, hi⟩, exact hf.1, },
      have hc' : is_chain r (insert top c) := (hc.insert $ λ ⟨b, _, _, hb⟩ _ _, or.inl hb),
      rintros g ⟨gt,rfl⟩ g' ⟨gt',rfl⟩ hn,
      apply hc' gt'.2 gt.2,
      intro h,
      simpa [h] using hn, },
    exact filter.infi_ne_bot_of_directed
      (is_chain.directed $ hc.insert $ λ ⟨b, _, _, hb⟩ _ _, or.inl hb)
      (assume ⟨⟨a, _, ha, _⟩, _⟩, ha),
    exact infi_le_of_le ⟨top, set.mem_insert _ _⟩ le_rfl, },
  have : ∀ c (hc : is_chain r c) a (ha : a ∈ c), r a (sup c hc),
    from assume c hc a ha, infi_le_of_le ⟨a, set.mem_insert_of_mem _ ha⟩ le_rfl,
  have : (∃ (u : τ), ∀ (a : τ), r u a → r a u),
    from exists_maximal_of_chains_bounded (assume c hc, ⟨sup c hc, this c hc⟩)
      (assume f₁ f₂ f₃ h₁ h₂, le_trans h₂ h₁),
  cases this with uτ hmin,
  exact ⟨⟨uτ.1, uτ.2.1, uτ.2.2.1,
    λ g hg₁ hg₂ hg₃, hmin ⟨g, hg₁, hg₂, hg₃.trans uτ.2.2.2⟩ hg₃⟩,
    uτ.2.2.2⟩,
end

lemma filter_eq_nhds_principal_pts
  [t2_space α] [compact_space α]
  (f : filter α) (hf : f.is_open) :
  f = 𝓝' {a : α | 𝓝 a ≤ f} :=
begin
  refine le_antisymm _ (nhds_principal_pts_le _),
  by_cases hi : f ⊓ (𝓝' {a : α | 𝓝 a ≤ f}ᶜ) = ⊥,
  { exact filter_le_nhds_principal_of_eq_bot hf _ hi },
  { exfalso,
    haveI : (f ⊓ (𝓝' {a : α | 𝓝 a ≤ f}ᶜ)).ne_bot := ⟨hi⟩,
    obtain ⟨P, hP⟩ := exists_gen_pt (f ⊓ (𝓝' {a : α | 𝓝 a ≤ f}ᶜ)) (hf.inf (nhds_principal.is_open _)),
    have : ∃ x, P.f = 𝓝 x := sorry, -- use compact Hausdorff here
    obtain ⟨x, hx⟩ := this,
    rw hx at hP,
    simpa [nhds_le_nhds_principal_iff] using hP, },
end

lemma filter_eq_nhds_principal_pts'
  [t2_space α] [compact_space α]
  (f : filter α) (hf : f.is_open) :
  f = ⨆ a : {a : α // 𝓝 a ≤ f}, 𝓝 a :=
begin
  rw filter_eq_nhds_principal_pts f hf,
  simp_rw [nhds_eq_nhds_principal],
  rw ← nhds_principal_Union,
  simp [nhds_le_nhds_principal_iff, ←nhds_eq_nhds_principal],
end