awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
⊢ image (α := Opens α) SetLike.coe
      {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' (↑U : Set β), is_open' := ⋯ : Opens α } = x} =
    preimage f '' SetLike.coe '' B
have h₁ : ∀ (x : Set α),
  x ∈
      image (α := Opens α) SetLike.coe
        {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' (↑U : Set β), is_open' := sorry : Opens α } = x} ↔
    x ∈ preimage f '' SetLike.coe '' B
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
⊢ IsCompactElement s ↔ IsCompact (↑s : Set α)
have rw : (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1) ↔
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
Tactic: rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
have refine_1 : (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1) →
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
Tactic: refine ⟨?_, fun H ι U hU => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
refine_1 :
  (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1) →
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
have refine_2 : ∀
  (H :
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i)
  (ι : Type u_2) (U : ι → Opens α) (hU : s ≤ iSup U), ∃ (t : Finset ι), s ≤ t.sup U
Tactic: refine ⟨?_, fun H ι U hU => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
hU' : (↑s : Set α) ⊆ ⋃ (i : ι), U i
⊢ ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
have refine_1 : ∀ (t : Finset ι) (ht : s ≤ t.sup fun (i : ι) ↦ { carrier := U i, is_open' := sorry }),
  ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
Tactic: obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
hU' : (↑s : Set α) ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }
⊢ ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
have refine_1 : (↑(t.sup fun (i : ι) ↦ { carrier := U i, is_open' := sorry : Opens α }) : Set α) ⊆ ⋃ i ∈ t, U i
Tactic: refine ⟨t, Set.Subset.trans ht ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
hU' : (↑s : Set α) ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }
⊢ (↑(t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ : Opens α }) : Set α) ⊆ ⋃ i ∈ t, U i
have refine_1 : Subset.{u_2} (α := Set α) (⨆ a ∈ t, comp (β := Opens α) SetLike.coe (fun (i : ι) ↦ { carrier := U i, is_open' := sorry }) a)
  (⨆ a ∈ t, comp (β := Opens α) SetLike.coe (fun (i : ι) ↦ { carrier := U i, is_open' := sorry }) a)
Tactic: rw [coe_finset_sup, Finset.sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ∃ (t : Finset ι), s ≤ t.sup U
have refine_2 : ∀ (t : Finset ι) (ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)), ∃ (t : Finset ι), s ≤ t.sup U
Tactic: obtain ⟨t, ht⟩ :=
      H (fun i => U i) (fun i => (U i).isOpen) (by simpa using show (s : Set α) ⊆ ↑(iSup U) from hU)
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)
⊢ ∃ (t : Finset ι), s ≤ t.sup U
have refine_2 : ⋃ i ∈ t, (↑(U i) : Set α) ⊆ (↑(t.sup U) : Set α)
Tactic: refine ⟨t, Set.Subset.trans ht ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)
⊢ ⋃ i ∈ t, (↑(U i) : Set α) ⊆ (↑(t.sup U) : Set α)
have refine_2 : ∀ (i : ι) (i_1 : i ∈ t), (↑(U i) : Set α) ⊆ (↑(t.sup U) : Set α)
Tactic: simp only [Set.iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.Opens (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)
⊢ ∀ (i : ι) (i_1 : i ∈ t), (↑(U i) : Set α) ⊆ (↑(t.sup U) : Set α)
have refine_2 : ∀ i ∈ t, U i ≤ t.sup U
Tactic: change ∀ i ∈ t, U i ≤ t.sup U
-- Lean 4 proof step from Mathlib.Topology.Sets.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
s t : ClopenUpperSet α
h : Eq.{u_1 + 1} (α := Set α) ((fun (s : ClopenUpperSet α) ↦ s.carrier) s) ((fun (s : ClopenUpperSet α) ↦ s.carrier) t)
⊢ s = t
have obtain : ∀ (carrier : Set α) (isClopen' : IsClopen carrier)
  (upper' : IsUpperSet { carrier := carrier, isClopen' := isClopen' : Clopens α }.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (s : ClopenUpperSet α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen', upper' := upper' })
      ((fun (s : ClopenUpperSet α) ↦ s.carrier) t)),
  { carrier := carrier, isClopen' := isClopen', upper' := upper' : ClopenUpperSet α } = t
Tactic: obtain ⟨⟨_, _⟩, _⟩ := s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
t : ClopenUpperSet α
carrier : Set α
isClopen' : IsClopen carrier
upper' : IsUpperSet { carrier := carrier, isClopen' := isClopen' : Clopens α }.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : ClopenUpperSet α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen', upper' := upper' })
    ((fun (s : ClopenUpperSet α) ↦ s.carrier) t)
⊢ { carrier := carrier, isClopen' := isClopen', upper' := upper' : ClopenUpperSet α } = t
have obtain : ∀ (carrier_1 : Set α) (isClopen'_1 : IsClopen carrier_1)
  (upper'_1 : IsUpperSet { carrier := carrier_1, isClopen' := isClopen'_1 : Clopens α }.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (s : ClopenUpperSet α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen', upper' := upper' })
      ((fun (s : ClopenUpperSet α) ↦ s.carrier)
        { carrier := carrier_1, isClopen' := isClopen'_1, upper' := upper'_1 })),
  { carrier := carrier, isClopen' := isClopen', upper' := upper' : ClopenUpperSet α } =
    { carrier := carrier_1, isClopen' := isClopen'_1, upper' := upper'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed[TopologicalSpace.vietoris α] (𝒫 F)
have simp_rw : IsOpen[TopologicalSpace.vietoris α] {a : Set α | (a ∩ Fᶜ).Nonempty}
Tactic: simp_rw [powerset, ← isOpen_compl_iff, compl_setOf, ← inter_compl_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed[TopologicalSpace.vietoris α] {s : Set α | (s ∩ F).Nonempty}
have simp_rw : IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ Fᶜ}ᶜ
Tactic: simp_rw +singlePass [← compl_compl F, inter_compl_nonempty_iff, ← compl_setOf]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsClopen (X := Set α) {∅}
have rw : IsClopen.{u_1} (X := Set α) (𝒫 ∅)
Tactic: rw [← powerset_empty]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsTopologicalBasis.{u_1} (α := Set α)
    ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
have refine_1 : ∀ (u : Set (Set α)),
  Membership.mem (γ := Set (Set (Set α)))
      ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
        {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
      u →
    IsOpen[generateFrom
          (powerset '' {U : Set α | IsOpen[inst] U} ∪
            (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
      u
Tactic: refine isTopologicalBasis_of_subbasis rfl |>.isTopologicalBasis_of_exists_subset ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
refine_1 :
  ∀ (u : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
        u →
      IsOpen[generateFrom
            (powerset '' {U : Set α | IsOpen[inst] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
        u
⊢ IsTopologicalBasis.{u_1} (α := Set α)
    ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
have refine_2 : ∀ (u : Set (Set α)),
  Membership.mem (γ := Set (Set (Set α)))
      ((fun (f : Set (Set (Set α))) ↦ ⋂₀ f) ''
        {f : Set (Set (Set α)) |
          f.Finite ∧
            f ⊆
              powerset '' {U : Set α | IsOpen[inst] U} ∪
                (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}})
      u →
    ∀ x ∈ u,
      ∃ (v : Set (Set α)),
        Membership.mem (γ := Set (Set (Set α)))
            ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
            v ∧
          x ∈ v ∧ v ⊆ u
Tactic: refine isTopologicalBasis_of_subbasis rfl |>.isTopologicalBasis_of_exists_subset ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ ∀ (u : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
        u →
      IsOpen[generateFrom
            (powerset '' {U : Set α | IsOpen[inst] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
        u
have refine_1 : ∀ ⦃x : Set (Set α)⦄,
  Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x →
    IsOpen[generateFrom
          (powerset '' {U : Set α | IsOpen[inst] U} ∪
            (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
      {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}
Tactic: rw [forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ ∀ (u : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (f : Set (Set (Set α))) ↦ ⋂₀ f) ''
          {f : Set (Set (Set α)) |
            f.Finite ∧
              f ⊆
                powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}})
        u →
      ∀ x ∈ u,
        ∃ (v : Set (Set α)),
          Membership.mem (γ := Set (Set (Set α)))
              ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
              v ∧
            x ∈ v ∧ v ⊆ u
have refine_2 : ∀ ⦃x : Set (Set (Set α))⦄,
  Membership.mem (γ := Set (Set (Set (Set α))))
      {f : Set (Set (Set α)) |
        f.Finite ∧
          f ⊆
            powerset '' {U : Set α | IsOpen[inst] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}}
      x →
    ∀ x_1 ∈ ⋂₀ x,
      ∃ (v : Set (Set α)),
        Membership.mem (γ := Set (Set (Set α)))
            ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
            v ∧
          x_1 ∈ v ∧ v ⊆ ⋂₀ x
Tactic: rw [forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
u : Set (Set α)
⊢ Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} u →
    IsOpen[generateFrom
          (powerset '' {U : Set α | IsOpen[inst] U} ∪
            (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
      {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have refine_1 : ∀ (hu₁ : u.Finite) (hu₂ : ∀ U ∈ u, IsOpen[inst] U),
  IsOpen[generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
    {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: ⟨hu₁, hu₂⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
⊢ IsOpen[generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
    {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have refine_1 : IsOpen[generateFrom
      (powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
  ({a : Set α | a ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x : Set α | (x ∩ i).Nonempty})
Tactic: simp_rw [setOf_and, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set (Set (Set α))
⊢ Membership.mem (γ := Set (Set (Set (Set α))))
      {f : Set (Set (Set α)) |
        f.Finite ∧
          f ⊆
            powerset '' {U : Set α | IsOpen[inst] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}}
      t →
    ∀ x ∈ ⋂₀ t,
      ∃ (v : Set (Set α)),
        Membership.mem (γ := Set (Set (Set α)))
            ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
            v ∧
          x ∈ v ∧ v ⊆ ⋂₀ t
have refine_2 : ∀ (ht₁ : t.Finite)
  (ht₂ :
    t ⊆
      powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}),
  ∀ x ∈ ⋂₀ t,
    ∃ (v : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α)))
          ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
          v ∧
        x ∈ v ∧ v ⊆ ⋂₀ t
Tactic: ⟨ht₁, ht₂⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ :
  t ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
s : Set α
hs : s ∈ ⋂₀ t
⊢ ∃ (v : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
        v ∧
      s ∈ v ∧ v ⊆ ⋂₀ t
have refine_2 : ∃ (x : Set (Set α)),
  Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
    Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} s ∧
      {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
Tactic: rw [exists_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ :
  t ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
s : Set α
hs : s ∈ ⋂₀ t
⊢ ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} s ∧
        {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
have refine_2 : ∀ (hs : ∅ ∈ ⋂₀ t),
  ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∅ ∧
        {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
Tactic: rcases eq_empty_or_nonempty s with rfl | _
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ :
  t ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
s : Set α
hs : s ∈ ⋂₀ t
refine_2 :
  ∀ (hs : ∅ ∈ ⋂₀ t),
    ∃ (x : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
        Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∅ ∧
          {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
⊢ ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} s ∧
        {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
have refine_2₁ : s.Nonempty →
  ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} s ∧
        {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
Tactic: rcases eq_empty_or_nonempty s with rfl | _
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ :
  t ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hs : ∅ ∈ ⋂₀ t
⊢ ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∅ ∧
        {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
have refine_2 : Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} ∅ ∧
  Membership.mem (γ := Set (Set α))
      {s : Set α | s ⊆ ⋃₀ ∅ ∧ ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → (s ∩ U).Nonempty} ∅ ∧
    {s : Set α | s ⊆ ⋃₀ ∅ ∧ ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → (s ∩ U).Nonempty} ⊆ ⋂₀ t
Tactic: exists ∅
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ :
  t ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
s : Set α
hs : s ∈ ⋂₀ t
h : s.Nonempty
⊢ ∃ (u : Set (Set (Set α))) (v : Set (Set (Set α))),
    u ⊆ powerset '' {U : Set α | IsOpen[inst] U} ∧
      v ⊆ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U} ∧ u ∪ v = t
have rw : ∀
  (ht₂ :
    t ∩ powerset '' {U : Set α | IsOpen[inst] U} ∪
        t ∩ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V} =
      t)
  (s : Set α) (hs : s ∈ ⋂₀ t),
  s.Nonempty →
    ∃ (u : Set (Set (Set α))) (v : Set (Set (Set α))),
      u ⊆ powerset '' {U : Set α | IsOpen[inst] U} ∧
        v ⊆ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U} ∧ u ∪ v = t
Tactic: rw [← inter_eq_left, inter_union_distrib_left] at ht₂
Cleared hypotheses: ht₂, s, hs, h
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set (Set (Set α))
ht₁ : t.Finite
ht₂ :
  t ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
s : Set α
hs : s ∈ ⋂₀ t
h : s.Nonempty
⊢ ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} s ∧
        {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ t
have refine_2 : ∀ (u v : Set (Set (Set α))) (hu : u ⊆ powerset '' {U : Set α | IsOpen[inst] U})
  (hv : v ⊆ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}) (ht₁ : (u ∪ v).Finite)
  (ht₂ :
    u ∪ v ⊆
      powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
  (hs : s ∈ ⋂₀ (u ∪ v)),
  ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} s ∧
        {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ (u ∪ v)
Tactic: obtain ⟨u, v, hu, hv, rfl⟩ : ∃ u v, u ⊆ powerset '' {U | IsOpen U} ∧
        v ⊆ (fun V => {s | (s ∩ V).Nonempty}) '' {U | IsOpen U} ∧ u ∪ v = t := by
      rw [← inter_eq_left, inter_union_distrib_left] at ht₂
      exact ⟨_, _, inter_subset_right, inter_subset_right, ht₂⟩
Cleared hypotheses: t, ht₁, ht₂, hs