/-
Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury G. Kudryashov

! This file was ported from Lean 3 source module order.filter.countable_Inter
! leanprover-community/mathlib commit b9e46fe101fc897fb2e7edaf0bf1f09ea49eb81a
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Filter.Basic
import Mathlib.Data.Set.Countable

/-!
# Filters with countable intersection property

In this file we define `CountableInterFilter` to be the class of filters with the following
property: for any countable collection of sets `s ∈ l` their intersection belongs to `l` as well.

Two main examples are the `residual` filter defined in `Mathlib.Topology.GDelta` and
the `MeasureTheory.Measure.ae` filter defined in `MeasureTheory.MeasureSpace`.

We reformulate the definition in terms of indexed intersection and in terms of `Filter.Eventually`
and provide instances for some basic constructions (`⊥`, `⊤`, `Filter.principal`, `Filter.map`,
`Filter.comap`, `Inf.inf`). We also provide a custom constructor `Filter.ofCountableInter`
that deduces two axioms of a `Filter` from the countable intersection property.

## Tags
filter, countable
-/


open Set Filter

open Filter

variable {
ι: Sort ?u.136
ι : 
Sort _: Type ?u.7308
Sort
Sort _: Type ?u.7308
 _} {
α: Type ?u.14
α 
β: Type ?u.142
β : 
Type _: Type (?u.3010+1)
Type _}

/-- A filter `l` has the countable intersection property if for any countable collection
of sets `s ∈ l` their intersection belongs to `l` as well. -/
class 
CountableInterFilter: ∀ {α : Type u_1} {l : Filter α},
  (∀ (S : Set (Set α)), Set.Countable S → (∀ (s : Set α), s ∈ S → s ∈ l) → ⋂₀ S ∈ l) → CountableInterFilter l
CountableInterFilter (
l: Filter α
l : 
Filter: Type ?u.20 → Type ?u.20
Filter 
α: Type ?u.14
α) : 
Prop: Type
Prop where
  /-- For a countable collection of sets `s ∈ l`, their intersection belongs to `l` as well. -/
  
countable_sInter_mem: ∀ {α : Type u_1} {l : Filter α} [self : CountableInterFilter l] (S : Set (Set α)),
  Set.Countable S → (∀ (s : Set α), s ∈ S → s ∈ l) → ⋂₀ S ∈ l
countable_sInter_mem : ∀ 
S: Set (Set α)
S : 
Set: Type ?u.25 → Type ?u.25
Set (
Set: Type ?u.26 → Type ?u.26
Set 
α: Type ?u.14
α), 
S: Set (Set α)
S.
Countable: {α : Type ?u.30} → Set α → Prop
Countable → (∀ 
s: ?m.38
s ∈ 
S: Set (Set α)
S, 
s: ?m.38
s ∈ 
l: Filter α
l) → ⋂₀ 
S: Set (Set α)
S ∈ 
l: Filter α
l
#align countable_Inter_filter 
CountableInterFilter: {α : Type u_1} → Filter α → Prop
CountableInterFilter

variable {
l: Filter α
l : 
Filter: Type ?u.6232 → Type ?u.6232
Filter 
α: Type ?u.166
α} [
CountableInterFilter: {α : Type ?u.2281} → Filter α → Prop
CountableInterFilter 
l: Filter α
l]

theorem 
countable_sInter_mem: ∀ {α : Type u_1} {l : Filter α} [inst : CountableInterFilter l] {S : Set (Set α)},
  Set.Countable S → (⋂₀ S ∈ l ↔ ∀ (s : Set α), s ∈ S → s ∈ l)
countable_sInter_mem {
S: Set (Set α)
S : 
Set: Type ?u.181 → Type ?u.181
Set (
Set: Type ?u.182 → Type ?u.182
Set 
α: Type ?u.166
α)} (
hSc: Set.Countable S
hSc : 
S: Set (Set α)
S.
Countable: {α : Type ?u.185} → Set α → Prop
Countable) : ⋂₀ 
S: Set (Set α)
S ∈ 
l: Filter α
l ↔ ∀ 
s: ?m.214
s ∈ 
S: Set (Set α)
S, 
s: ?m.214
s ∈ 
l: Filter α
l :=
  ⟨fun 
hS: ?m.286
hS 
_s: ?m.289
_s 
hs: ?m.292
hs => 
mem_of_superset: ∀ {α : Type ?u.294} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ f
mem_of_superset 
hS: ?m.286
hS (
sInter_subset_of_mem: ∀ {α : Type ?u.308} {S : Set (Set α)} {t : Set α}, t ∈ S → ⋂₀ S ⊆ t
sInter_subset_of_mem 
hs: ?m.292
hs),
    
CountableInterFilter.countable_sInter_mem: ∀ {α : Type ?u.328} {l : Filter α} [self : CountableInterFilter l] (S : Set (Set α)),
  Set.Countable S → (∀ (s : Set α), s ∈ S → s ∈ l) → ⋂₀ S ∈ l
CountableInterFilter.countable_sInter_mem 
_: Set (Set ?m.329)
_ 
hSc: Set.Countable S
hSc⟩
#align countable_sInter_mem 
countable_sInter_mem: ∀ {α : Type u_1} {l : Filter α} [inst : CountableInterFilter l] {S : Set (Set α)},
  Set.Countable S → (⋂₀ S ∈ l ↔ ∀ (s : Set α), s ∈ S → s ∈ l)
countable_sInter_mem

theorem 
countable_iInter_mem: ∀ [inst : Countable ι] {s : ι → Set α}, (iInter fun i => s i) ∈ l ↔ ∀ (i : ι), s i ∈ l
countable_iInter_mem [
Countable: Sort ?u.394 → Prop
Countable 
ι: Sort ?u.376
ι] {
s: ι → Set α
s : 
ι: Sort ?u.376
ι → 
Set: Type ?u.399 → Type ?u.399
Set 
α: Type ?u.379
α} : (⋂ 
i: ?m.414
i, 
s: ι → Set α
s 
i: ?m.414
i) ∈ 
l: Filter α
l ↔ ∀ 
i: ?m.434
i, 
s: ι → Set α
s 
i: ?m.434
i ∈ 
l: Filter α
l :=
  
sInter_range: ∀ {β : Type ?u.464} {ι : Sort ?u.465} (f : ι → Set β), ⋂₀ range f = iInter fun x => f x
sInter_range 
s: ι → Set α
s ▸ (
countable_sInter_mem: ∀ {α : Type ?u.474} {l : Filter α} [inst : CountableInterFilter l] {S : Set (Set α)},
  Set.Countable S → (⋂₀ S ∈ l ↔ ∀ (s : Set α), s ∈ S → s ∈ l)
countable_sInter_mem (
countable_range: ∀ {β : Type ?u.480} {ι : Sort ?u.479} [inst : Countable ι] (f : ι → β), Set.Countable (range f)
countable_range 
_: ?m.482 → ?m.481
_)).
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans 
forall_range_iff: ∀ {α : Type ?u.582} {ι : Sort ?u.583} {f : ι → α} {p : α → Prop}, (∀ (a : α), a ∈ range f → p a) ↔ ∀ (i : ι), p (f i)
forall_range_iff
#align countable_Inter_mem 
countable_iInter_mem: ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ι → Set α},
  (iInter fun i => s i) ∈ l ↔ ∀ (i : ι), s i ∈ l
countable_iInter_mem

