case mp
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
h : U ∈ generate s
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ U

case mpr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
h : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
⊢ U ∈ generate s ↔ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ U
constructor <;> intro h
case mp.basic
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ : Set α
a✝ : s✝ ∈ s
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝

case mp.univ
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ univ

case mp.superset
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : s✝ ⊆ t✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝

case mp.inter
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
a_ih✝¹ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝ ∩ t✝
case mp
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
h : U ∈ generate s
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ U
induction h
case mp.univ
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ univ

case mp.superset
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : s✝ ⊆ t✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝

case mp.inter
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
a_ih✝¹ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝ ∩ t✝
case mp.basic
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ : Set α
a✝ : s✝ ∈ s
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝

case mp.univ
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ univ

case mp.superset
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : s✝ ⊆ t✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝

case mp.inter
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
a_ih✝¹ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝ ∩ t✝
case basic V V_in =>
  exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
case mp.superset
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : s✝ ⊆ t✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝

case mp.inter
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
a_ih✝¹ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝ ∩ t✝
case mp.univ
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ univ

case mp.superset
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : s✝ ⊆ t✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝

case mp.inter
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
a_ih✝¹ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝ ∩ t✝
case univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
case mp.inter
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
a_ih✝¹ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝ ∩ t✝
case mp.superset
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : s✝ ⊆ t✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝

case mp.inter
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
a_ih✝¹ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝ ∩ t✝
case superset V W _ hVW hV =>
  rcases hV with ⟨t, hts, ht, htV⟩
  exact ⟨t, hts, ht, htV.trans hVW⟩
no goals
case mp.inter
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝¹ t : Set α
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
a_ih✝¹ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝
a_ih✝ : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ s✝ ∩ t✝
case inter V W _ _ 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⟩
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U V : Set α
V_in : V ∈ s
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ V
exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ univ
exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t✝ : Set α
s : Set (Set α)
U V W : Set α
a✝ : GenerateSets s V
hVW : V ⊆ W
t : Set (Set α)
hts : t ⊆ s
ht : Set.Finite t
htV : ⋂₀ t ⊆ V
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ W
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U V W : Set α
a✝ : GenerateSets s V
hVW : V ⊆ W
hV : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ V
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ W
rcases hV with ⟨t, hts, ht, htV⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t✝ : Set α
s : Set (Set α)
U V W : Set α
a✝ : GenerateSets s V
hVW : V ⊆ W
t : Set (Set α)
hts : t ⊆ s
ht : Set.Finite t
htV : ⋂₀ t ⊆ V
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ W
exact ⟨t, hts, ht, htV.trans hVW⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t✝ : Set α
s : Set (Set α)
U V W : Set α
a✝¹ : GenerateSets s V
a✝ : GenerateSets s W
t : Set (Set α)
hts : t ⊆ s
ht : Set.Finite t
htV : ⋂₀ t ⊆ V
u : Set (Set α)
hus : u ⊆ s
hu : Set.Finite u
huW : ⋂₀ u ⊆ W
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ V ∩ W
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U V W : Set α
a✝¹ : GenerateSets s V
a✝ : GenerateSets s W
hV : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ V
hW : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ W
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ V ∩ W
rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
no goals
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t✝ : Set α
s : Set (Set α)
U V W : Set α
a✝¹ : GenerateSets s V
a✝ : GenerateSets s W
t : Set (Set α)
hts : t ⊆ s
ht : Set.Finite t
htV : ⋂₀ t ⊆ V
u : Set (Set α)
hus : u ⊆ s
hu : Set.Finite u
huW : ⋂₀ u ⊆ W
⊢ ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ V ∩ W
exact
  ⟨t ∪ u, union_subset hts hus, ht.union hu,
    (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩
case mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t✝ : Set α
s : Set (Set α)
U : Set α
t : Set (Set α)
hts : t ⊆ s
tfin : Set.Finite t
h : ⋂₀ t ⊆ U
⊢ U ∈ generate s
case mpr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t : Set α
s : Set (Set α)
U : Set α
h : ∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s
rcases h with ⟨t, hts, tfin, h⟩
no goals
case mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.51737
ι : Sort x
f g : Filter α
s✝ t✝ : Set α
s : Set (Set α)
U : Set α
t : Set (Set α)
hts : t ⊆ s
tfin : Set.Finite t
h : ⋂₀ t ⊆ U
⊢ U ∈ generate s
exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h