case mp
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : f ≤ countableGenerate g
⊢ g ⊆ f.sets

case mpr
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
⊢ f ≤ countableGenerate g
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g ↔ g ⊆ f.sets
constructor <;> intro h
case mpr
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
hs : s ∈ countableGenerate g
⊢ s ∈ f
case mpr
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
⊢ f ≤ countableGenerate g
intro s hs
case mpr.basic
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s✝ s : Set α
hs : s ∈ g
⊢ s ∈ f

case mpr.univ
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
⊢ univ ∈ f

case mpr.superset
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s✝ s t : Set α
a✝ : CountableGenerateSets g s
st : s ⊆ t
ih : s ∈ f
⊢ t ∈ f

case mpr.sInter
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
S : Set (Set α)
Sct : Set.Countable S
a✝ : ∀ (s : Set α), s ∈ S → CountableGenerateSets g s
ih : ∀ (s : Set α), s ∈ S → s ∈ f
⊢ ⋂₀ S ∈ f
case mpr
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
hs : s ∈ countableGenerate g
⊢ s ∈ f
induction' hs with s hs s t _ st ih S Sct _ ih
no goals
case mpr.sInter
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
S : Set (Set α)
Sct : Set.Countable S
a✝ : ∀ (s : Set α), s ∈ S → CountableGenerateSets g s
ih : ∀ (s : Set α), s ∈ S → s ∈ f
⊢ ⋂₀ S ∈ f
exact (countable_sInter_mem Sct).mpr ih
no goals
case mp
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : f ≤ countableGenerate g
⊢ g ⊆ f.sets
exact subset_trans (fun s => CountableGenerateSets.basic) h
no goals
case mpr.basic
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s✝ s : Set α
hs : s ∈ g
⊢ s ∈ f
exact h hs
no goals
case mpr.univ
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
⊢ univ ∈ f
exact univ_mem
no goals
case mpr.superset
ι : Sort ?u.24349
α : Type u_1
β : Type ?u.24355
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s✝ s t : Set α
a✝ : CountableGenerateSets g s
st : s ⊆ t
ih : s ∈ f
⊢ t ∈ f
exact mem_of_superset ih st