-- Mathlib/Topology/Bases.lean
theorem isTopologicalBasis_of_subbasis {s : Set (Set α)} (hs : t = generateFrom s) :
    IsTopologicalBasis ((fun f => ⋂₀ f) '' { f : Set (Set α) | f.Finite ∧ f ⊆ s })

Proof state:
case refine_3.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : t.Finite
htb : t ⊆ s
⊢ IsOpen ((fun f => ⋂₀ f) t)

Tactic:
exact hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t₁ : Set (Set α)
hft₁ : t₁.Finite
ht₁b : t₁ ⊆ s
t₂ : Set (Set α)
hft₂ : t₂.Finite
ht₂b : t₂ ⊆ s
x : α
h : x ∈ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂
⊢ ∃ t₃ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, x ∈ t₃ ∧ t₃ ⊆ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂

Tactic:
exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩

Result:
no goals

Proof state:
case refine_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ s_1 ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, IsOpen s_1

Tactic:
rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩

Result:
case refine_3.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : t.Finite
htb : t ⊆ s
⊢ IsOpen ((fun f => ⋂₀ f) t)

Proof state:
case refine_1
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ t₁ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
    ∀ t₂ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
      ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h

Result:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t₁ : Set (Set α)
hft₁ : t₁.Finite
ht₁b : t₁ ⊆ s
t₂ : Set (Set α)
hft₂ : t₂.Finite
ht₂b : t₂ ⊆ s
x : α
h : x ∈ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂
⊢ ∃ t₃ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, x ∈ t₃ ∧ t₃ ⊆ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂

Proof state:
case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (a : α), ∃ i, ∃ (_ : i ∈ {f | f.Finite ∧ f ⊆ s}), a ∈ ⋂₀ i

Tactic:
exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩

Result:
no goals

Proof state:
case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃₀ ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}) = univ

Tactic:
rw [sUnion_image, iUnion₂_eq_univ_iff]

Result:
case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (a : α), ∃ i, ∃ (_ : i ∈ {f | f.Finite ∧ f ⊆ s}), a ∈ ⋂₀ i

Proof state:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hs : t = generateFrom s
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})

Tactic:
subst t

Result:
α : Type u
s : Set (Set α)
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})

Proof state:
α : Type u
s : Set (Set α)
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})

Tactic:
letI := generateFrom s

Result:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})

Proof state:
case refine_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ ⋂₀ {t} ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}

Tactic:
exact ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})

Tactic:
refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩

Result:
case refine_1
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ t₁ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
    ∀ t₂ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
      ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃₀ ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}) = univ

case refine_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ s_1 ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, IsOpen s_1

case refine_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ t ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}

Proof state:
case refine_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ t ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}

Tactic:
rw [← sInter_singleton t]

Result:
case refine_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ ⋂₀ {t} ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}