case mp
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
h : s ∈ countableGenerate g
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s

case mpr
ι : 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
⊢ 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
constructor <;> intro h
case mpr.intro.intro.intro
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : Set.Countable S
hS : ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
case mpr
ι : 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
⊢ s ∈ countableGenerate g
rcases h with ⟨S, Sg, Sct, hS⟩
case mpr.intro.intro.intro
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : Set.Countable S
hS : ⋂₀ S ⊆ s
⊢ ∀ (s : Set α), s ∈ S → s ∈ countableGenerate g
case mpr.intro.intro.intro
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : Set.Countable S
hS : ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
refine' mem_of_superset ((countable_sInter_mem Sct).mpr _) hS
case mpr.intro.intro.intro
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : Set.Countable S
hS : ⋂₀ S ⊆ s✝
s : Set α
H : s ∈ S
⊢ s ∈ countableGenerate g
case mpr.intro.intro.intro
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : Set.Countable S
hS : ⋂₀ S ⊆ s
⊢ ∀ (s : Set α), s ∈ S → s ∈ countableGenerate g
intro s H
no goals
case mpr.intro.intro.intro
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : Set.Countable S
hS : ⋂₀ S ⊆ s✝
s : Set α
H : s ∈ S
⊢ s ∈ countableGenerate g
exact CountableGenerateSets.basic (Sg H)
case mp.basic
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ s : Set α
hs : s ∈ g
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s

case mp.univ
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ univ

case mp.superset
ι : 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
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ t

case mp.sInter
ι : 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
⊢ ∃ S_1, S_1 ⊆ g ∧ Set.Countable S_1 ∧ ⋂₀ S_1 ⊆ ⋂₀ S
case mp
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
h : s ∈ countableGenerate g
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
induction' h with s hs s t _ st ih S Sct _ ih
case mp.sInter
ι : 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
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∃ S_1, S_1 ⊆ g ∧ Set.Countable S_1 ∧ ⋂₀ S_1 ⊆ ⋂₀ S
case mp.sInter
ι : 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
⊢ ∃ S_1, S_1 ⊆ g ∧ Set.Countable S_1 ∧ ⋂₀ S_1 ⊆ ⋂₀ S
choose T Tg Tct hT using ih
case mp.sInter
ι : 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
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ (⋂₀ ⋃ (s : Set α) (H : s ∈ S), T s H) ⊆ ⋂₀ S
case mp.sInter
ι : 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
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∃ S_1, S_1 ⊆ g ∧ Set.Countable S_1 ∧ ⋂₀ S_1 ⊆ ⋂₀ S
refine' ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, _⟩
case mp.sInter.h
ι : 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
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∀ (t' : Set α), t' ∈ S → (⋂₀ ⋃ (s : Set α) (H : s ∈ S), T s H) ⊆ t'
case mp.sInter
ι : 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
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ (⋂₀ ⋃ (s : Set α) (H : s ∈ S), T s H) ⊆ ⋂₀ S
apply subset_sInter
case mp.sInter.h
ι : 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
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
s : Set α
H : s ∈ S
⊢ (⋂₀ ⋃ (s : Set α) (H : s ∈ S), T s H) ⊆ s
case mp.sInter.h
ι : 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
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∀ (t' : Set α), t' ∈ S → (⋂₀ ⋃ (s : Set α) (H : s ∈ S), T s H) ⊆ t'
intro s H
no goals
case mp.sInter.h
ι : 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
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
s : Set α
H : s ∈ S
⊢ (⋂₀ ⋃ (s : Set α) (H : s ∈ S), T s H) ⊆ s
refine' subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)
no goals
case mp.basic
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ s : Set α
hs : s ∈ g
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
exact ⟨{s}, by simp [hs, subset_refl]⟩
no goals
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ s : Set α
hs : s ∈ g
⊢ {s} ⊆ g ∧ Set.Countable {s} ∧ ⋂₀ {s} ⊆ s
simp [hs, subset_refl]
no goals
case mp.univ
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ univ
exact ⟨∅, by simp⟩
no goals
ι : Sort ?u.18419
α : Type u_1
β : Type ?u.18425
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
⊢ ∅ ⊆ g ∧ Set.Countable ∅ ∧ ⋂₀ ∅ ⊆ univ
simp
case mp.superset
ι : 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
S : Set (Set α)
⊢ S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s → S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ t
case mp.superset
ι : 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
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ t
refine' Exists.imp (fun S => _) ih
no goals
case mp.superset
ι : 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
S : Set (Set α)
⊢ S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s → S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ t
tauto
no goals
ι : 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
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ (⋃ (s : Set α) (H : s ∈ S), T s H) ⊆ g
simpa