theorem 
countable_bInter_mem: ∀ {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s : (i : ι) → i ∈ S → Set α}, (iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
countable_bInter_mem {
ι: Type ?u.660
ι : 
Type _: Type (?u.660+1)
Type _} {
S: Set ι
S : 
Set: Type ?u.663 → Type ?u.663
Set 
ι: Type ?u.660
ι} (
hS: Set.Countable S
hS : 
S: Set ι
S.
Countable: {α : Type ?u.666} → Set α → Prop
Countable) {
s: (i : ι) → i ∈ S → Set α
s : ∀ 
i: ?m.674
i ∈ 
S: Set ι
S, 
Set: Type ?u.711 → Type ?u.711
Set 
α: Type ?u.645
α} :
    (⋂ 
i: ?m.727
i, ⋂ 
hi: i ∈ S
hi : 
i: ?m.727
i ∈ 
S: Set ι
S, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.727
i ‹_›) ∈ 
l: Filter α
l ↔ ∀ 
i: ?m.793
i, ∀ 
hi: i ∈ S
hi : 
i: ?m.793
i ∈ 
S: Set ι
S, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.793
i ‹_› ∈ 
l: Filter α
l := by
Goals accomplished! 🐙
  
ι✝: Sort ?u.642

α: Type u_2

β: Type ?u.648

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s: (i : ι) → i ∈ S → Set α

(iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ lrw [
ι✝: Sort ?u.642

α: Type u_2

β: Type ?u.648

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s: (i : ι) → i ∈ S → Set α

(iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
biInter_eq_iInter: ∀ {α : Type ?u.868} {β : Type ?u.869} (s : Set α) (t : (x : α) → x ∈ s → Set β),
  (iInter fun x => iInter fun h => t x h) = iInter fun x => t ↑x (_ : ↑x ∈ s)
biInter_eq_iInter
ι✝: Sort ?u.642

α: Type u_2

β: Type ?u.648

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s: (i : ι) → i ∈ S → Set α

(iInter fun x => s ↑x (_ : ↑x ∈ S)) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l]
ι✝: Sort ?u.642

α: Type u_2

β: Type ?u.648

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s: (i : ι) → i ∈ S → Set α

(iInter fun x => s ↑x (_ : ↑x ∈ S)) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
  
ι✝: Sort ?u.642

α: Type u_2

β: Type ?u.648

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s: (i : ι) → i ∈ S → Set α

(iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ lhaveI := 
hS: Set.Countable S
hS.
toEncodable: {α : Type ?u.928} → {s : Set α} → Set.Countable s → Encodable ↑s
toEncodable
ι✝: Sort ?u.642

α: Type u_2

β: Type ?u.648

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s: (i : ι) → i ∈ S → Set α

this: Encodable ↑S

(iInter fun x => s ↑x (_ : ↑x ∈ S)) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
  
ι✝: Sort ?u.642

α: Type u_2

β: Type ?u.648

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s: (i : ι) → i ∈ S → Set α

(iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ lexact 
countable_iInter_mem: ∀ {ι : Sort ?u.941} {α : Type ?u.942} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {s : ι → Set α}, (iInter fun i => s i) ∈ l ↔ ∀ (i : ι), s i ∈ l
countable_iInter_mem.
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans 
Subtype.forall: ∀ {α : Sort ?u.1011} {p : α → Prop} {q : { a // p a } → Prop},
  (∀ (x : { a // p a }), q x) ↔ ∀ (a : α) (b : p a), q { val := a, property := b }
Subtype.forall
Goals accomplished! 🐙
#align countable_bInter_mem 
countable_bInter_mem: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s : (i : ι) → i ∈ S → Set α}, (iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
countable_bInter_mem

theorem 
eventually_countable_forall: ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {p : α → ι → Prop},
  Filter.Eventually (fun x => ∀ (i : ι), p x i) l ↔ ∀ (i : ι), Filter.Eventually (fun x => p x i) l
eventually_countable_forall [
Countable: Sort ?u.1152 → Prop
Countable 
ι: Sort ?u.1134
ι] {
p: α → ι → Prop
p : 
α: Type ?u.1137
α → 
ι: Sort ?u.1134
ι → 
Prop: Type
Prop} :
    (∀ᶠ 
x: ?m.1164
x in 
l: Filter α
l, ∀ 
i: ?m.1167
i, 
p: α → ι → Prop
p 
x: ?m.1164
x 
i: ?m.1167
i) ↔ ∀ 
i: ?m.1176
i, ∀ᶠ 
x: ?m.1182
x in 
l: Filter α
l, 
p: α → ι → Prop
p 
x: ?m.1182
x 
i: ?m.1176
i := by
Goals accomplished! 🐙
  
ι: Sort u_1

α: Type u_2

β: Type ?u.1140

l: Filter α

inst✝¹: CountableInterFilter l

inst✝: Countable ι

p: α → ι → Prop

Filter.Eventually (fun x => ∀ (i : ι), p x i) l ↔ ∀ (i : ι), Filter.Eventually (fun x => p x i) lsimpa only [
Filter.Eventually: {α : Type ?u.1203} → (α → Prop) → Filter α → Prop
Filter.Eventually, 
setOf_forall: ∀ {β : Type ?u.1205} {ι : Sort ?u.1206} (p : ι → β → Prop), { x | ∀ (i : ι), p i x } = iInter fun i => { x | p i x }
setOf_forall] using
    @
countable_iInter_mem: ∀ {ι : Sort ?u.1398} {α : Type ?u.1399} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {s : ι → Set α}, (iInter fun i => s i) ∈ l ↔ ∀ (i : ι), s i ∈ l
countable_iInter_mem 
_: Sort ?u.1398
_ 
_: Type ?u.1399
_ 
l: Filter α
l _ _ fun 
i: ?m.1407
i => { 
x: ?m.1414
x | 
p: α → ι → Prop
p 
x: ?m.1414
x 
i: ?m.1407
i }
Goals accomplished! 🐙
#align eventually_countable_forall 
eventually_countable_forall: ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {p : α → ι → Prop},
  Filter.Eventually (fun x => ∀ (i : ι), p x i) l ↔ ∀ (i : ι), Filter.Eventually (fun x => p x i) l
eventually_countable_forall

theorem 
eventually_countable_ball: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {p : α → (i : ι) → i ∈ S → Prop},
      Filter.Eventually (fun x => ∀ (i : ι) (hi : i ∈ S), p x i hi) l ↔         ∀ (i : ι) (hi : i ∈ S), Filter.Eventually (fun x => p x i hi) l
eventually_countable_ball {
ι: Type ?u.1514
ι : 
Type _: Type (?u.1514+1)
Type _} {
S: Set ι
S : 
Set: Type ?u.1517 → Type ?u.1517
Set 
ι: Type ?u.1514
ι} (
hS: Set.Countable S
hS : 
S: Set ι
S.
Countable: {α : Type ?u.1520} → Set α → Prop
Countable)
    {
p: α → (i : ι) → i ∈ S → Prop
p : 
α: Type ?u.1499
α → ∀ 
i: ?m.1530
i ∈ 
S: Set ι
S, 
Prop: Type
Prop} :
    (∀ᶠ 
x: ?m.1572
x in 
l: Filter α
l, ∀ 
i: ?m.1575
i 
hi: ?m.1578
hi, 
p: α → (i : ι) → i ∈ S → Prop
p 
x: ?m.1572
x 
i: ?m.1575
i 
hi: ?m.1578
hi) ↔ ∀ 
i: ?m.1589
i 
hi: ?m.1592
hi, ∀ᶠ 
x: ?m.1598
x in 
l: Filter α
l, 
p: α → (i : ι) → i ∈ S → Prop
p 
x: ?m.1598
x 
i: ?m.1589
i 
hi: ?m.1592
hi := by
Goals accomplished! 🐙
  
ι✝: Sort ?u.1496

α: Type u_2

β: Type ?u.1502

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

p: α → (i : ι) → i ∈ S → Prop

Filter.Eventually (fun x => ∀ (i : ι) (hi : i ∈ S), p x i hi) l ↔   ∀ (i : ι) (hi : i ∈ S), Filter.Eventually (fun x => p x i hi) lsimpa only [
Filter.Eventually: {α : Type ?u.1622} → (α → Prop) → Filter α → Prop
Filter.Eventually, 
setOf_forall: ∀ {β : Type ?u.1624} {ι : Sort ?u.1625} (p : ι → β → Prop), { x | ∀ (i : ι), p i x } = iInter fun i => { x | p i x }
setOf_forall] using
    @
countable_bInter_mem: ∀ {α : Type ?u.2083} {l : Filter α} [inst : CountableInterFilter l] {ι : Type ?u.2082} {S : Set ι},
  Set.Countable S →
    ∀ {s : (i : ι) → i ∈ S → Set α}, (iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
countable_bInter_mem 
_: Type ?u.2083
_ 
l: Filter α
l _ 
_: Type ?u.2082
_ 
_: Set ?m.2088
_ 
hS: Set.Countable S
hS fun 
i: ?m.2098
i 
hi: ?m.2101
hi => { 
x: ?m.2107
x | 
p: α → (i : ι) → i ∈ S → Prop
p 
x: ?m.2107
x 
i: ?m.2098
i 
hi: ?m.2101
hi }
Goals accomplished! 🐙
#align eventually_countable_ball 
eventually_countable_ball: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {p : α → (i : ι) → i ∈ S → Prop},
      Filter.Eventually (fun x => ∀ (i : ι) (hi : i ∈ S), p x i hi) l ↔         ∀ (i : ι) (hi : i ∈ S), Filter.Eventually (fun x => p x i hi) l
eventually_countable_ball

theorem 
EventuallyLE.countable_iUnion: ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → (iUnion fun i => s i) ≤ᶠ[l] iUnion fun i => t i
EventuallyLE.countable_iUnion [
Countable: Sort ?u.2287 → Prop
Countable 
ι: Sort ?u.2269
ι] {
s: ι → Set α
s 
t: ι → Set α
t : 
ι: Sort ?u.2269
ι → 
Set: Type ?u.2298 → Type ?u.2298
Set 
α: Type ?u.2272
α} (
h: ∀ (i : ι), s i ≤ᶠ[l] t i
h : ∀ 
i: ?m.2303
i, 
s: ι → Set α
s 
i: ?m.2303
i ≤ᶠ[
l: Filter α
l] 
t: ι → Set α
t 
i: ?m.2303
i) :
    (⋃ 
i: ?m.2375
i, 
s: ι → Set α
s 
i: ?m.2375
i) ≤ᶠ[
l: Filter α
l] ⋃ 
i: ?m.2390
i, 
t: ι → Set α
t 
i: ?m.2390
i :=
  (
eventually_countable_forall: ∀ {ι : Sort ?u.2409} {α : Type ?u.2410} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {p : α → ι → Prop}, Filter.Eventually (fun x => ∀ (i : ι), p x i) l ↔ ∀ (i : ι), Filter.Eventually (fun x => p x i) l
eventually_countable_forall.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
h: ∀ (i : ι), s i ≤ᶠ[l] t i
h).
mono: ∀ {α : Type ?u.2470} {p q : α → Prop} {f : Filter α},
  Filter.Eventually (fun x => p x) f → (∀ (x : α), p x → q x) → Filter.Eventually (fun x => q x) f
mono fun 
_: ?m.2493
_ 
hst: ?m.2496
hst 
hs: ?m.2501
hs => 
mem_iUnion: ∀ {α : Type ?u.2503} {ι : Sort ?u.2504} {x : α} {s : ι → Set α}, (x ∈ iUnion fun i => s i) ↔ ∃ i, x ∈ s i
mem_iUnion.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| (
mem_iUnion: ∀ {α : Type ?u.2530} {ι : Sort ?u.2531} {x : α} {s : ι → Set α}, (x ∈ iUnion fun i => s i) ↔ ∃ i, x ∈ s i
mem_iUnion.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
hs: ?m.2501
hs).
imp: ∀ {α : Sort ?u.2550} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q a
imp 
hst: ?m.2496
hst
#align eventually_le.countable_Union 
EventuallyLE.countable_iUnion: ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → (iUnion fun i => s i) ≤ᶠ[l] iUnion fun i => t i
EventuallyLE.countable_iUnion

theorem 
EventuallyEq.countable_iUnion: ∀ [inst : Countable ι] {s t : ι → Set α}, (∀ (i : ι), s i =ᶠ[l] t i) → (iUnion fun i => s i) =ᶠ[l] iUnion fun i => t i
EventuallyEq.countable_iUnion [
Countable: Sort ?u.2672 → Prop
Countable 
ι: Sort ?u.2654
ι] {
s: ι → Set α
s 
t: ι → Set α
t : 
ι: Sort ?u.2654
ι → 
Set: Type ?u.2683 → Type ?u.2683
Set 
α: Type ?u.2657
α} (
h: ∀ (i : ι), s i =ᶠ[l] t i
h : ∀ 
i: ?m.2688
i, 
s: ι → Set α
s 
i: ?m.2688
i =ᶠ[
l: Filter α
l] 
t: ι → Set α
t 
i: ?m.2688
i) :
    (⋃ 
i: ?m.2717
i, 
s: ι → Set α
s 
i: ?m.2717
i) =ᶠ[
l: Filter α
l] ⋃ 
i: ?m.2732
i, 
t: ι → Set α
t 
i: ?m.2732
i :=
  (
EventuallyLE.countable_iUnion: ∀ {ι : Sort ?u.2751} {α : Type ?u.2752} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {s t : ι → Set α}, (∀ (i : ι), s i ≤ᶠ[l] t i) → (iUnion fun i => s i) ≤ᶠ[l] iUnion fun i => t i
EventuallyLE.countable_iUnion fun 
i: ?m.2761
i => (
h: ∀ (i : ι), s i =ᶠ[l] t i
h 
i: ?m.2761
i).
le: ∀ {α : Type ?u.2764} {β : Type ?u.2763} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g
le).
antisymm: ∀ {α : Type ?u.2860} {β : Type ?u.2859} [inst : PartialOrder β] {l : Filter α} {f g : α → β},
  f ≤ᶠ[l] g → g ≤ᶠ[l] f → f =ᶠ[l] g
antisymm
    (
EventuallyLE.countable_iUnion: ∀ {ι : Sort ?u.2895} {α : Type ?u.2896} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {s t : ι → Set α}, (∀ (i : ι), s i ≤ᶠ[l] t i) → (iUnion fun i => s i) ≤ᶠ[l] iUnion fun i => t i
EventuallyLE.countable_iUnion fun 
i: ?m.2952
i => (
h: ∀ (i : ι), s i =ᶠ[l] t i
h 
i: ?m.2952
i).
symm: ∀ {α : Type ?u.2955} {β : Type ?u.2954} {f g : α → β} {l : Filter α}, f =ᶠ[l] g → g =ᶠ[l] f
symm.
le: ∀ {α : Type ?u.2962} {β : Type ?u.2961} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g
le)
#align eventually_eq.countable_Union 
EventuallyEq.countable_iUnion: ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i =ᶠ[l] t i) → (iUnion fun i => s i) =ᶠ[l] iUnion fun i => t i
EventuallyEq.countable_iUnion

theorem 
EventuallyLE.countable_bUnion: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) →
        (iUnion fun i => iUnion fun h => s i h) ≤ᶠ[l] iUnion fun i => iUnion fun h => t i h
EventuallyLE.countable_bUnion {
ι: Type u_1
ι : 
Type _: Type (?u.3025+1)
Type _} {
S: Set ι
S : 
Set: Type ?u.3028 → Type ?u.3028
Set 
ι: Type ?u.3025
ι} (
hS: Set.Countable S
hS : 
S: Set ι
S.
Countable: {α : Type ?u.3031} → Set α → Prop
Countable)
    {
s: (i : ι) → i ∈ S → Set α
s 
t: (i : ι) → i ∈ S → Set α
t : ∀ 
i: ?m.3039
i ∈ 
S: Set ι
S, 
Set: Type ?u.3116 → Type ?u.3116
Set 
α: Type ?u.3010
α} (
h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
h : ∀ 
i: ?m.3122
i 
hi: ?m.3125
hi, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.3122
i 
hi: ?m.3125
hi ≤ᶠ[
l: Filter α
l] 
t: (i : ι) → i ∈ S → Set α
t 
i: ?m.3122
i 
hi: ?m.3125
hi) :
    (⋃ 
i: ?m.3198
i ∈ 
S: Set ι
S, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.3198
i ‹_›) ≤ᶠ[
l: Filter α
l] ⋃ 
i: ?m.3257
i ∈ 
S: Set ι
S, 
t: (i : ι) → i ∈ S → Set α
t 
i: ?m.3257
i ‹_› := by
Goals accomplished! 🐙
  
ι✝: Sort ?u.3007

α: Type u_2

β: Type ?u.3013

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

(iUnion fun i => iUnion fun h => s i h) ≤ᶠ[l] iUnion fun i => iUnion fun h => t i hsimp only [
biUnion_eq_iUnion: ∀ {α : Type ?u.3342} {β : Type ?u.3343} (s : Set α) (t : (x : α) → x ∈ s → Set β),
  (iUnion fun x => iUnion fun h => t x h) = iUnion fun x => t ↑x (_ : ↑x ∈ s)
biUnion_eq_iUnion]
ι✝: Sort ?u.3007

α: Type u_2

β: Type ?u.3013

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

(iUnion fun x => s ↑x (_ : ↑x ∈ S)) ≤ᶠ[l] iUnion fun x => t ↑x (_ : ↑x ∈ S)
  
ι✝: Sort ?u.3007

α: Type u_2

β: Type ?u.3013

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

(iUnion fun i => iUnion fun h => s i h) ≤ᶠ[l] iUnion fun i => iUnion fun h => t i hhaveI := 
hS: Set.Countable S
hS.
toEncodable: {α : Type ?u.3691} → {s : Set α} → Set.Countable s → Encodable ↑s
toEncodable
ι✝: Sort ?u.3007

α: Type u_2

β: Type ?u.3013

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

this: Encodable ↑S

(iUnion fun x => s ↑x (_ : ↑x ∈ S)) ≤ᶠ[l] iUnion fun x => t ↑x (_ : ↑x ∈ S)
  
ι✝: Sort ?u.3007

α: Type u_2

β: Type ?u.3013

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

(iUnion fun i => iUnion fun h => s i h) ≤ᶠ[l] iUnion fun i => iUnion fun h => t i hexact 
EventuallyLE.countable_iUnion: ∀ {ι : Sort ?u.3704} {α : Type ?u.3705} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {s t : ι → Set α}, (∀ (i : ι), s i ≤ᶠ[l] t i) → (iUnion fun i => s i) ≤ᶠ[l] iUnion fun i => t i
EventuallyLE.countable_iUnion fun 
i: ?m.3770
i => 
h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
h 
i: ?m.3770
i 
i: ?m.3770
i.
2: ∀ {α : Sort ?u.3850} {p : α → Prop} (self : Subtype p), p ↑self
2
Goals accomplished! 🐙
#align eventually_le.countable_bUnion 
EventuallyLE.countable_bUnion: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) →
        (iUnion fun i => iUnion fun h => s i h) ≤ᶠ[l] iUnion fun i => iUnion fun h => t i h
EventuallyLE.countable_bUnion

theorem 
EventuallyEq.countable_bUnion: ∀ {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) →
        (iUnion fun i => iUnion fun h => s i h) =ᶠ[l] iUnion fun i => iUnion fun h => t i h
EventuallyEq.countable_bUnion {
ι: Type u_1
ι : 
Type _: Type (?u.3989+1)
Type _} {
S: Set ι
S : 
Set: Type ?u.3992 → Type ?u.3992
Set 
ι: Type ?u.3989
ι} (
hS: Set.Countable S
hS : 
S: Set ι
S.
Countable: {α : Type ?u.3995} → Set α → Prop
Countable)
    {
s: (i : ι) → i ∈ S → Set α
s 
t: (i : ι) → i ∈ S → Set α
t : ∀ 
i: ?m.4046
i ∈ 
S: Set ι
S, 
Set: Type ?u.4080 → Type ?u.4080
Set 
α: Type ?u.3974
α} (
h: ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
h : ∀ 
i: ?m.4086
i 
hi: ?m.4089
hi, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.4086
i 
hi: ?m.4089
hi =ᶠ[
l: Filter α
l] 
t: (i : ι) → i ∈ S → Set α
t 
i: ?m.4086
i 
hi: ?m.4089
hi) :
    (⋃ 
i: ?m.4119
i ∈ 
S: Set ι
S, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.4119
i ‹_›) =ᶠ[
l: Filter α
l] ⋃ 
i: ?m.4178
i ∈ 
S: Set ι
S, 
t: (i : ι) → i ∈ S → Set α
t 
i: ?m.4178
i ‹_› :=
  (
EventuallyLE.countable_bUnion: ∀ {α : Type ?u.4251} {l : Filter α} [inst : CountableInterFilter l] {ι : Type ?u.4250} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) →
        (iUnion fun i => iUnion fun h => s i h) ≤ᶠ[l] iUnion fun i => iUnion fun h => t i h
EventuallyLE.countable_bUnion 
hS: Set.Countable S
hS fun 
i: ?m.4267
i 
hi: ?m.4270
hi => (
h: ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
h 
i: ?m.4267
i 
hi: ?m.4270
hi).
le: ∀ {α : Type ?u.4273} {β : Type ?u.4272} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g
le).
antisymm: ∀ {α : Type ?u.4370} {β : Type ?u.4369} [inst : PartialOrder β] {l : Filter α} {f g : α → β},
  f ≤ᶠ[l] g → g ≤ᶠ[l] f → f =ᶠ[l] g
antisymm
    (
EventuallyLE.countable_bUnion: ∀ {α : Type ?u.4406} {l : Filter α} [inst : CountableInterFilter l] {ι : Type ?u.4405} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) →
        (iUnion fun i => iUnion fun h => s i h) ≤ᶠ[l] iUnion fun i => iUnion fun h => t i h
EventuallyLE.countable_bUnion 
hS: Set.Countable S
hS fun 
i: ?m.4447
i 
hi: ?m.4450
hi => (
h: ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
h 
i: ?m.4447
i 
hi: ?m.4450
hi).
symm: ∀ {α : Type ?u.4453} {β : Type ?u.4452} {f g : α → β} {l : Filter α}, f =ᶠ[l] g → g =ᶠ[l] f
symm.
le: ∀ {α : Type ?u.4460} {β : Type ?u.4459} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g
le)
#align eventually_eq.countable_bUnion 
EventuallyEq.countable_bUnion: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) →
        (iUnion fun i => iUnion fun h => s i h) =ᶠ[l] iUnion fun i => iUnion fun h => t i h
EventuallyEq.countable_bUnion

theorem 
EventuallyLE.countable_iInter: ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → (iInter fun i => s i) ≤ᶠ[l] iInter fun i => t i
EventuallyLE.countable_iInter [
Countable: Sort ?u.4544 → Prop
Countable 
ι: Sort ?u.4526
ι] {
s: ι → Set α
s 
t: ι → Set α
t : 
ι: Sort ?u.4526
ι → 
Set: Type ?u.4555 → Type ?u.4555
Set 
α: Type ?u.4529
α} (
h: ∀ (i : ι), s i ≤ᶠ[l] t i
h : ∀ 
i: ?m.4560
i, 
s: ι → Set α
s 
i: ?m.4560
i ≤ᶠ[
l: Filter α
l] 
t: ι → Set α
t 
i: ?m.4560
i) :
    (⋂ 
i: ?m.4632
i, 
s: ι → Set α
s 
i: ?m.4632
i) ≤ᶠ[
l: Filter α
l] ⋂ 
i: ?m.4647
i, 
t: ι → Set α
t 
i: ?m.4647
i :=
  (
eventually_countable_forall: ∀ {ι : Sort ?u.4666} {α : Type ?u.4667} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {p : α → ι → Prop}, Filter.Eventually (fun x => ∀ (i : ι), p x i) l ↔ ∀ (i : ι), Filter.Eventually (fun x => p x i) l
eventually_countable_forall.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
h: ∀ (i : ι), s i ≤ᶠ[l] t i
h).
mono: ∀ {α : Type ?u.4727} {p q : α → Prop} {f : Filter α},
  Filter.Eventually (fun x => p x) f → (∀ (x : α), p x → q x) → Filter.Eventually (fun x => q x) f
mono fun 
_: ?m.4750
_ 
hst: ?m.4753
hst 
hs: ?m.4758
hs =>
    
mem_iInter: ∀ {α : Type ?u.4760} {ι : Sort ?u.4761} {x : α} {s : ι → Set α}, (x ∈ iInter fun i => s i) ↔ ∀ (i : ι), x ∈ s i
mem_iInter.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun 
i: ?m.4790
i => 
hst: ?m.4753
hst 
_: ι
_ (
mem_iInter: ∀ {α : Type ?u.4795} {ι : Sort ?u.4796} {x : α} {s : ι → Set α}, (x ∈ iInter fun i => s i) ↔ ∀ (i : ι), x ∈ s i
mem_iInter.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
hs: ?m.4758
hs 
i: ?m.4790
i)
#align eventually_le.countable_Inter 
EventuallyLE.countable_iInter: ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → (iInter fun i => s i) ≤ᶠ[l] iInter fun i => t i
EventuallyLE.countable_iInter

theorem 
EventuallyEq.countable_iInter: ∀ [inst : Countable ι] {s t : ι → Set α}, (∀ (i : ι), s i =ᶠ[l] t i) → (iInter fun i => s i) =ᶠ[l] iInter fun i => t i
EventuallyEq.countable_iInter [
Countable: Sort ?u.4924 → Prop
Countable 
ι: Sort ?u.4906
ι] {
s: ι → Set α
s 
t: ι → Set α
t : 
ι: Sort ?u.4906
ι → 
Set: Type ?u.4935 → Type ?u.4935
Set 
α: Type ?u.4909
α} (
h: ∀ (i : ι), s i =ᶠ[l] t i
h : ∀ 
i: ?m.4940
i, 
s: ι → Set α
s 
i: ?m.4940
i =ᶠ[
l: Filter α
l] 
t: ι → Set α
t 
i: ?m.4940
i) :
    (⋂ 
i: ?m.4969
i, 
s: ι → Set α
s 
i: ?m.4969
i) =ᶠ[
l: Filter α
l] ⋂ 
i: ?m.4984
i, 
t: ι → Set α
t 
i: ?m.4984
i :=
  (
EventuallyLE.countable_iInter: ∀ {ι : Sort ?u.5003} {α : Type ?u.5004} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {s t : ι → Set α}, (∀ (i : ι), s i ≤ᶠ[l] t i) → (iInter fun i => s i) ≤ᶠ[l] iInter fun i => t i
EventuallyLE.countable_iInter fun 
i: ?m.5013
i => (
h: ∀ (i : ι), s i =ᶠ[l] t i
h 
i: ?m.5013
i).
le: ∀ {α : Type ?u.5016} {β : Type ?u.5015} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g
le).
antisymm: ∀ {α : Type ?u.5112} {β : Type ?u.5111} [inst : PartialOrder β] {l : Filter α} {f g : α → β},
  f ≤ᶠ[l] g → g ≤ᶠ[l] f → f =ᶠ[l] g
antisymm
    (
EventuallyLE.countable_iInter: ∀ {ι : Sort ?u.5147} {α : Type ?u.5148} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {s t : ι → Set α}, (∀ (i : ι), s i ≤ᶠ[l] t i) → (iInter fun i => s i) ≤ᶠ[l] iInter fun i => t i
EventuallyLE.countable_iInter fun 
i: ?m.5204
i => (
h: ∀ (i : ι), s i =ᶠ[l] t i
h 
i: ?m.5204
i).
symm: ∀ {α : Type ?u.5207} {β : Type ?u.5206} {f g : α → β} {l : Filter α}, f =ᶠ[l] g → g =ᶠ[l] f
symm.
le: ∀ {α : Type ?u.5214} {β : Type ?u.5213} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g
le)
#align eventually_eq.countable_Inter 
EventuallyEq.countable_iInter: ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i =ᶠ[l] t i) → (iInter fun i => s i) =ᶠ[l] iInter fun i => t i
EventuallyEq.countable_iInter

theorem 
EventuallyLE.countable_bInter: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) →
        (iInter fun i => iInter fun h => s i h) ≤ᶠ[l] iInter fun i => iInter fun h => t i h
EventuallyLE.countable_bInter {
ι: Type u_1
ι : 
Type _: Type (?u.5277+1)
Type _} {
S: Set ι
S : 
Set: Type ?u.5280 → Type ?u.5280
Set 
ι: Type ?u.5277
ι} (
hS: Set.Countable S
hS : 
S: Set ι
S.
Countable: {α : Type ?u.5283} → Set α → Prop
Countable)
    {
s: (i : ι) → i ∈ S → Set α
s 
t: (i : ι) → i ∈ S → Set α
t : ∀ 
i: ?m.5334
i ∈ 
S: Set ι
S, 
Set: Type ?u.5368 → Type ?u.5368
Set 
α: Type ?u.5262
α} (
h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
h : ∀ 
i: ?m.5374
i 
hi: ?m.5377
hi, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.5374
i 
hi: ?m.5377
hi ≤ᶠ[
l: Filter α
l] 
t: (i : ι) → i ∈ S → Set α
t 
i: ?m.5374
i 
hi: ?m.5377
hi) :
    (⋂ 
i: ?m.5450
i ∈ 
S: Set ι
S, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.5450
i ‹_›) ≤ᶠ[
l: Filter α
l] ⋂ 
i: ?m.5509
i ∈ 
S: Set ι
S, 
t: (i : ι) → i ∈ S → Set α
t 
i: ?m.5509
i ‹_› := by
Goals accomplished! 🐙
  
ι✝: Sort ?u.5259

α: Type u_2

β: Type ?u.5265

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

(iInter fun i => iInter fun h => s i h) ≤ᶠ[l] iInter fun i => iInter fun h => t i hsimp only [
biInter_eq_iInter: ∀ {α : Type ?u.5594} {β : Type ?u.5595} (s : Set α) (t : (x : α) → x ∈ s → Set β),
  (iInter fun x => iInter fun h => t x h) = iInter fun x => t ↑x (_ : ↑x ∈ s)
biInter_eq_iInter]
ι✝: Sort ?u.5259

α: Type u_2

β: Type ?u.5265

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

(iInter fun x => s ↑x (_ : ↑x ∈ S)) ≤ᶠ[l] iInter fun x => t ↑x (_ : ↑x ∈ S)
  
ι✝: Sort ?u.5259

α: Type u_2

β: Type ?u.5265

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

(iInter fun i => iInter fun h => s i h) ≤ᶠ[l] iInter fun i => iInter fun h => t i hhaveI := 
hS: Set.Countable S
hS.
toEncodable: {α : Type ?u.5943} → {s : Set α} → Set.Countable s → Encodable ↑s
toEncodable
ι✝: Sort ?u.5259

α: Type u_2

β: Type ?u.5265

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

this: Encodable ↑S

(iInter fun x => s ↑x (_ : ↑x ∈ S)) ≤ᶠ[l] iInter fun x => t ↑x (_ : ↑x ∈ S)
  
ι✝: Sort ?u.5259

α: Type u_2

β: Type ?u.5265

l: Filter α

inst✝: CountableInterFilter l

ι: Type u_1

S: Set ι

hS: Set.Countable S

s, t: (i : ι) → i ∈ S → Set α

h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi

(iInter fun i => iInter fun h => s i h) ≤ᶠ[l] iInter fun i => iInter fun h => t i hexact 
EventuallyLE.countable_iInter: ∀ {ι : Sort ?u.5956} {α : Type ?u.5957} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
  {s t : ι → Set α}, (∀ (i : ι), s i ≤ᶠ[l] t i) → (iInter fun i => s i) ≤ᶠ[l] iInter fun i => t i
EventuallyLE.countable_iInter fun 
i: ?m.6022
i => 
h: ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
h 
i: ?m.6022
i 
i: ?m.6022
i.
2: ∀ {α : Sort ?u.6102} {p : α → Prop} (self : Subtype p), p ↑self
2
Goals accomplished! 🐙
#align eventually_le.countable_bInter 
EventuallyLE.countable_bInter: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) →
        (iInter fun i => iInter fun h => s i h) ≤ᶠ[l] iInter fun i => iInter fun h => t i h
EventuallyLE.countable_bInter

theorem 
EventuallyEq.countable_bInter: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) →
        (iInter fun i => iInter fun h => s i h) =ᶠ[l] iInter fun i => iInter fun h => t i h
EventuallyEq.countable_bInter {
ι: Type ?u.6241
ι : 
Type _: Type (?u.6241+1)
Type _} {
S: Set ι
S : 
Set: Type ?u.6244 → Type ?u.6244
Set 
ι: Type ?u.6241
ι} (
hS: Set.Countable S
hS : 
S: Set ι
S.
Countable: {α : Type ?u.6247} → Set α → Prop
Countable)
    {
s: (i : ι) → i ∈ S → Set α
s 
t: (i : ι) → i ∈ S → Set α
t : ∀ 
i: ?m.6298
i ∈ 
S: Set ι
S, 
Set: Type ?u.6332 → Type ?u.6332
Set 
α: Type ?u.6226
α} (
h: ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
h : ∀ 
i: ?m.6338
i 
hi: ?m.6341
hi, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.6338
i 
hi: ?m.6341
hi =ᶠ[
l: Filter α
l] 
t: (i : ι) → i ∈ S → Set α
t 
i: ?m.6338
i 
hi: ?m.6341
hi) :
    (⋂ 
i: ?m.6371
i ∈ 
S: Set ι
S, 
s: (i : ι) → i ∈ S → Set α
s 
i: ?m.6371
i ‹_›) =ᶠ[
l: Filter α
l] ⋂ 
i: ?m.6430
i ∈ 
S: Set ι
S, 
t: (i : ι) → i ∈ S → Set α
t 
i: ?m.6430
i ‹_› :=
  (
EventuallyLE.countable_bInter: ∀ {α : Type ?u.6503} {l : Filter α} [inst : CountableInterFilter l] {ι : Type ?u.6502} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) →
        (iInter fun i => iInter fun h => s i h) ≤ᶠ[l] iInter fun i => iInter fun h => t i h
EventuallyLE.countable_bInter 
hS: Set.Countable S
hS fun 
i: ?m.6519
i 
hi: ?m.6522
hi => (
h: ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
h 
i: ?m.6519
i 
hi: ?m.6522
hi).
le: ∀ {α : Type ?u.6525} {β : Type ?u.6524} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g
le).
antisymm: ∀ {α : Type ?u.6622} {β : Type ?u.6621} [inst : PartialOrder β] {l : Filter α} {f g : α → β},
  f ≤ᶠ[l] g → g ≤ᶠ[l] f → f =ᶠ[l] g
