import control.traversable.instances

import data.set.finite

import order.copy

import tactic.monotonicity

open function set order

universes u v w x y

open_locale classical

structure filter (α : Type*) :=

(sets : set (set α))

(univ_sets : set.univ ∈ sets)

(sets_of_superset {x y} : x ∈ sets → x ⊆ y → y ∈ sets)

(inter_sets {x y} : x ∈ sets → y ∈ sets → x ∩ y ∈ sets)

instance {α : Type*}: has_mem (set α) (filter α) := ⟨λ U F, U ∈ F.sets⟩

namespace filter

variables {α : Type u} {f g : filter α} {s t : set α}

@[simp] protected lemma mem_mk {t : set (set α)} {h₁ h₂ h₃} : s ∈ mk t h₁ h₂ h₃ ↔ s ∈ t := iff.rfl

@[simp] protected lemma mem_sets : s ∈ f.sets ↔ s ∈ f := iff.rfl

instance inhabited_mem : inhabited {s : set α // s ∈ f} := ⟨⟨univ, f.univ_sets⟩⟩

lemma filter_eq : ∀ {f g : filter α}, f.sets = g.sets → f = g

| ⟨a, _, _, _⟩ ⟨._, _, _, _⟩ rfl := rfl

lemma filter_eq_iff : f = g ↔ f.sets = g.sets :=

⟨congr_arg _, filter_eq⟩

protected lemma ext_iff : f = g ↔ ∀ s, s ∈ f ↔ s ∈ g :=

by simp only [filter_eq_iff, ext_iff, filter.mem_sets]

protected lemma ext : (∀ s, s ∈ f ↔ s ∈ g) → f = g :=

filter.ext_iff.2

protected lemma coext (h : ∀ s, sᶜ ∈ f ↔ sᶜ ∈ g) : f = g :=

filter.ext $ compl_surjective.forall.2 h

@[simp] lemma univ_mem : univ ∈ f :=

f.univ_sets

lemma mem_of_superset {x y : set α} (hx : x ∈ f) (hxy : x ⊆ y) : y ∈ f :=

f.sets_of_superset hx hxy

lemma inter_mem {s t : set α} (hs : s ∈ f) (ht : t ∈ f) : s ∩ t ∈ f :=

f.inter_sets hs ht

@[simp] lemma inter_mem_iff {s t : set α} : s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f :=

⟨λ h, ⟨mem_of_superset h (inter_subset_left s t),

mem_of_superset h (inter_subset_right s t)⟩, and_imp.2 inter_mem⟩

lemma diff_mem {s t : set α} (hs : s ∈ f) (ht : tᶜ ∈ f) : s \ t ∈ f :=

inter_mem hs ht

lemma univ_mem' (h : ∀ a, a ∈ s) : s ∈ f :=

mem_of_superset univ_mem (λ x _, h x)

lemma mp_mem (hs : s ∈ f) (h : {x | x ∈ s → x ∈ t} ∈ f) : t ∈ f :=

mem_of_superset (inter_mem hs h) $ λ x ⟨h₁, h₂⟩, h₂ h₁

lemma congr_sets (h : {x | x ∈ s ↔ x ∈ t} ∈ f) : s ∈ f ↔ t ∈ f :=

⟨λ hs, mp_mem hs (mem_of_superset h (λ x, iff.mp)),

λ hs, mp_mem hs (mem_of_superset h (λ x, iff.mpr))⟩

@[simp] lemma bInter_mem {β : Type v} {s : β → set α} {is : set β} (hf : is.finite) :

(⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f :=

finite.induction_on hf (by simp) (λ i s hi _ hs, by simp [hs])

@[simp] lemma bInter_finset_mem {β : Type v} {s : β → set α} (is : finset β) :

(⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f :=

bInter_mem is.finite_to_set

alias bInter_finset_mem ← _root_.finset.Inter_mem_sets

attribute [protected] finset.Inter_mem_sets

@[simp] lemma sInter_mem {s : set (set α)} (hfin : s.finite) :

⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f :=

by rw [sInter_eq_bInter, bInter_mem hfin]

@[simp] lemma Inter_mem {β : Type v} {s : β → set α} [finite β] :

(⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f :=

by simpa using bInter_mem finite_univ

lemma exists_mem_subset_iff : (∃ t ∈ f, t ⊆ s) ↔ s ∈ f :=

⟨λ ⟨t, ht, ts⟩, mem_of_superset ht ts, λ hs, ⟨s, hs, subset.rfl⟩⟩

lemma monotone_mem {f : filter α} : monotone (λ s, s ∈ f) :=

λ s t hst h, mem_of_superset h hst

lemma exists_mem_and_iff {P : set α → Prop} {Q : set α → Prop} (hP : antitone P) (hQ : antitone Q) :

(∃ u ∈ f, P u) ∧ (∃ u ∈ f, Q u) ↔ (∃ u ∈ f, P u ∧ Q u) :=

split,

{ rintro ⟨⟨u, huf, hPu⟩, v, hvf, hQv⟩, exact ⟨u ∩ v, inter_mem huf hvf,

hP (inter_subset_left _ _) hPu, hQ (inter_subset_right _ _) hQv⟩ },

{ rintro ⟨u, huf, hPu, hQu⟩, exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩ }

lemma forall_in_swap {β : Type*} {p : set α → β → Prop} :

(∀ (a ∈ f) b, p a b) ↔ ∀ b (a ∈ f), p a b :=

set.forall_in_swap

end filter

namespace tactic.interactive

open tactic

setup_tactic_parser

meta def filter_upwards

(s : parse types.pexpr_list?)

(wth : parse with_ident_list?)

(tgt : parse (tk "using" *> texpr)?) : tactic unit :=

(s.get_or_else []).reverse.mmap (λ e, eapplyc `filter.mp_mem >> eapply e),

eapplyc `filter.univ_mem',

`[dsimp only [set.mem_set_of_eq]],

let wth := wth.get_or_else [],

if ¬wth.empty then intros wth else skip,

match tgt with

| some e := exact e

| none := skip

end

add_tactic_doc

{ name := "filter_upwards",

category := doc_category.tactic,

decl_names := [`tactic.interactive.filter_upwards],

tags := ["goal management", "lemma application"] }

end tactic.interactive

namespace filter

variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type*} {ι : Sort x}

section principal

def principal (s : set α) : filter α :=

{ sets := {t | s ⊆ t},

univ_sets := subset_univ s,

sets_of_superset := λ x y hx, subset.trans hx,

inter_sets := λ x y, subset_inter }

localized "notation (name := filter.principal) `𝓟` := filter.principal" in filter

@[simp] lemma mem_principal {s t : set α} : s ∈ 𝓟 t ↔ t ⊆ s := iff.rfl

lemma mem_principal_self (s : set α) : s ∈ 𝓟 s := subset.rfl

end principal

open_locale filter

section join

def join (f : filter (filter α)) : filter α :=

{ sets := {s | {t : filter α | s ∈ t} ∈ f},

univ_sets := by simp only [mem_set_of_eq, univ_sets, ← filter.mem_sets, set_of_true],

sets_of_superset := λ x y hx xy,

mem_of_superset hx $ λ f h, mem_of_superset h xy,

inter_sets := λ x y hx hy,

mem_of_superset (inter_mem hx hy) $ λ f ⟨h₁, h₂⟩, inter_mem h₁ h₂ }

@[simp] lemma mem_join {s : set α} {f : filter (filter α)} :

s ∈ join f ↔ {t | s ∈ t} ∈ f := iff.rfl

end join

section lattice

variables {f g : filter α} {s t : set α}

instance : partial_order (filter α) :=

{ le := λ f g, ∀ ⦃U : set α⦄, U ∈ g → U ∈ f,

le_antisymm := λ a b h₁ h₂, filter_eq $ subset.antisymm h₂ h₁,

le_refl := λ a, subset.rfl,

le_trans := λ a b c h₁ h₂, subset.trans h₂ h₁ }

theorem le_def : f ≤ g ↔ ∀ x ∈ g, x ∈ f := iff.rfl

protected lemma not_le : ¬ f ≤ g ↔ ∃ s ∈ g, s ∉ f := by simp_rw [le_def, not_forall]

inductive generate_sets (g : set (set α)) : set α → Prop

| basic {s : set α} : s ∈ g → generate_sets s

| univ : generate_sets univ

| superset {s t : set α} : generate_sets s → s ⊆ t → generate_sets t

| inter {s t : set α} : generate_sets s → generate_sets t → generate_sets (s ∩ t)

def generate (g : set (set α)) : filter α :=

{ sets := generate_sets g,

univ_sets := generate_sets.univ,

sets_of_superset := λ x y, generate_sets.superset,

inter_sets := λ s t, generate_sets.inter }

lemma sets_iff_generate {s : set (set α)} {f : filter α} : f ≤ filter.generate s ↔ s ⊆ f.sets :=

iff.intro

(λ h u hu, h $ generate_sets.basic $ hu)

(λ h u hu, hu.rec_on h univ_mem

(λ x y _ hxy hx, mem_of_superset hx hxy)

(λ x y _ _ hx hy, inter_mem hx hy))

lemma mem_generate_iff {s : set $ set α} {U : set α} :

U ∈ generate s ↔ ∃ t ⊆ s, set.finite t ∧ ⋂₀ t ⊆ U :=

split ; intro h,

{ induction h,

case basic : V V_in

{ exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩ },

case univ { exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩ },

case superset : V W hV' hVW hV

{ rcases hV with ⟨t, hts, ht, htV⟩,

exact ⟨t, hts, ht, htV.trans hVW⟩ },

case inter : V W hV' hW' hV hW

{ rcases ⟨hV, hW⟩ with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩,

exact ⟨t ∪ u, union_subset hts hus, ht.union hu,

(sInter_union _ _).subset.trans $ inter_subset_inter htV huW⟩ } },

{ rcases h with ⟨t, hts, tfin, h⟩,

exact mem_of_superset ((sInter_mem tfin).2 $ λ V hV, generate_sets.basic $ hts hV) h },

protected def mk_of_closure (s : set (set α)) (hs : (generate s).sets = s) : filter α :=

{ sets := s,

univ_sets := hs ▸ (univ_mem : univ ∈ generate s),

sets_of_superset := λ x y, hs ▸ (mem_of_superset : x ∈ generate s → x ⊆ y → y ∈ generate s),

inter_sets := λ x y, hs ▸ (inter_mem : x ∈ generate s → y ∈ generate s →

x ∩ y ∈ generate s) }

lemma mk_of_closure_sets {s : set (set α)} {hs : (generate s).sets = s} :

filter.mk_of_closure s hs = generate s :=

filter.ext $ λ u,

show u ∈ (filter.mk_of_closure s hs).sets ↔ u ∈ (generate s).sets, from hs.symm ▸ iff.rfl

def gi_generate (α : Type*) :

@galois_insertion (set (set α)) (filter α)ᵒᵈ _ _ filter.generate filter.sets :=

{ gc := λ s f, sets_iff_generate,

le_l_u := λ f u h, generate_sets.basic h,

choice := λ s hs, filter.mk_of_closure s (le_antisymm hs $ sets_iff_generate.1 $ le_rfl),

choice_eq := λ s hs, mk_of_closure_sets }

instance : has_inf (filter α) := ⟨λf g : filter α,

{ sets := {s | ∃ (a ∈ f) (b ∈ g), s = a ∩ b },

univ_sets := ⟨_, univ_mem, _, univ_mem, by simp⟩,

sets_of_superset := begin

rintro x y ⟨a, ha, b, hb, rfl⟩ xy,

refine ⟨a ∪ y, mem_of_superset ha (subset_union_left a y),

b ∪ y, mem_of_superset hb (subset_union_left b y), _⟩,

rw [← inter_union_distrib_right, union_eq_self_of_subset_left xy]

end,

inter_sets := begin

rintro x y ⟨a, ha, b, hb, rfl⟩ ⟨c, hc, d, hd, rfl⟩,

refine ⟨a ∩ c, inter_mem ha hc, b ∩ d, inter_mem hb hd, _⟩,

ac_refl

end }⟩

lemma mem_inf_iff {f g : filter α} {s : set α} :

s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, s = t₁ ∩ t₂ := iff.rfl

lemma mem_inf_of_left {f g : filter α} {s : set α} (h : s ∈ f) : s ∈ f ⊓ g :=

⟨s, h, univ, univ_mem, (inter_univ s).symm⟩

lemma mem_inf_of_right {f g : filter α} {s : set α} (h : s ∈ g) : s ∈ f ⊓ g :=

⟨univ, univ_mem, s, h, (univ_inter s).symm⟩

lemma inter_mem_inf {α : Type u} {f g : filter α} {s t : set α}

(hs : s ∈ f) (ht : t ∈ g) : s ∩ t ∈ f ⊓ g :=

⟨s, hs, t, ht, rfl⟩

lemma mem_inf_of_inter {f g : filter α} {s t u : set α} (hs : s ∈ f) (ht : t ∈ g) (h : s ∩ t ⊆ u) :

u ∈ f ⊓ g :=

mem_of_superset (inter_mem_inf hs ht) h

lemma mem_inf_iff_superset {f g : filter α} {s : set α} :

s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ∩ t₂ ⊆ s :=

⟨λ ⟨t₁, h₁, t₂, h₂, eq⟩, ⟨t₁, h₁, t₂, h₂, eq ▸ subset.rfl⟩,

λ ⟨t₁, h₁, t₂, h₂, sub⟩, mem_inf_of_inter h₁ h₂ sub⟩

instance : has_top (filter α) :=

⟨{ sets := {s | ∀ x, x ∈ s},

univ_sets := λ x, mem_univ x,

sets_of_superset := λ x y hx hxy a, hxy (hx a),

inter_sets := λ x y hx hy a, mem_inter (hx _) (hy _) }⟩

lemma mem_top_iff_forall {s : set α} : s ∈ (⊤ : filter α) ↔ (∀ x, x ∈ s) :=

iff.rfl

@[simp] lemma mem_top {s : set α} : s ∈ (⊤ : filter α) ↔ s = univ :=

by rw [mem_top_iff_forall, eq_univ_iff_forall]

section complete_lattice

private def original_complete_lattice : complete_lattice (filter α) :=

@order_dual.complete_lattice _ (gi_generate α).lift_complete_lattice

local attribute [instance] original_complete_lattice

instance : complete_lattice (filter α) := original_complete_lattice.copy

/- le -/ filter.partial_order.le rfl

/- top -/ (filter.has_top).1

(top_unique $ λ s hs, by simp [mem_top.1 hs])

/- bot -/ _ rfl

/- sup -/ _ rfl

/- inf -/ (filter.has_inf).1

begin

ext f g : 2,

exact le_antisymm

(le_inf (λ s, mem_inf_of_left) (λ s, mem_inf_of_right))

(begin

rintro s ⟨a, ha, b, hb, rfl⟩,

exact inter_sets _ (@inf_le_left (filter α) _ _ _ _ ha)

(@inf_le_right (filter α) _ _ _ _ hb)

end)

end

/- Sup -/ (join ∘ 𝓟) (by { ext s x, exact mem_Inter₂.symm.trans

(set.ext_iff.1 (sInter_image _ _) x).symm})

/- Inf -/ _ rfl

instance : inhabited (filter α) := ⟨⊥⟩

end complete_lattice

class ne_bot (f : filter α) : Prop := (ne' : f ≠ ⊥)

lemma ne_bot_iff {f : filter α} : ne_bot f ↔ f ≠ ⊥ := ⟨λ h, h.1, λ h, ⟨h⟩⟩

lemma ne_bot.ne {f : filter α} (hf : ne_bot f) : f ≠ ⊥ := ne_bot.ne'

@[simp] lemma not_ne_bot {α : Type*} {f : filter α} : ¬ f.ne_bot ↔ f = ⊥ :=

not_iff_comm.1 ne_bot_iff.symm

lemma ne_bot.mono {f g : filter α} (hf : ne_bot f) (hg : f ≤ g) : ne_bot g :=

⟨ne_bot_of_le_ne_bot hf.1 hg⟩

lemma ne_bot_of_le {f g : filter α} [hf : ne_bot f] (hg : f ≤ g) : ne_bot g :=

hf.mono hg

@[simp] lemma sup_ne_bot {f g : filter α} : ne_bot (f ⊔ g) ↔ ne_bot f ∨ ne_bot g :=

by simp [ne_bot_iff, not_and_distrib]

lemma not_disjoint_self_iff : ¬ disjoint f f ↔ f.ne_bot := by rw [disjoint_self, ne_bot_iff]

lemma bot_sets_eq : (⊥ : filter α).sets = univ := rfl

lemma sup_sets_eq {f g : filter α} : (f ⊔ g).sets = f.sets ∩ g.sets :=

(gi_generate α).gc.u_inf

lemma Sup_sets_eq {s : set (filter α)} : (Sup s).sets = (⋂ f ∈ s, (f : filter α).sets) :=

(gi_generate α).gc.u_Inf

lemma supr_sets_eq {f : ι → filter α} : (supr f).sets = (⋂ i, (f i).sets) :=

(gi_generate α).gc.u_infi

lemma generate_empty : filter.generate ∅ = (⊤ : filter α) :=

(gi_generate α).gc.l_bot

lemma generate_univ : filter.generate univ = (⊥ : filter α) :=

mk_of_closure_sets.symm

lemma generate_union {s t : set (set α)} :

filter.generate (s ∪ t) = filter.generate s ⊓ filter.generate t :=

(gi_generate α).gc.l_sup

lemma generate_Union {s : ι → set (set α)} :

filter.generate (⋃ i, s i) = (⨅ i, filter.generate (s i)) :=

(gi_generate α).gc.l_supr

@[simp] lemma mem_bot {s : set α} : s ∈ (⊥ : filter α) :=

trivial

@[simp] lemma mem_sup {f g : filter α} {s : set α} :

s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g :=

iff.rfl

lemma union_mem_sup {f g : filter α} {s t : set α} (hs : s ∈ f) (ht : t ∈ g) :

s ∪ t ∈ f ⊔ g :=

⟨mem_of_superset hs (subset_union_left s t), mem_of_superset ht (subset_union_right s t)⟩

@[simp] lemma mem_Sup {x : set α} {s : set (filter α)} :

x ∈ Sup s ↔ (∀ f ∈ s, x ∈ (f : filter α)) :=

iff.rfl

@[simp] lemma mem_supr {x : set α} {f : ι → filter α} :

x ∈ supr f ↔ (∀ i, x ∈ f i) :=

by simp only [← filter.mem_sets, supr_sets_eq, iff_self, mem_Inter]

@[simp] lemma supr_ne_bot {f : ι → filter α} : (⨆ i, f i).ne_bot ↔ ∃ i, (f i).ne_bot :=

by simp [ne_bot_iff]

lemma infi_eq_generate (s : ι → filter α) : infi s = generate (⋃ i, (s i).sets) :=

show generate _ = generate _, from congr_arg _ $ congr_arg Sup $ (range_comp _ _).symm

lemma mem_infi_of_mem {f : ι → filter α} (i : ι) : ∀ {s}, s ∈ f i → s ∈ ⨅ i, f i :=

show (⨅ i, f i) ≤ f i, from infi_le _ _

lemma mem_infi_of_Inter {ι} {s : ι → filter α} {U : set α} {I : set ι} (I_fin : I.finite)

{V : I → set α} (hV : ∀ i, V i ∈ s i) (hU : (⋂ i, V i) ⊆ U) : U ∈ ⨅ i, s i :=

haveI := I_fin.fintype,

refine mem_of_superset (Inter_mem.2 $ λ i, _) hU,

exact mem_infi_of_mem i (hV _)

lemma mem_infi {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔

∃ I : set ι, I.finite ∧ ∃ V : I → set α, (∀ i, V i ∈ s i) ∧ U = ⋂ i, V i :=

split,

{ rw [infi_eq_generate, mem_generate_iff],

rintro ⟨t, tsub, tfin, tinter⟩,

rcases eq_finite_Union_of_finite_subset_Union tfin tsub with ⟨I, Ifin, σ, σfin, σsub, rfl⟩,

rw sInter_Union at tinter,

set V := λ i, U ∪ ⋂₀ σ i with hV,

have V_in : ∀ i, V i ∈ s i,

{ rintro i,

have : (⋂₀ σ i) ∈ s i,

{ rw sInter_mem (σfin _),

apply σsub },

exact mem_of_superset this (subset_union_right _ _) },

refine ⟨I, Ifin, V, V_in, _⟩,

rwa [hV, ← union_Inter, union_eq_self_of_subset_right] },

{ rintro ⟨I, Ifin, V, V_in, rfl⟩,

exact mem_infi_of_Inter Ifin V_in subset.rfl }

lemma mem_infi' {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔

∃ I : set ι, I.finite ∧ ∃ V : ι → set α, (∀ i, V i ∈ s i) ∧

(∀ i ∉ I, V i = univ) ∧ (U = ⋂ i ∈ I, V i) ∧ U = ⋂ i, V i :=

simp only [mem_infi, set_coe.forall', bInter_eq_Inter],

refine ⟨_, λ ⟨I, If, V, hVs, _, hVU, _⟩, ⟨I, If, λ i, V i, λ i, hVs i, hVU⟩⟩,

rintro ⟨I, If, V, hV, rfl⟩,

refine ⟨I, If, λ i, if hi : i ∈ I then V ⟨i, hi⟩ else univ, λ i, _, λ i hi, _, _⟩,

{ split_ifs, exacts [hV _, univ_mem] },

{ exact dif_neg hi },

{ simp only [Inter_dite, bInter_eq_Inter, dif_pos (subtype.coe_prop _), subtype.coe_eta,

Inter_univ, inter_univ, eq_self_iff_true, true_and] }

lemma exists_Inter_of_mem_infi {ι : Type*} {α : Type*} {f : ι → filter α} {s}

(hs : s ∈ ⨅ i, f i) : ∃ t : ι → set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i :=

let ⟨I, If, V, hVs, hV', hVU, hVU'⟩ := mem_infi'.1 hs in ⟨V, hVs, hVU'⟩

lemma mem_infi_of_finite {ι : Type*} [finite ι] {α : Type*} {f : ι → filter α} (s) :

s ∈ (⨅ i, f i) ↔ ∃ t : ι → set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i :=

refine ⟨exists_Inter_of_mem_infi, _⟩,

rintro ⟨t, ht, rfl⟩,

exact Inter_mem.2 (λ i, mem_infi_of_mem i (ht i))

@[simp] lemma le_principal_iff {s : set α} {f : filter α} : f ≤ 𝓟 s ↔ s ∈ f :=

show (∀ {t}, s ⊆ t → t ∈ f) ↔ s ∈ f,

from ⟨λ h, h (subset.refl s), λ hs t ht, mem_of_superset hs ht⟩

lemma Iic_principal (s : set α) : Iic (𝓟 s) = {l | s ∈ l} :=

set.ext $ λ x, le_principal_iff

lemma principal_mono {s t : set α} : 𝓟 s ≤ 𝓟 t ↔ s ⊆ t :=

by simp only [le_principal_iff, iff_self, mem_principal]

@[mono] lemma monotone_principal : monotone (𝓟 : set α → filter α) :=

λ _ _, principal_mono.2

@[simp] lemma principal_eq_iff_eq {s t : set α} : 𝓟 s = 𝓟 t ↔ s = t :=

by simp only [le_antisymm_iff, le_principal_iff, mem_principal]; refl

@[simp] lemma join_principal_eq_Sup {s : set (filter α)} : join (𝓟 s) = Sup s := rfl

@[simp] lemma principal_univ : 𝓟 (univ : set α) = ⊤ :=

top_unique $ by simp only [le_principal_iff, mem_top, eq_self_iff_true]

@[simp] lemma principal_empty : 𝓟 (∅ : set α) = ⊥ :=

bot_unique $ λ s _, empty_subset _

lemma generate_eq_binfi (S : set (set α)) : generate S = ⨅ s ∈ S, 𝓟 s :=

eq_of_forall_le_iff $ λ f, by simp [sets_iff_generate, le_principal_iff, subset_def]

lemma empty_mem_iff_bot {f : filter α} : ∅ ∈ f ↔ f = ⊥ :=

⟨λ h, bot_unique $ λ s _, mem_of_superset h (empty_subset s),

λ h, h.symm ▸ mem_bot⟩

lemma nonempty_of_mem {f : filter α} [hf : ne_bot f] {s : set α} (hs : s ∈ f) :

s.nonempty :=

s.eq_empty_or_nonempty.elim (λ h, absurd hs (h.symm ▸ mt empty_mem_iff_bot.mp hf.1)) id

lemma ne_bot.nonempty_of_mem {f : filter α} (hf : ne_bot f) {s : set α} (hs : s ∈ f) :

s.nonempty :=

@nonempty_of_mem α f hf s hs

@[simp] lemma empty_not_mem (f : filter α) [ne_bot f] : ¬(∅ ∈ f) :=

λ h, (nonempty_of_mem h).ne_empty rfl

lemma nonempty_of_ne_bot (f : filter α) [ne_bot f] : nonempty α :=

nonempty_of_exists $ nonempty_of_mem (univ_mem : univ ∈ f)

lemma compl_not_mem {f : filter α} {s : set α} [ne_bot f] (h : s ∈ f) : sᶜ ∉ f :=

λ hsc, (nonempty_of_mem (inter_mem h hsc)).ne_empty $ inter_compl_self s

lemma filter_eq_bot_of_is_empty [is_empty α] (f : filter α) : f = ⊥ :=

empty_mem_iff_bot.mp $ univ_mem' is_empty_elim

protected lemma disjoint_iff {f g : filter α} :

disjoint f g ↔ ∃ (s ∈ f) (t ∈ g), disjoint s t :=

by simp only [disjoint_iff, ← empty_mem_iff_bot, mem_inf_iff,

inf_eq_inter, bot_eq_empty, @eq_comm _ ∅]

lemma disjoint_of_disjoint_of_mem {f g : filter α} {s t : set α} (h : disjoint s t)

(hs : s ∈ f) (ht : t ∈ g) : disjoint f g :=

filter.disjoint_iff.mpr ⟨s, hs, t, ht, h⟩

lemma ne_bot.not_disjoint (hf : f.ne_bot) (hs : s ∈ f) (ht : t ∈ f) :

¬ disjoint s t :=

λ h, not_disjoint_self_iff.2 hf $ filter.disjoint_iff.2 ⟨s, hs, t, ht, h⟩

lemma inf_eq_bot_iff {f g : filter α} :

f ⊓ g = ⊥ ↔ ∃ (U ∈ f) (V ∈ g), U ∩ V = ∅ :=

by simpa only [←disjoint_iff, set.disjoint_iff_inter_eq_empty] using filter.disjoint_iff

lemma _root_.pairwise.exists_mem_filter_of_disjoint {ι : Type*} [finite ι]

{l : ι → filter α} (hd : pairwise (disjoint on l)) :

∃ s : ι → set α, (∀ i, s i ∈ l i) ∧ pairwise (disjoint on s) :=

simp only [pairwise, function.on_fun, filter.disjoint_iff, subtype.exists'] at hd,

choose! s t hst using hd,

refine ⟨λ i, ⋂ j, @s i j ∩ @t j i, λ i, _, λ i j hij, _⟩,

exacts [Inter_mem.2 (λ j, inter_mem (@s i j).2 (@t j i).2),

(hst hij).mono ((Inter_subset _ j).trans (inter_subset_left _ _))

((Inter_subset _ i).trans (inter_subset_right _ _))]

lemma _root_.set.pairwise_disjoint.exists_mem_filter {ι : Type*} {l : ι → filter α} {t : set ι}

(hd : t.pairwise_disjoint l) (ht : t.finite) :

∃ s : ι → set α, (∀ i, s i ∈ l i) ∧ t.pairwise_disjoint s :=

casesI ht,

obtain ⟨s, hd⟩ : ∃ s : Π i : t, {s : set α // s ∈ l i}, pairwise (disjoint on λ i, (s i : set α)),

{ rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩,

exact ⟨λ i, ⟨s i, hsl i⟩, hsd⟩ },

-- TODO: Lean fails to find `can_lift` instance and fails to use an instance supplied by `letI`

rcases @subtype.exists_pi_extension ι (λ i, {s // s ∈ l i}) _ _ s with ⟨s, rfl⟩,

exact ⟨λ i, s i, λ i, (s i).2, pairwise.set_of_subtype _ _ hd⟩

instance unique [is_empty α] : unique (filter α) :=

{ to_inhabited := filter.inhabited, uniq := filter_eq_bot_of_is_empty }

lemma eq_top_of_ne_bot [subsingleton α] (l : filter α) [ne_bot l] : l = ⊤ :=

refine top_unique (λ s hs, _),

obtain rfl : s = univ, from subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs),

exact univ_mem

lemma forall_mem_nonempty_iff_ne_bot {f : filter α} :

(∀ (s : set α), s ∈ f → s.nonempty) ↔ ne_bot f :=

⟨λ h, ⟨λ hf, not_nonempty_empty (h ∅ $ hf.symm ▸ mem_bot)⟩, @nonempty_of_mem _ _⟩

instance [nonempty α] : nontrivial (filter α) :=

⟨⟨⊤, ⊥, ne_bot.ne $ forall_mem_nonempty_iff_ne_bot.1 $ λ s hs,

by rwa [mem_top.1 hs, ← nonempty_iff_univ_nonempty]⟩⟩

lemma nontrivial_iff_nonempty : nontrivial (filter α) ↔ nonempty α :=

⟨λ h, by_contra $ λ h',

by { haveI := not_nonempty_iff.1 h', exact not_subsingleton (filter α) infer_instance },

@filter.nontrivial α⟩

lemma eq_Inf_of_mem_iff_exists_mem {S : set (filter α)} {l : filter α}

(h : ∀ {s}, s ∈ l ↔ ∃ f ∈ S, s ∈ f) : l = Inf S :=

le_antisymm (le_Inf $ λ f hf s hs, h.2 ⟨f, hf, hs⟩)

(λ s hs, let ⟨f, hf, hs⟩ := h.1 hs in (Inf_le hf : Inf S ≤ f) hs)

lemma eq_infi_of_mem_iff_exists_mem {f : ι → filter α} {l : filter α}

(h : ∀ {s}, s ∈ l ↔ ∃ i, s ∈ f i) :

l = infi f :=

eq_Inf_of_mem_iff_exists_mem $ λ s, h.trans exists_range_iff.symm

lemma eq_binfi_of_mem_iff_exists_mem {f : ι → filter α} {p : ι → Prop} {l : filter α}

(h : ∀ {s}, s ∈ l ↔ ∃ i (_ : p i), s ∈ f i) :

l = ⨅ i (_ : p i), f i :=

rw [infi_subtype'],

apply eq_infi_of_mem_iff_exists_mem,

intro s,

exact h.trans ⟨λ ⟨i, pi, si⟩, ⟨⟨i, pi⟩, si⟩, λ ⟨⟨i, pi⟩, si⟩, ⟨i, pi, si⟩⟩

lemma infi_sets_eq {f : ι → filter α} (h : directed (≥) f) [ne : nonempty ι] :

(infi f).sets = (⋃ i, (f i).sets) :=

let ⟨i⟩ := ne, u := { filter .

sets := (⋃ i, (f i).sets),

univ_sets := by simp only [mem_Union]; exact ⟨i, univ_mem⟩,

sets_of_superset := by simp only [mem_Union, exists_imp_distrib];

intros x y i hx hxy; exact ⟨i, mem_of_superset hx hxy⟩,

inter_sets :=

begin

simp only [mem_Union, exists_imp_distrib],

intros x y a hx b hy,

rcases h a b with ⟨c, ha, hb⟩,

exact ⟨c, inter_mem (ha hx) (hb hy)⟩

end } in

have u = infi f, from eq_infi_of_mem_iff_exists_mem

(λ s, by simp only [filter.mem_mk, mem_Union, filter.mem_sets]),

congr_arg filter.sets this.symm

lemma mem_infi_of_directed {f : ι → filter α} (h : directed (≥) f) [nonempty ι] (s) :

s ∈ infi f ↔ ∃ i, s ∈ f i :=

by simp only [← filter.mem_sets, infi_sets_eq h, mem_Union]

lemma mem_binfi_of_directed {f : β → filter α} {s : set β}

(h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) {t : set α} :

t ∈ (⨅ i ∈ s, f i) ↔ ∃ i ∈ s, t ∈ f i :=

by haveI : nonempty {x // x ∈ s} := ne.to_subtype;

erw [infi_subtype', mem_infi_of_directed h.directed_coe, subtype.exists]; refl

lemma binfi_sets_eq {f : β → filter α} {s : set β}

(h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) :

(⨅ i ∈ s, f i).sets = ⋃ i ∈ s, (f i).sets :=

ext $ λ t, by simp [mem_binfi_of_directed h ne]

lemma infi_sets_eq_finite {ι : Type*} (f : ι → filter α) :

(⨅ i, f i).sets = (⋃ t : finset ι, (⨅ i ∈ t, f i).sets) :=

rw [infi_eq_infi_finset, infi_sets_eq],

exact directed_of_sup (λ s₁ s₂, binfi_mono),

lemma infi_sets_eq_finite' (f : ι → filter α) :

(⨅ i, f i).sets = (⋃ t : finset (plift ι), (⨅ i ∈ t, f (plift.down i)).sets) :=

by { rw [← infi_sets_eq_finite, ← equiv.plift.surjective.infi_comp], refl }

lemma mem_infi_finite {ι : Type*} {f : ι → filter α} (s) :

s ∈ infi f ↔ ∃ t : finset ι, s ∈ ⨅ i ∈ t, f i :=

(set.ext_iff.1 (infi_sets_eq_finite f) s).trans mem_Union

lemma mem_infi_finite' {f : ι → filter α} (s) :

s ∈ infi f ↔ ∃ t : finset (plift ι), s ∈ ⨅ i ∈ t, f (plift.down i) :=

(set.ext_iff.1 (infi_sets_eq_finite' f) s).trans mem_Union

@[simp] lemma sup_join {f₁ f₂ : filter (filter α)} : (join f₁ ⊔ join f₂) = join (f₁ ⊔ f₂) :=

filter.ext $ λ x, by simp only [mem_sup, mem_join]

@[simp] lemma supr_join {ι : Sort w} {f : ι → filter (filter α)} :

(⨆ x, join (f x)) = join (⨆ x, f x) :=

filter.ext $ λ x, by simp only [mem_supr, mem_join]

instance : distrib_lattice (filter α) :=

{ le_sup_inf :=

begin

intros x y z s,

simp only [and_assoc, mem_inf_iff, mem_sup, exists_prop, exists_imp_distrib, and_imp],

rintro hs t₁ ht₁ t₂ ht₂ rfl,

exact ⟨t₁, x.sets_of_superset hs (inter_subset_left t₁ t₂),

ht₁,

t₂,

x.sets_of_superset hs (inter_subset_right t₁ t₂),

ht₂,

rfl⟩

end,

..filter.complete_lattice }

instance : coframe (filter α) :=

{ Inf := Inf,

infi_sup_le_sup_Inf := λ f s, begin

rw [Inf_eq_infi', infi_subtype'],

rintro t ⟨h₁, h₂⟩,

rw infi_sets_eq_finite' at h₂,

simp only [mem_Union, (finset.inf_eq_infi _ _).symm] at h₂,

obtain ⟨u, hu⟩ := h₂,

suffices : (⨅ i, f ⊔ ↑i) ≤ f ⊔ u.inf (λ i, ↑i.down),

{ exact this ⟨h₁, hu⟩ },

refine finset.induction_on u (le_sup_of_le_right le_top) _,

rintro ⟨i⟩ u _ ih,

rw [finset.inf_insert, sup_inf_left],

exact le_inf (infi_le _ _) ih,

end,

..filter.complete_lattice }

lemma mem_infi_finset {s : finset α} {f : α → filter β} {t : set β} :

t ∈ (⨅ a ∈ s, f a) ↔ (∃ p : α → set β, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a) :=

simp only [← finset.set_bInter_coe, bInter_eq_Inter, infi_subtype'],

refine ⟨λ h, _, _⟩,

{ rcases (mem_infi_of_finite _).1 h with ⟨p, hp, rfl⟩,

refine ⟨λ a, if h : a ∈ s then p ⟨a, h⟩ else univ, λ a ha, by simpa [ha] using hp ⟨a, ha⟩, _⟩,

refine Inter_congr_of_surjective id surjective_id _,

rintro ⟨a, ha⟩, simp [ha] },

{ rintro ⟨p, hpf, rfl⟩,

exact Inter_mem.2 (λ a, mem_infi_of_mem a (hpf a a.2)) }

lemma infi_ne_bot_of_directed' {f : ι → filter α} [nonempty ι]

(hd : directed (≥) f) (hb : ∀ i, ne_bot (f i)) : ne_bot (infi f) :=

⟨begin

intro h,

have he : ∅ ∈ (infi f), from h.symm ▸ (mem_bot : ∅ ∈ (⊥ : filter α)),

obtain ⟨i, hi⟩ : ∃ i, ∅ ∈ f i,

from (mem_infi_of_directed hd ∅).1 he,

exact (hb i).ne (empty_mem_iff_bot.1 hi)

end⟩

lemma infi_ne_bot_of_directed {f : ι → filter α}

[hn : nonempty α] (hd : directed (≥) f) (hb : ∀ i, ne_bot (f i)) : ne_bot (infi f) :=

casesI is_empty_or_nonempty ι,

{ constructor, simp [infi_of_empty f, top_ne_bot] },

{ exact infi_ne_bot_of_directed' hd hb }

lemma Inf_ne_bot_of_directed' {s : set (filter α)} (hne : s.nonempty) (hd : directed_on (≥) s)

(hbot : ⊥ ∉ s) : ne_bot (Inf s) :=

(Inf_eq_infi' s).symm ▸ @infi_ne_bot_of_directed' _ _ _

hne.to_subtype hd.directed_coe (λ ⟨f, hf⟩, ⟨ne_of_mem_of_not_mem hf hbot⟩)

lemma Inf_ne_bot_of_directed [nonempty α] {s : set (filter α)} (hd : directed_on (≥) s)

(hbot : ⊥ ∉ s) : ne_bot (Inf s) :=

(Inf_eq_infi' s).symm ▸ infi_ne_bot_of_directed hd.directed_coe

(λ ⟨f, hf⟩, ⟨ne_of_mem_of_not_mem hf hbot⟩)

lemma infi_ne_bot_iff_of_directed' {f : ι → filter α} [nonempty ι] (hd : directed (≥) f) :

ne_bot (infi f) ↔ ∀ i, ne_bot (f i) :=

⟨λ H i, H.mono (infi_le _ i), infi_ne_bot_of_directed' hd⟩

lemma infi_ne_bot_iff_of_directed {f : ι → filter α} [nonempty α] (hd : directed (≥) f) :

ne_bot (infi f) ↔ (∀ i, ne_bot (f i)) :=

⟨λ H i, H.mono (infi_le _ i), infi_ne_bot_of_directed hd⟩

lemma infi_sets_induct {f : ι → filter α} {s : set α} (hs : s ∈ infi f) {p : set α → Prop}

(uni : p univ)

(ins : ∀ {i s₁ s₂}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) : p s :=

rw [mem_infi_finite'] at hs,

simp only [← finset.inf_eq_infi] at hs,

rcases hs with ⟨is, his⟩,

revert s,

refine finset.induction_on is _ _,

{ intros s hs, rwa [mem_top.1 hs] },

{ rintro ⟨i⟩ js his ih s hs,

rw [finset.inf_insert, mem_inf_iff] at hs,

rcases hs with ⟨s₁, hs₁, s₂, hs₂, rfl⟩,

exact ins hs₁ (ih hs₂) }

@[simp] lemma inf_principal {s t : set α} : 𝓟 s ⊓ 𝓟 t = 𝓟 (s ∩ t) :=

le_antisymm

(by simp only [le_principal_iff, mem_inf_iff]; exact ⟨s, subset.rfl, t, subset.rfl, rfl⟩)

(by simp [le_inf_iff, inter_subset_left, inter_subset_right])

@[simp] lemma sup_principal {s t : set α} : 𝓟 s ⊔ 𝓟 t = 𝓟 (s ∪ t) :=

filter.ext $ λ u, by simp only [union_subset_iff, mem_sup, mem_principal]

@[simp] lemma supr_principal {ι : Sort w} {s : ι → set α} : (⨆ x, 𝓟 (s x)) = 𝓟 (⋃ i, s i) :=

filter.ext $ λ x, by simp only [mem_supr, mem_principal, Union_subset_iff]

@[simp] lemma principal_eq_bot_iff {s : set α} : 𝓟 s = ⊥ ↔ s = ∅ :=

empty_mem_iff_bot.symm.trans $ mem_principal.trans subset_empty_iff

@[simp] lemma principal_ne_bot_iff {s : set α} : ne_bot (𝓟 s) ↔ s.nonempty :=

ne_bot_iff.trans $ (not_congr principal_eq_bot_iff).trans nonempty_iff_ne_empty.symm

alias principal_ne_bot_iff ↔ _ _root_.set.nonempty.principal_ne_bot

lemma is_compl_principal (s : set α) : is_compl (𝓟 s) (𝓟 sᶜ) :=

is_compl.of_eq (by rw [inf_principal, inter_compl_self, principal_empty]) $

by rw [sup_principal, union_compl_self, principal_univ]

theorem mem_inf_principal' {f : filter α} {s t : set α} :

s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f :=

by simp only [← le_principal_iff, (is_compl_principal s).le_left_iff, disjoint_assoc, inf_principal,

← (is_compl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl]

theorem mem_inf_principal {f : filter α} {s t : set α} :

s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f :=

by { simp only [mem_inf_principal', imp_iff_not_or], refl }

lemma supr_inf_principal (f : ι → filter α) (s : set α) :

(⨆ i, f i ⊓ 𝓟 s) = (⨆ i, f i) ⊓ 𝓟 s :=

by { ext, simp only [mem_supr, mem_inf_principal] }

lemma inf_principal_eq_bot {f : filter α} {s : set α} : f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f :=

by { rw [← empty_mem_iff_bot, mem_inf_principal], refl }

lemma mem_of_eq_bot {f : filter α} {s : set α} (h : f ⊓ 𝓟 sᶜ = ⊥) : s ∈ f :=

by rwa [inf_principal_eq_bot, compl_compl] at h

lemma diff_mem_inf_principal_compl {f : filter α} {s : set α} (hs : s ∈ f) (t : set α) :

s \ t ∈ f ⊓ 𝓟 tᶜ :=

inter_mem_inf hs $ mem_principal_self tᶜ

lemma principal_le_iff {s : set α} {f : filter α} :

𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V :=

change (∀ V, V ∈ f → V ∈ _) ↔ _,

simp_rw mem_principal,

@[simp] lemma infi_principal_finset {ι : Type w} (s : finset ι) (f : ι → set α) :

(⨅ i ∈ s, 𝓟 (f i)) = 𝓟 (⋂ i ∈ s, f i) :=

induction s using finset.induction_on with i s hi hs,

{ simp },

{ rw [finset.infi_insert, finset.set_bInter_insert, hs, inf_principal] },

@[simp] lemma infi_principal {ι : Type w} [finite ι] (f : ι → set α) :

(⨅ i, 𝓟 (f i)) = 𝓟 (⋂ i, f i) :=

by { casesI nonempty_fintype ι, simpa using infi_principal_finset finset.univ f }

lemma infi_principal_finite {ι : Type w} {s : set ι} (hs : s.finite) (f : ι → set α) :

(⨅ i ∈ s, 𝓟 (f i)) = 𝓟 (⋂ i ∈ s, f i) :=

lift s to finset ι using hs,

exact_mod_cast infi_principal_finset s f

end lattice

@[mono] lemma join_mono {f₁ f₂ : filter (filter α)} (h : f₁ ≤ f₂) :

join f₁ ≤ join f₂ :=

λ s hs, h hs

protected def eventually (p : α → Prop) (f : filter α) : Prop := {x | p x} ∈ f

notation `∀ᶠ` binders ` in ` f `, ` r:(scoped p, filter.eventually p f) := r

lemma eventually_iff {f : filter α} {P : α → Prop} : (∀ᶠ x in f, P x) ↔ {x | P x} ∈ f :=

iff.rfl

@[simp] lemma eventually_mem_set {s : set α} {l : filter α} : (∀ᶠ x in l, x ∈ s) ↔ s ∈ l := iff.rfl

protected lemma ext' {f₁ f₂ : filter α}

(h : ∀ p : α → Prop, (∀ᶠ x in f₁, p x) ↔ (∀ᶠ x in f₂, p x)) :

f₁ = f₂ :=

filter.ext h

lemma eventually.filter_mono {f₁ f₂ : filter α} (h : f₁ ≤ f₂) {p : α → Prop}

(hp : ∀ᶠ x in f₂, p x) :

∀ᶠ x in f₁, p x :=

h hp

lemma eventually_of_mem {f : filter α} {P : α → Prop} {U : set α} (hU : U ∈ f) (h : ∀ x ∈ U, P x) :

∀ᶠ x in f, P x :=

mem_of_superset hU h

protected lemma eventually.and {p q : α → Prop} {f : filter α} :

f.eventually p → f.eventually q → ∀ᶠ x in f, p x ∧ q x :=

inter_mem

lemma eventually_true (f : filter α) : ∀ᶠ x in f, true := univ_mem

lemma eventually_of_forall {p : α → Prop} {f : filter α} (hp : ∀ x, p x) :

∀ᶠ x in f, p x :=

univ_mem' hp

lemma forall_eventually_of_eventually_forall {f : filter α} {p : α → β → Prop}

(h : ∀ᶠ x in f, ∀ y, p x y) : ∀ y, ∀ᶠ x in f, p x y :=

by { intros y, filter_upwards [h], tauto, }

@[simp] lemma eventually_false_iff_eq_bot {f : filter α} :

(∀ᶠ x in f, false) ↔ f = ⊥ :=

empty_mem_iff_bot

@[simp] lemma eventually_const {f : filter α} [t : ne_bot f] {p : Prop} :

(∀ᶠ x in f, p) ↔ p :=

classical.by_cases (λ h : p, by simp [h]) (λ h, by simpa [h] using t.ne)