-- Mathlib/Order/Filter/Finite.lean
theorem mem_generate_iff {s : Set <| Set α} {U : Set α} :
    U ∈ generate s ↔ ∃ t ⊆ s, Set.Finite t ∧ ⋂₀ t ⊆ U

Proof state:
case mp.univ
α : Type u
s : Set (Set α)
U : Set α
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ univ

Tactic:
exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩

Result:
no goals

Proof state:
case mp.superset.intro.intro.intro
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝ : GenerateSets s s✝
hVW : s✝ ⊆ t✝
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ t✝

Tactic:
exact ⟨t, hts, ht, htV.trans hVW⟩

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
U : Set α
⊢ U ∈ generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

case mpr
α : Type u
s : Set (Set α)
U : Set α
h : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s

Proof state:
case mp.inter
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝
hW : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝ ∩ t✝

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

Result:
case mp.inter.intro.intro.intro.intro.intro.intro
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s✝
u : Set (Set α)
hus : u ⊆ s
hu : u.Finite
huW : ⋂₀ u ⊆ t✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝ ∩ t✝

Proof state:
case mpr.intro.intro.intro
α : Type u
s : Set (Set α)
U : Set α
t : Set (Set α)
hts : t ⊆ s
tfin : t.Finite
h : ⋂₀ t ⊆ U
⊢ U ∈ generate s

Tactic:
exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h

Result:
no goals

Proof state:
case mp
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

Tactic:
induction h with
| @basic V V_in =>
  exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
| univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
| superset _ hVW hV =>
  rcases hV with ⟨t, hts, ht, htV⟩
  exact ⟨t, hts, ht, htV.trans hVW⟩
| inter _ _ 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⟩

Result:
no goals

Proof state:
case mp.basic
α : Type u
s : Set (Set α)
U V : Set α
V_in : V ∈ s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ V

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

Result:
no goals

Proof state:
case mp.inter.intro.intro.intro.intro.intro.intro
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s✝
u : Set (Set α)
hus : u ⊆ s
hu : u.Finite
huW : ⋂₀ u ⊆ t✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝ ∩ t✝

Tactic:
exact
  ⟨t ∪ u, union_subset hts hus, ht.union hu,
    (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩

Result:
no goals

Proof state:
case mpr
α : Type u
s : Set (Set α)
U : Set α
h : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s

Tactic:
rcases h with ⟨t, hts, tfin, h⟩

Result:
case mpr.intro.intro.intro
α : Type u
s : Set (Set α)
U : Set α
t : Set (Set α)
hts : t ⊆ s
tfin : t.Finite
h : ⋂₀ t ⊆ U
⊢ U ∈ generate s

Proof state:
case mp.superset
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝ : GenerateSets s s✝
hVW : s✝ ⊆ t✝
hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ t✝

Tactic:
rcases hV with ⟨t, hts, ht, htV⟩

Result:
case mp.superset.intro.intro.intro
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝ : GenerateSets s s✝
hVW : s✝ ⊆ t✝
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ t✝