antisymm
    (
EventuallyLE.countable_bInter: ∀ {α : Type ?u.6658} {l : Filter α} [inst : CountableInterFilter l] {ι : Type ?u.6657} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) →
        (iInter fun i => iInter fun h => s i h) ≤ᶠ[l] iInter fun i => iInter fun h => t i h
EventuallyLE.countable_bInter 
hS: Set.Countable S
hS fun 
i: ?m.6699
i 
hi: ?m.6702
hi => (
h: ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
h 
i: ?m.6699
i 
hi: ?m.6702
hi).
symm: ∀ {α : Type ?u.6705} {β : Type ?u.6704} {f g : α → β} {l : Filter α}, f =ᶠ[l] g → g =ᶠ[l] f
symm.
le: ∀ {α : Type ?u.6712} {β : Type ?u.6711} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g
le)
#align eventually_eq.countable_bInter 
EventuallyEq.countable_bInter: ∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι},
  Set.Countable S →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) →
        (iInter fun i => iInter fun h => s i h) =ᶠ[l] iInter fun i => iInter fun h => t i h
EventuallyEq.countable_bInter

/-- Construct a filter with countable intersection property. This constructor deduces
`Filter.univ_sets` and `Filter.inter_sets` from the countable intersection property. -/
def 
Filter.ofCountableInter: (l : Set (Set α)) →
  (∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l) → (∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) → Filter α
Filter.ofCountableInter (
l: Set (Set α)
l : 
Set: Type ?u.6796 → Type ?u.6796
Set (
Set: Type ?u.6797 → Type ?u.6797
Set 
α: Type ?u.6781
α))
    (
hp: ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l
hp : ∀ 
S: Set (Set α)
S : 
Set: Type ?u.6801 → Type ?u.6801
Set (
Set: Type ?u.6802 → Type ?u.6802
Set 
α: Type ?u.6781
α), 
S: Set (Set α)
S.
Countable: {α : Type ?u.6806} → Set α → Prop
Countable → 
S: Set (Set α)
S ⊆ 
l: Set (Set α)
l → ⋂₀ 
S: Set (Set α)
S ∈ 
l: Set (Set α)
l)
    (
h_mono: ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
h_mono : ∀ 
s: ?m.6873
s 
t: ?m.6876
t, 
s: ?m.6873
s ∈ 
l: Set (Set α)
l → 
s: ?m.6873
s ⊆ 
t: ?m.6876
t → 
t: ?m.6876
t ∈ 
l: Set (Set α)
l) : 
Filter: Type ?u.6954 → Type ?u.6954
Filter 
α: Type ?u.6781
α
    where
  sets := 
l: Set (Set α)
l
  univ_sets := @
sInter_empty: ∀ {α : Type ?u.6970}, ⋂₀ ∅ = univ
sInter_empty 
α: Type ?u.6781
α ▸ 
hp: ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l
hp 
_: Set (Set α)
_ 
countable_empty: ∀ {α : Type ?u.6980}, Set.Countable ∅
countable_empty (
empty_subset: ∀ {α : Type ?u.6985} (s : Set α), ∅ ⊆ s
empty_subset 
_: Set ?m.6986
_)
  sets_of_superset := 
h_mono: ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
h_mono 
_: Set α
_ 
_: Set α
_
  inter_sets {
s: ?m.7019
s 
t: ?m.7022
t} 
hs: ?m.7025
hs 
ht: ?m.7028
ht := 
sInter_pair: ∀ {α : Type ?u.7030} (s t : Set α), ⋂₀ {s, t} = s ∩ t
sInter_pair 
s: ?m.7019
s 
t: ?m.7022
t ▸
    
hp: ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l
hp 
_: Set (Set α)
_ ((
countable_singleton: ∀ {α : Type ?u.7036} (a : α), Set.Countable {a}
countable_singleton 
_: ?m.7037
_).
insert: ∀ {α : Type ?u.7039} {s : Set α} (a : α), Set.Countable s → Set.Countable (insert a s)
insert 
_: ?m.7044
_) (
insert_subset: ∀ {α : Type ?u.7059} {a : α} {s t : Set α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
insert_subset.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨
hs: ?m.7025
hs, 
singleton_subset_iff: ∀ {α : Type ?u.7079} {a : α} {s : Set α}, {a} ⊆ s ↔ a ∈ s
singleton_subset_iff.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
ht: ?m.7028
ht⟩)
#align filter.of_countable_Inter 
Filter.ofCountableInter: {α : Type u_1} →
  (l : Set (Set α)) →
    (∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l) → (∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) → Filter α
Filter.ofCountableInter

instance 
Filter.countable_Inter_ofCountableInter: ∀ {α : Type u_1} (l : Set (Set α)) (hp : ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l)
  (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l), CountableInterFilter (ofCountableInter l hp h_mono)
Filter.countable_Inter_ofCountableInter (
l: Set (Set α)
l : 
Set: Type ?u.7326 → Type ?u.7326
Set (
Set: Type ?u.7327 → Type ?u.7327
Set 
α: Type ?u.7311
α))
    (
hp: ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l
hp : ∀ 
S: Set (Set α)
S : 
Set: Type ?u.7331 → Type ?u.7331
Set (
Set: Type ?u.7332 → Type ?u.7332
Set 
α: Type ?u.7311
α), 
S: Set (Set α)
S.
Countable: {α : Type ?u.7336} → Set α → Prop
Countable → 
S: Set (Set α)
S ⊆ 
l: Set (Set α)
l → ⋂₀ 
S: Set (Set α)
S ∈ 
l: Set (Set α)
l)
    (
h_mono: ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
h_mono : ∀ 
s: ?m.7403
s 
t: ?m.7406
t, 
s: ?m.7403
s ∈ 
l: Set (Set α)
l → 
s: ?m.7403
s ⊆ 
t: ?m.7406
t → 
t: ?m.7406
t ∈ 
l: Set (Set α)
l) :
    
CountableInterFilter: {α : Type ?u.7484} → Filter α → Prop
CountableInterFilter (
Filter.ofCountableInter: {α : Type ?u.7486} →
  (l : Set (Set α)) →
    (∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l) → (∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) → Filter α
Filter.ofCountableInter 
l: Set (Set α)
l 
hp: ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l
hp 
h_mono: ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
h_mono) :=
  ⟨
hp: ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l
hp⟩
#align filter.countable_Inter_of_countable_Inter 
Filter.countable_Inter_ofCountableInter: ∀ {α : Type u_1} (l : Set (Set α)) (hp : ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l)
  (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l), CountableInterFilter (ofCountableInter l hp h_mono)
Filter.countable_Inter_ofCountableInter

@[simp]
theorem 
Filter.mem_ofCountableInter: ∀ {l : Set (Set α)} (hp : ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l)
  (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) {s : Set α}, s ∈ ofCountableInter l hp h_mono ↔ s ∈ l
Filter.mem_ofCountableInter {
l: Set (Set α)
l : 
Set: Type ?u.7640 → Type ?u.7640
Set (
Set: Type ?u.7641 → Type ?u.7641
Set 
α: Type ?u.7625
α)}
    (
hp: ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l
hp : ∀ 
S: Set (Set α)
S : 
Set: Type ?u.7645 → Type ?u.7645
Set (
Set: Type ?u.7646 → Type ?u.7646
Set 
α: Type ?u.7625
α), 
S: Set (Set α)
S.
Countable: {α : Type ?u.7650} → Set α → Prop
Countable → 
S: Set (Set α)
S ⊆ 
l: Set (Set α)
l → ⋂₀ 
S: Set (Set α)
S ∈ 
l: Set (Set α)
l) (
h_mono: ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
h_mono : ∀ 
s: ?m.7717
s 
t: ?m.7720
t, 
s: ?m.7717
s ∈ 
l: Set (Set α)
l → 
s: ?m.7717
s ⊆ 
t: ?m.7720
t → 
t: ?m.7720
t ∈ 
l: Set (Set α)
l)
    {
s: Set α
s : 
Set: Type ?u.7798 → Type ?u.7798
Set 
α: Type ?u.7625
α} : 
s: Set α
s ∈ 
Filter.ofCountableInter: {α : Type ?u.7807} →
  (l : Set (Set α)) →
    (∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l) → (∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) → Filter α
Filter.ofCountableInter 
l: Set (Set α)
l 
hp: ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l
hp 
h_mono: ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
h_mono ↔ 
s: Set α
s ∈ 
l: Set (Set α)
l :=
  
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align filter.mem_of_countable_Inter 
Filter.mem_ofCountableInter: ∀ {α : Type u_1} {l : Set (Set α)} (hp : ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l)
  (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) {s : Set α}, s ∈ ofCountableInter l hp h_mono ↔ s ∈ l
Filter.mem_ofCountableInter

instance 
countableInterFilter_principal: ∀ (s : Set α), CountableInterFilter (𝓟 s)
countableInterFilter_principal (
s: Set α
s : 
Set: Type ?u.7950 → Type ?u.7950
Set 
α: Type ?u.7935
α) : 
CountableInterFilter: {α : Type ?u.7953} → Filter α → Prop
CountableInterFilter (
𝓟: Set ?m.7956 → Filter ?m.7956
𝓟 
s: Set α
s) :=
  ⟨fun 
_: ?m.7977
_ 
_: ?m.7980
_ 
hS: ?m.7983
hS => 
subset_sInter: ∀ {α : Type ?u.7989} {S : Set (Set α)} {t : Set α}, (∀ (t' : Set α), t' ∈ S → t ⊆ t') → t ⊆ ⋂₀ S
subset_sInter 
hS: ?m.7983
hS⟩
#align countable_Inter_filter_principal 
countableInterFilter_principal: ∀ {α : Type u_1} (s : Set α), CountableInterFilter (𝓟 s)
countableInterFilter_principal

instance 
countableInterFilter_bot: CountableInterFilter ⊥
countableInterFilter_bot : 
CountableInterFilter: {α : Type ?u.8073} → Filter α → Prop
CountableInterFilter (
⊥: ?m.8078
⊥ : 
Filter: Type ?u.8076 → Type ?u.8076
Filter 
α: Type ?u.8058
α) := by
Goals accomplished! 🐙
  
ι: Sort ?u.8055

α: Type ?u.8058

β: Type ?u.8061

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter ⊥rw [
ι: Sort ?u.8055

α: Type ?u.8058

β: Type ?u.8061

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter ⊥← 
principal_empty: ∀ {α : Type ?u.8128}, 𝓟 ∅ = ⊥
principal_empty
ι: Sort ?u.8055

α: Type ?u.8058

β: Type ?u.8061

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter (𝓟 ∅)]
ι: Sort ?u.8055

α: Type ?u.8058

β: Type ?u.8061

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter (𝓟 ∅)
  
ι: Sort ?u.8055

α: Type ?u.8058

β: Type ?u.8061

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter ⊥apply 
countableInterFilter_principal: ∀ {α : Type ?u.8142} (s : Set α), CountableInterFilter (𝓟 s)
countableInterFilter_principal
Goals accomplished! 🐙
#align countable_Inter_filter_bot 
countableInterFilter_bot: ∀ {α : Type u_1}, CountableInterFilter ⊥
countableInterFilter_bot

instance 
countableInterFilter_top: ∀ {α : Type u_1}, CountableInterFilter ⊤
countableInterFilter_top : 
CountableInterFilter: {α : Type ?u.8185} → Filter α → Prop
CountableInterFilter (
⊤: ?m.8190
⊤ : 
Filter: Type ?u.8188 → Type ?u.8188
Filter 
α: Type ?u.8170
α) := by
Goals accomplished! 🐙
  
ι: Sort ?u.8167

α: Type ?u.8170

β: Type ?u.8173

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter ⊤rw [
ι: Sort ?u.8167

α: Type ?u.8170

β: Type ?u.8173

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter ⊤← 
principal_univ: ∀ {α : Type ?u.8227}, 𝓟 univ = ⊤
principal_univ
ι: Sort ?u.8167

α: Type ?u.8170

β: Type ?u.8173

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter (𝓟 univ)]
ι: Sort ?u.8167

α: Type ?u.8170

β: Type ?u.8173

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter (𝓟 univ)
  
ι: Sort ?u.8167

α: Type ?u.8170

β: Type ?u.8173

l: Filter α

inst✝: CountableInterFilter l

CountableInterFilter ⊤apply 
countableInterFilter_principal: ∀ {α : Type ?u.8240} (s : Set α), CountableInterFilter (𝓟 s)
countableInterFilter_principal
Goals accomplished! 🐙
#align countable_Inter_filter_top 
countableInterFilter_top: ∀ {α : Type u_1}, CountableInterFilter ⊤
countableInterFilter_top

instance: ∀ {α : Type u_1} {β : Type u_2} (l : Filter β) [inst : CountableInterFilter l] (f : α → β),
  CountableInterFilter (comap f l)
instance (
l: Filter β
l : 
Filter: Type ?u.8283 → Type ?u.8283
Filter 
β: Type ?u.8271
β) [
CountableInterFilter: {α : Type ?u.8286} → Filter α → Prop
CountableInterFilter 
l: Filter β
l] (
f: α → β
f : 
α: Type ?u.8268
α → 
β: Type ?u.8271
β) :
    
CountableInterFilter: {α : Type ?u.8296} → Filter α → Prop
CountableInterFilter (
comap: {α : Type ?u.8299} → {β : Type ?u.8298} → (α → β) → Filter β → Filter α
comap 
f: α → β
f 
l: Filter β
l) := by
Goals accomplished! 🐙
  
ι: Sort ?u.8265

α: Type ?u.8268

β: Type ?u.8271

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter β

inst✝: CountableInterFilter l

f: α → β

CountableInterFilter (comap f l)refine' ⟨fun 
S: ?m.8325
S 
hSc: ?m.8328
hSc 
hS: ?m.8331
hS => 
_: ⋂₀ S ∈ ?m.8321
_⟩
ι: Sort ?u.8265

α: Type ?u.8268

β: Type ?u.8271

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter β

inst✝: CountableInterFilter l

f: α → β

S: Set (Set α)

hSc: Set.Countable S

hS: ∀ (s : Set α), s ∈ S → s ∈ comap f l

⋂₀ S ∈ comap f l
  
ι: Sort ?u.8265

α: Type ?u.8268

β: Type ?u.8271

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter β

inst✝: CountableInterFilter l

f: α → β

CountableInterFilter (comap f l)choose! 
t: Set α → Set β
t 
htl: ∀ (s : Set α), s ∈ S → t s ∈ l
htl 
ht: ∀ (s : Set α), s ∈ S → f ⁻¹' t s ⊆ s
ht using 
hS: ?m.8331
hS
ι: Sort ?u.8265

α: Type ?u.8268

β: Type ?u.8271

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter β

inst✝: CountableInterFilter l

f: α → β

S: Set (Set α)

hSc: Set.Countable S

t: Set α → Set β

htl: ∀ (s : Set α), s ∈ S → t s ∈ l

ht: ∀ (s : Set α), s ∈ S → f ⁻¹' t s ⊆ s

⋂₀ S ∈ comap f l
  
ι: Sort ?u.8265

α: Type ?u.8268

β: Type ?u.8271

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter β

inst✝: CountableInterFilter l

f: α → β

CountableInterFilter (comap f l)have : (⋂ 
s: ?m.9721
s ∈ 
S: ?m.8325
S, 
t: Set α → Set β
t 
s: ?m.9721
s) ∈ 
l: Filter β
l := (
countable_bInter_mem: ∀ {α : Type ?u.9785} {l : Filter α} [inst : CountableInterFilter l] {ι : Type ?u.9784} {S : Set ι},
  Set.Countable S →
    ∀ {s : (i : ι) → i ∈ S → Set α}, (iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
countable_bInter_mem 
hSc: ?m.8328
hSc).
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
htl: ∀ (s : Set α), s ∈ S → t s ∈ l
htl
ι: Sort ?u.8265

α: Type ?u.8268

β: Type ?u.8271

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter β

inst✝: CountableInterFilter l

f: α → β

S: Set (Set α)

hSc: Set.Countable S

t: Set α → Set β

htl: ∀ (s : Set α), s ∈ S → t s ∈ l

ht: ∀ (s : Set α), s ∈ S → f ⁻¹' t s ⊆ s

this: (iInter fun s => iInter fun h => t s) ∈ l

⋂₀ S ∈ comap f l
  
ι: Sort ?u.8265

α: Type ?u.8268

β: Type ?u.8271

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter β

inst✝: CountableInterFilter l

f: α → β

CountableInterFilter (comap f l)refine' ⟨
_: ?m.9846
_, 
this: (iInter fun s => iInter fun h => t s) ∈ l
this, 
_: ?m.9859
_⟩
ι: Sort ?u.8265

α: Type ?u.8268

β: Type ?u.8271

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter β

inst✝: CountableInterFilter l

f: α → β

S: Set (Set α)

hSc: Set.Countable S

t: Set α → Set β

htl: ∀ (s : Set α), s ∈ S → t s ∈ l

ht: ∀ (s : Set α), s ∈ S → f ⁻¹' t s ⊆ s

this: (iInter fun s => iInter fun h => t s) ∈ l

(f ⁻¹' iInter fun s => iInter fun h => t s) ⊆ ⋂₀ S
  
ι: Sort ?u.8265

α: Type ?u.8268

β: Type ?u.8271

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter β

inst✝: CountableInterFilter l

f: α → β

CountableInterFilter (comap f l)simpa [
preimage_iInter: ∀ {α : Type ?u.9864} {β : Type ?u.9863} {ι : Sort ?u.9865} {f : α → β} {s : ι → Set β},
  (f ⁻¹' iInter fun i => s i) = iInter fun i => f ⁻¹' s i
preimage_iInter] using 
iInter₂_mono: ∀ {α : Type ?u.13381} {ι : Sort ?u.13382} {κ : ι → Sort ?u.13383} {s t : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), s i j ⊆ t i j) → (iInter fun i => iInter fun j => s i j) ⊆ iInter fun i => iInter fun j => t i j
iInter₂_mono 
ht: ∀ (s : Set α), s ∈ S → f ⁻¹' t s ⊆ s
ht
Goals accomplished! 🐙

instance: ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) [inst : CountableInterFilter l] (f : α → β),
  CountableInterFilter (map f l)
instance (
l: Filter α
l : 
Filter: Type ?u.15952 → Type ?u.15952
Filter 
α: Type ?u.15937
α) [
CountableInterFilter: {α : Type ?u.15955} → Filter α → Prop
CountableInterFilter 
l: Filter α
l] (
f: α → β
f : 
α: Type ?u.15937
α → 
β: Type ?u.15940
β) : 
CountableInterFilter: {α : Type ?u.15965} → Filter α → Prop
CountableInterFilter (
map: {α : Type ?u.15968} → {β : Type ?u.15967} → (α → β) → Filter α → Filter β
map 
f: α → β
f 
l: Filter α
l) := by
Goals accomplished! 🐙
  
ι: Sort ?u.15934

α: Type ?u.15937

β: Type ?u.15940

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter α

inst✝: CountableInterFilter l

f: α → β

CountableInterFilter (map f l)refine' ⟨fun 
S: ?m.15994
S 
hSc: ?m.15997
hSc 
hS: ?m.16000
hS => 
_: ⋂₀ S ∈ ?m.15990
_⟩
ι: Sort ?u.15934

α: Type ?u.15937

β: Type ?u.15940

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter α

inst✝: CountableInterFilter l

f: α → β

S: Set (Set β)

hSc: Set.Countable S

hS: ∀ (s : Set β), s ∈ S → s ∈ map f l

⋂₀ S ∈ map f l
  
ι: Sort ?u.15934

α: Type ?u.15937

β: Type ?u.15940

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter α

inst✝: CountableInterFilter l

f: α → β

CountableInterFilter (map f l)simp only [
mem_map: ∀ {α : Type ?u.16036} {β : Type ?u.16035} {f : Filter α} {m : α → β} {t : Set β}, t ∈ map m f ↔ m ⁻¹' t ∈ f
mem_map, 
sInter_eq_biInter: ∀ {α : Type ?u.16067} {s : Set (Set α)}, ⋂₀ s = iInter fun i => iInter fun _h => i
sInter_eq_biInter, 
preimage_iInter₂: ∀ {α : Type ?u.16077} {β : Type ?u.16076} {ι : Sort ?u.16078} {κ : ι → Sort ?u.16079} {f : α → β}
  {s : (i : ι) → κ i → Set β},
  (f ⁻¹' iInter fun i => iInter fun j => s i j) = iInter fun i => iInter fun j => f ⁻¹' s i j
preimage_iInter₂] at 
hS: ?m.16000
hS⊢
ι: Sort ?u.15934

α: Type ?u.15937

β: Type ?u.15940

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter α

inst✝: CountableInterFilter l

f: α → β

S: Set (Set β)

hSc: Set.Countable S

hS: ∀ (s : Set β), s ∈ S → f ⁻¹' s ∈ l

(iInter fun i => iInter fun j => f ⁻¹' i) ∈ l
  
ι: Sort ?u.15934

α: Type ?u.15937

β: Type ?u.15940

l✝: Filter α

inst✝¹: CountableInterFilter l✝

l: Filter α

inst✝: CountableInterFilter l

f: α → β

CountableInterFilter (map f l)exact (
countable_bInter_mem: ∀ {α : Type ?u.16465} {l : Filter α} [inst : CountableInterFilter l] {ι : Type ?u.16464} {S : Set ι},
  Set.Countable S →
    ∀ {s : (i : ι) → i ∈ S → Set α}, (iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
countable_bInter_mem 
hSc: ?m.15997
hSc).
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
hS: ∀ (s : Set β), s ∈ S → f ⁻¹' s ∈ l
hS
Goals accomplished! 🐙

/-- Infimum of two `CountableInterFilter`s is a `CountableInterFilter`. This is useful, e.g.,
to automatically get an instance for `residual α ⊓ 𝓟 s`. -/
instance 
countableInterFilter_inf: ∀ (l₁ l₂ : Filter α) [inst : CountableInterFilter l₁] [inst : CountableInterFilter l₂], CountableInterFilter (l₁ ⊓ l₂)
countableInterFilter_inf (
l₁: Filter α
l₁ 
l₂: Filter α
l₂ : 
Filter: Type ?u.16611 → Type ?u.16611
Filter 
α: Type ?u.16596
α) [
CountableInterFilter: {α : Type ?u.16617} → Filter α → Prop
CountableInterFilter 
l₁: Filter α
l₁]
    [
CountableInterFilter: {α : Type ?u.16623} → Filter α → Prop
CountableInterFilter 
l₂: Filter α
l₂] : 
CountableInterFilter: {α : Type ?u.16628} → Filter α → Prop
CountableInterFilter (
l₁: Filter α
l₁ ⊓ 
l₂: Filter α
l₂) := by
Goals accomplished! 🐙
  
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊓ l₂)refine' ⟨fun 
S: ?m.16681
S 
hSc: ?m.16684
hSc 
hS: ?m.16687
hS => 
_: ⋂₀ S ∈ ?m.16677
_⟩
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

hS: ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊓ l₂

⋂₀ S ∈ l₁ ⊓ l₂
  
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊓ l₂)choose 
s: (s : Set α) → s ∈ S → Set α
s 
hs: ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁
hs 
t: (s : Set α) → s ∈ S → Set α
t 
ht: ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
ht 
hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hst using 
hS: ?m.16687
hS
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s: (s : Set α) → s ∈ S → Set α

hs: ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁

t: (s : Set α) → s ∈ S → Set α

ht: ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

⋂₀ S ∈ l₁ ⊓ l₂
  
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊓ l₂)replace 
hs: (iInter fun i => iInter fun h => s i (_ : i ∈ S)) ∈ l₁
hs : (⋂ 
i: ?m.16802
i ∈ 
S: ?m.16681
S, 
s: (s : Set α) → s ∈ S → Set α
s 
i: ?m.16802
i ‹_›) ∈ 
l₁: Filter α
l₁ := (
countable_bInter_mem: ∀ {α : Type ?u.16867} {l : Filter α} [inst : CountableInterFilter l] {ι : Type ?u.16866} {S : Set ι},
  Set.Countable S →
    ∀ {s : (i : ι) → i ∈ S → Set α}, (iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
countable_bInter_mem 
hSc: ?m.16684
hSc).
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
hs: ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁
hs
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

ht: ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

⋂₀ S ∈ l₁ ⊓ l₂
  
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊓ l₂)replace 
ht: (iInter fun i => iInter fun h => t i (_ : i ∈ S)) ∈ l₂
ht : (⋂ 
i: ?m.16962
i ∈ 
S: ?m.16681
S, 
t: (s : Set α) → s ∈ S → Set α
t 
i: ?m.16962
i ‹_›) ∈ 
l₂: Filter α
l₂ := (
countable_bInter_mem: ∀ {α : Type ?u.17018} {l : Filter α} [inst : CountableInterFilter l] {ι : Type ?u.17017} {S : Set ι},
  Set.Countable S →
    ∀ {s : (i : ι) → i ∈ S → Set α}, (iInter fun i => iInter fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
countable_bInter_mem 
hSc: ?m.16684
hSc).
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
ht: ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
ht
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

⋂₀ S ∈ l₁ ⊓ l₂
  
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊓ l₂)refine' 
mem_of_superset: ∀ {α : Type ?u.17064} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ f
mem_of_superset (
inter_mem_inf: ∀ {α : Type ?u.17070} {f g : Filter α} {s t : Set α}, s ∈ f → t ∈ g → s ∩ t ∈ f ⊓ g
inter_mem_inf 
hs: (iInter fun i => iInter fun h => s i (_ : i ∈ S)) ∈ l₁
hs 
ht: (iInter fun i => iInter fun h => t i (_ : i ∈ S)) ∈ l₂
ht) (
subset_sInter: ∀ {α : Type ?u.17080} {S : Set (Set α)} {t : Set α}, (∀ (t' : Set α), t' ∈ S → t ⊆ t') → t ⊆ ⋂₀ S
subset_sInter fun 
i: ?m.17098
i 
hi: ?m.17101
hi => 
_: ?m.17083 ⊆ i
_)
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

((iInter fun i => iInter fun h => s i h) ∩ iInter fun i => iInter fun h => t i h) ⊆ i
  
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊓ l₂)rw [
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

((iInter fun i => iInter fun h => s i h) ∩ iInter fun i => iInter fun h => t i h) ⊆ i
hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hst 
i: ?m.17098
i 
hi: ?m.17101
hi
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

((iInter fun i => iInter fun h => s i h) ∩ iInter fun i => iInter fun h => t i h) ⊆ s i hi ∩ t i hi]
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

((iInter fun i => iInter fun h => s i h) ∩ iInter fun i => iInter fun h => t i h) ⊆ s i hi ∩ t i hi
  
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊓ l₂)apply 
inter_subset_inter: ∀ {α : Type ?u.17192} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ ∩ s₂ ⊆ t₁ ∩ t₂
inter_subset_inter
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

h₁
(iInter fun i => iInter fun h => s i h) ⊆ s i hi
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

h₂
(iInter fun i => iInter fun h => t i h) ⊆ t i hi 
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

((iInter fun i => iInter fun h => s i h) ∩ iInter fun i => iInter fun h => t i h) ⊆ s i hi ∩ t i hi<;>
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

h₁
(iInter fun i => iInter fun h => s i h) ⊆ s i hi
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

h₂
(iInter fun i => iInter fun h => t i h) ⊆ t i hi 
ι: Sort ?u.16593

α: Type ?u.16596

β: Type ?u.16599

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

s, t: (s : Set α) → s ∈ S → Set α

hst: ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a

hs: (iInter fun i => iInter fun h => s i h) ∈ l₁

ht: (iInter fun i => iInter fun h => t i h) ∈ l₂

i: Set α

hi: i ∈ S

((iInter fun i => iInter fun h => s i h) ∩ iInter fun i => iInter fun h => t i h) ⊆ s i hi ∩ t i hiexact 
iInter_subset_of_subset: ∀ {α : Type ?u.17225} {ι : Sort ?u.17226} {s : ι → Set α} {t : Set α} (i : ι), s i ⊆ t → (iInter fun i => s i) ⊆ t
iInter_subset_of_subset 
i: ?m.17098
i (
iInter_subset: ∀ {β : Type ?u.17258} {ι : Sort ?u.17259} (s : ι → Set β) (i : ι), (iInter fun i => s i) ⊆ s i
iInter_subset 
_: ?m.17240 → Set ?m.17239
_ 
_: ?m.17261
_)
Goals accomplished! 🐙
#align countable_Inter_filter_inf 
countableInterFilter_inf: ∀ {α : Type u_1} (l₁ l₂ : Filter α) [inst : CountableInterFilter l₁] [inst : CountableInterFilter l₂],
  CountableInterFilter (l₁ ⊓ l₂)
countableInterFilter_inf

/-- Supremum of two `CountableInterFilter`s is a `CountableInterFilter`. -/
instance 
countableInterFilter_sup: ∀ (l₁ l₂ : Filter α) [inst : CountableInterFilter l₁] [inst : CountableInterFilter l₂], CountableInterFilter (l₁ ⊔ l₂)
countableInterFilter_sup (
l₁: Filter α
l₁ 
l₂: Filter α
l₂ : 
Filter: Type ?u.17393 → Type ?u.17393
Filter 
α: Type ?u.17378
α) [
CountableInterFilter: {α : Type ?u.17399} → Filter α → Prop
CountableInterFilter 
l₁: Filter α
l₁]
    [
CountableInterFilter: {α : Type ?u.17405} → Filter α → Prop
CountableInterFilter 
l₂: Filter α
l₂] : 
CountableInterFilter: {α : Type ?u.17410} → Filter α → Prop
CountableInterFilter (
l₁: Filter α
l₁ ⊔ 
l₂: Filter α
l₂) := by
Goals accomplished! 🐙
  
ι: Sort ?u.17375

α: Type ?u.17378

β: Type ?u.17381

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊔ l₂)refine' ⟨fun 
S: ?m.17486
S 
hSc: ?m.17489
hSc 
hS: ?m.17492
hS => ⟨
_: ?m.17502
_, 
_: ?m.17503
_⟩⟩
ι: Sort ?u.17375

α: Type ?u.17378

β: Type ?u.17381

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

hS: ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊔ l₂

refine'_1
⋂₀ S ∈ l₁.sets
ι: Sort ?u.17375

α: Type ?u.17378

β: Type ?u.17381

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

hS: ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊔ l₂

refine'_2
⋂₀ S ∈ l₂.sets 
ι: Sort ?u.17375

α: Type ?u.17378

β: Type ?u.17381

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊔ l₂)<;>
ι: Sort ?u.17375

α: Type ?u.17378

β: Type ?u.17381

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

hS: ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊔ l₂

refine'_1
⋂₀ S ∈ l₁.sets
ι: Sort ?u.17375

α: Type ?u.17378

β: Type ?u.17381

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

hS: ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊔ l₂

refine'_2
⋂₀ S ∈ l₂.sets 
ι: Sort ?u.17375

α: Type ?u.17378

β: Type ?u.17381

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊔ l₂)refine' (
countable_sInter_mem: ∀ {α : Type ?u.17526} {l : Filter α} [inst : CountableInterFilter l] {S : Set (Set α)},
  Set.Countable S → (⋂₀ S ∈ l ↔ ∀ (s : Set α), s ∈ S → s ∈ l)
countable_sInter_mem 
hSc: ?m.17489
hSc).
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun 
s: ?m.17565
s 
hs: ?m.17568
hs => 
_: s ∈ ?m.17577
_
ι: Sort ?u.17375

α: Type ?u.17378

β: Type ?u.17381

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

S: Set (Set α)

hSc: Set.Countable S

hS: ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊔ l₂

s: Set α

hs: s ∈ S

refine'_1
s ∈ l₁
  
ι: Sort ?u.17375

α: Type ?u.17378

β: Type ?u.17381

l: Filter α

inst✝²: CountableInterFilter l

l₁, l₂: Filter α

inst✝¹: CountableInterFilter l₁

inst✝: CountableInterFilter l₂

CountableInterFilter (l₁ ⊔ l₂)exacts[(
hS: ?m.17492
hS 
s: ?m.17565
s 
hs: ?m.17568
hs).
1: ∀ {a b : Prop}, a ∧ b → a
1, (
hS: ?m.17492
hS 
s: ?m.17599
s 
hs: ?m.17602
hs).
2: ∀ {a b : Prop}, a ∧ b → b
2]
Goals accomplished! 🐙
#align countable_Inter_filter_sup 
countableInterFilter_sup: ∀ {α : Type u_1} (l₁ l₂ : Filter α) [inst : CountableInterFilter l₁] [inst : CountableInterFilter l₂],
  CountableInterFilter (l₁ ⊔ l₂)
countableInterFilter_sup

namespace Filter

variable (
g: Set (Set α)
g : 
Set: Type ?u.18112 → Type ?u.18112
Set (
Set: Type ?u.18310 → Type ?u.18310
Set 
α: Type ?u.17672
α))

/-- `Filter.CountableGenerateSets g` is the (sets of the)
greatest `countableInterFilter` containing `g`.-/
inductive 
CountableGenerateSets: Set α → Prop
CountableGenerateSets : 
Set: Type ?u.17714 → Type ?u.17714
Set 
α: Type ?u.17694
α → 
Prop: Type
Prop
  | 
basic: ∀ {α : Type u_1} {g : Set (Set α)} {s : Set α}, s ∈ g → CountableGenerateSets g s
basic {
s: Set α
s : 
Set: Type ?u.17719 → Type ?u.17719
Set 
α: Type ?u.17694
α} : 
s: Set α
s ∈ 
g: Set (Set α)
g → 
CountableGenerateSets: Set α → Prop
CountableGenerateSets 
s: Set α
s
  | 
univ: ∀ {α : Type u_1} {g : Set (Set α)}, CountableGenerateSets g univ
univ : 
CountableGenerateSets: Set α → Prop
CountableGenerateSets 
univ: {α : Type ?u.17762} → Set α
univ
  | 
superset: ∀ {α : Type u_1} {g : Set (Set α)} {s t : Set α}, CountableGenerateSets g s → s ⊆ t → CountableGenerateSets g t
superset {
s: Set α
s 
t: Set α
t : 
Set: Type ?u.17766 → Type ?u.17766
Set 
α: Type ?u.17694
α} : 
CountableGenerateSets: Set α → Prop
CountableGenerateSets 
s: Set α
s → 
s: Set α
s ⊆ 
t: Set α
t → 
CountableGenerateSets: Set α → Prop
CountableGenerateSets 
t: Set α
t
  | 
sInter: ∀ {α : Type u_1} {g S : Set (Set α)},
  Set.Countable S → (∀ (s : Set α), s ∈ S → CountableGenerateSets g s) → CountableGenerateSets g (⋂₀ S)
sInter {
S: Set (Set α)
S : 
Set: Type ?u.17804 → Type ?u.17804
Set (
Set: Type ?u.17805 → Type ?u.17805
Set 
α: Type ?u.17694
α)} :
    
S: Set (Set α)
S.
Countable: {α : Type ?u.17809} → Set α → Prop
Countable → (∀ 
s: ?m.17816
s ∈ 
S: Set (Set α)
S, 
CountableGenerateSets: Set α → Prop
CountableGenerateSets 
s: ?m.17816
s) → 
CountableGenerateSets: Set α → Prop
CountableGenerateSets (⋂₀ 
S: Set (Set α)
S)
#align filter.countable_generate_sets 
Filter.CountableGenerateSets: {α : Type u_1} → Set (Set α) → Set α → Prop
Filter.CountableGenerateSets

/-- `Filter.countableGenerate g` is the greatest `countableInterFilter` containing `g`.-/
def 
countableGenerate: Filter α
countableGenerate : 
Filter: Type ?u.18138 → Type ?u.18138
Filter 
α: Type ?u.18119
α :=
  
ofCountableInter: {α : Type ?u.18140} →
  (l : Set (Set α)) →
    (∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l) → (∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) → Filter α
ofCountableInter (
CountableGenerateSets: {α : Type ?u.18143} → Set (Set α) → Set α → Prop
CountableGenerateSets 
g: Set (Set α)
g) (fun 
_: ?m.18151
_ => 
CountableGenerateSets.sInter: ∀ {α : Type ?u.18153} {g S : Set (Set α)},
  Set.Countable S → (∀ (s : Set α), s ∈ S → CountableGenerateSets g s) → CountableGenerateSets g (⋂₀ S)
CountableGenerateSets.sInter) fun 
_: ?m.18183
_ 
_: ?m.18186
_ =>
    
CountableGenerateSets.superset: ∀ {α : Type ?u.18188} {g : Set (Set α)} {s t : Set α}, CountableGenerateSets g s → s ⊆ t → CountableGenerateSets g t
CountableGenerateSets.superset
  --deriving CountableInterFilter
#align filter.countable_generate 
Filter.countableGenerate: {α : Type u_1} → Set (Set α) → Filter α
Filter.countableGenerate

--Porting note: could not de derived
instance: ∀ {α : Type u_1} (g : Set (Set α)), CountableInterFilter (countableGenerate g)
instance : 
CountableInterFilter: {α : Type ?u.18313} → Filter α → Prop
CountableInterFilter (
countableGenerate: {α : Type ?u.18315} → Set (Set α) → Filter α
countableGenerate 
g: Set (Set α)
g) := by
Goals accomplished! 🐙
  
ι: Sort ?u.18291

α: Type ?u.18294

β: Type ?u.18297

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

CountableInterFilter (countableGenerate g)delta 
countableGenerate: {α : Type u_1} → Set (Set α) → Filter α
countableGenerate
ι: Sort ?u.18291

α: Type ?u.18294

β: Type ?u.18297

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

CountableInterFilter
  (ofCountableInter (CountableGenerateSets g)
    (_ :
      ∀ (x : Set (Set α)),
        Set.Countable x → (∀ (s : Set α), s ∈ x → CountableGenerateSets g s) → CountableGenerateSets g (⋂₀ x))
    (_ : ∀ (x x_1 : Set α), CountableGenerateSets g x → x ⊆ x_1 → CountableGenerateSets g x_1));
ι: Sort ?u.18291

α: Type ?u.18294

β: Type ?u.18297

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

CountableInterFilter
  (ofCountableInter (CountableGenerateSets g)
    (_ :
      ∀ (x : Set (Set α)),
        Set.Countable x → (∀ (s : Set α), s ∈ x → CountableGenerateSets g s) → CountableGenerateSets g (⋂₀ x))
    (_ : ∀ (x x_1 : Set α), CountableGenerateSets g x → x ⊆ x_1 → CountableGenerateSets g x_1)) 
ι: Sort ?u.18291

α: Type ?u.18294

β: Type ?u.18297

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

CountableInterFilter (countableGenerate g)infer_instance
Goals accomplished! 🐙

variable {
g: ?m.18416
g}

/-- A set is in the `countableInterFilter` generated by `g` if and only if
it contains a countable intersection of elements of `g`. -/
theorem 
mem_countableGenerate_iff: ∀ {s : Set α}, s ∈ countableGenerate g ↔ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
mem_countableGenerate_iff {
s: Set α
s : 
Set: Type ?u.18441 → Type ?u.18441
Set 
α: Type ?u.18422
α} :
    
s: Set α
s ∈ 
countableGenerate: {α : Type ?u.18451} → Set (Set α) → Filter α
countableGenerate 
g: Set (Set α)
g ↔ ∃ 
S: Set (Set α)
S : 
Set: Type ?u.18468 → Type ?u.18468
Set (
Set: Type ?u.18469 → Type ?u.18469
Set 
α: Type ?u.18422
α), 
S: Set (Set α)
S ⊆ 
g: Set (Set α)
g ∧ 
S: Set (Set α)
S.
Countable: {α : Type ?u.18482} → Set α → Prop
Countable ∧ ⋂₀ 
S: Set (Set α)
S ⊆ 
s: Set α
s := by
Goals accomplished! 🐙
  
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

s ∈ countableGenerate g ↔ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ sconstructor
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

mp
s ∈ countableGenerate g → ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

mpr
(∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s) → s ∈ countableGenerate g 
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

s ∈ countableGenerate g ↔ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s<;>
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

mp
s ∈ countableGenerate g → ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

mpr
(∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s) → s ∈ countableGenerate g 
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

s ∈ countableGenerate g ↔ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ sintro 
h: ?a
h
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

h: s ∈ countableGenerate g

mp
∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
  
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

s ∈ countableGenerate g ↔ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s·
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

h: s ∈ countableGenerate g

mp
∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s 
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

h: s ∈ countableGenerate g

mp
∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

h: ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s

mpr
s ∈ countableGenerate ginduction' 
h: ?a
h with 
s: Set ?m.18559
s 
hs: s ∈ ?m.18560
hs 
s: Set ?m.18559
s 
t: Set ?m.18559
t _ 
st: s ⊆ t
st 
ih: ?m.18561 s a✝
ih 
S: Set (Set ?m.18559)
S 
Sct: Set.Countable S
Sct _ 
ih: ∀ (s : Set ?m.18559) (a : s ∈ S), ?m.18561 s (_ : CountableGenerateSets ?m.18560 s)
ih
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s✝, s: Set α

hs: s ∈ g

mp.basic
∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

mp.univ
∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ univ
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s✝, s, t: Set α

a✝: CountableGenerateSets g s

st: s ⊆ t

ih: ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s

mp.superset
∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ t
ι: Sort ?u.18419

α: Type u_1

β: Type ?u.18425

l: Filter α

inst✝: CountableInterFilter l

g: Set (Set α)

s: Set α

S: Set (Set α)

Sct: Set.Countable S

a✝: ∀ (s : Set α), s ∈ S → CountableGenerateSets g s

ih: ∀ (s : Set α), s ∈ S → ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s

mp.sInter
∃ S_1, S_1 ⊆ g ∧ Set.Countable S_1 ∧ ⋂₀ S_1 ⊆ ⋂₀ S