awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U : Set α | IsOpen[inst] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U : Set α | IsOpen[inst] U}
v : Set (Set α)
hv₁ : v ⊆ {U : Set α | IsOpen[inst] U}
hv₂ : v.Finite
hv :
  Subset (α := Set (Set (Set α))) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
    ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U})
ht₁ : (powerset '' u).Finite ∧ Set.Finite (α := Set (Set α)) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
ht₂ :
  powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst] U
hs : s ⊆ U ∧ ∀ (i : Set α) (j : i ∈ v), Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ i).Nonempty} s
refine_2 :
  (Set.Finite (α := Set α) ((fun (x : Set α) ↦ U ∩ x) '' v) ∧
      IsOpen[inst] U ∧ ∀ ⦃x : Set α⦄, x ∈ v → IsOpen[inst] (U ∩ x)) ∧
    (s ⊆ U ∧ s.Nonempty ∧ ∀ ⦃x : Set α⦄, x ∈ v → (s ∩ x).Nonempty) ∧
      {s : Set α | s ⊆ U ∧ (s ∩ U).Nonempty ∧ ∀ ⦃x : Set α⦄, x ∈ v → (s ∩ U ∩ x).Nonempty} ⊆
        𝒫 U ∩ ⋂ a ∈ v, {s : Set α | (s ∩ a).Nonempty}
⊢ Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U}
      (insert U ((fun (x : Set α) ↦ U ∩ x) '' v)) ∧
    Membership.mem (γ := Set (Set α))
        {s : Set α |
          s ⊆ ⋃₀ insert U ((fun (x : Set α) ↦ U ∩ x) '' v) ∧
            ∀ (U_1 : Set α),
              Membership.mem (γ := Set (Set α)) (insert U ((fun (x : Set α) ↦ U ∩ x) '' v)) U_1 → (s ∩ U_1).Nonempty}
        s ∧
      {s : Set α |
          s ⊆ ⋃₀ insert U ((fun (x : Set α) ↦ U ∩ x) '' v) ∧
            ∀ (U_1 : Set α),
              Membership.mem (γ := Set (Set α)) (insert U ((fun (x : Set α) ↦ U ∩ x) '' v)) U_1 → (s ∩ U_1).Nonempty} ⊆
        𝒫 U ∩ ⋂ a ∈ v, {s : Set α | (s ∩ a).Nonempty}

Tactic:
simp_rw [show ⋃₀ (insert U ((U ∩ ·) '' v)) = U by simp, mem_setOf, finite_insert,
      forall_mem_insert, forall_mem_image, ← inter_assoc, inter_eq_left.mpr hs.1]

Premises used: Set.inter_eq_left, Iff.mpr, Set.forall_mem_insert, Set.finite_insert, Set.mem_setOf, And.left, Set.inter_assoc, Set.forall_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U : Set α | IsOpen[inst] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U : Set α | IsOpen[inst] U}
v : Set (Set α)
hv₁ : v ⊆ {U : Set α | IsOpen[inst] U}
hv₂ : v.Finite
hv :
  Subset (α := Set (Set (Set α))) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
    ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U})
ht₁ : (powerset '' u).Finite ∧ Set.Finite (α := Set (Set α)) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
ht₂ :
  powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst] U
hs : s ⊆ U ∧ ∀ (i : Set α) (j : i ∈ v), Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ i).Nonempty} s
⊢ s ⊆ U ∧ s.Nonempty ∧ ∀ ⦃x : Set α⦄, x ∈ v → (s ∩ x).Nonempty

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U : Set α | IsOpen[inst] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U : Set α | IsOpen[inst] U}
v : Set (Set α)
hv₁ : v ⊆ {U : Set α | IsOpen[inst] U}
hv₂ : v.Finite
hv :
  Subset (α := Set (Set (Set α))) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
    ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U})
ht₁ : (powerset '' u).Finite ∧ Set.Finite (α := Set (Set α)) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
ht₂ :
  powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst] U
hs : s ⊆ U ∧ ∀ (i : Set α) (j : i ∈ v), Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ i).Nonempty} s
refine_2 :
  ∀ (t : Set α),
    Membership.mem (γ := Set (Set α))
        {s : Set α | s ⊆ U ∧ (s ∩ U).Nonempty ∧ ∀ ⦃x : Set α⦄, x ∈ v → (s ∩ U ∩ x).Nonempty} t →
      ∀ (htU : t ⊆ U),
        (t ∩ U).Nonempty →
          ∀ (ht : ∀ ⦃x : Set α⦄, x ∈ v → (t ∩ U ∩ x).Nonempty) (i : Set α) (j : i ∈ v),
            Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ i).Nonempty} t
⊢ (Set.Finite (α := Set α) ((fun (x : Set α) ↦ U ∩ x) '' v) ∧
      IsOpen[inst] U ∧ ∀ ⦃x : Set α⦄, x ∈ v → IsOpen[inst] (U ∩ x)) ∧
    (s ⊆ U ∧ s.Nonempty ∧ ∀ ⦃x : Set α⦄, x ∈ v → (s ∩ x).Nonempty) ∧
      {s : Set α | s ⊆ U ∧ (s ∩ U).Nonempty ∧ ∀ ⦃x : Set α⦄, x ∈ v → (s ∩ U ∩ x).Nonempty} ⊆
        𝒫 U ∩ ⋂ a ∈ v, {s : Set α | (s ∩ a).Nonempty}

Tactic:
refine ⟨⟨hv₂.image _, hU, fun V hV => hU.inter (hv₁ hV)⟩, by grind,
      fun t ⟨htU, _, ht⟩ => ⟨htU, mem_iInter₂_of_mem ?_⟩⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U : Set α | IsOpen[inst] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U : Set α | IsOpen[inst] U}
v : Set (Set α)
hv₁ : v ⊆ {U : Set α | IsOpen[inst] U}
hv₂ : v.Finite
hv :
  Subset (α := Set (Set (Set α))) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
    ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U})
ht₁ : (powerset '' u).Finite ∧ Set.Finite (α := Set (Set α)) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
ht₂ :
  powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst] U
hs : s ⊆ U ∧ ∀ (i : Set α) (j : i ∈ v), Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ i).Nonempty} s
t : Set α
h_1 :
  Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ U ∧ (s ∩ U).Nonempty ∧ ∀ ⦃x : Set α⦄, x ∈ v → (s ∩ U ∩ x).Nonempty}
    t
htU : t ⊆ U
left : (t ∩ U).Nonempty
ht : ∀ ⦃x : Set α⦄, x ∈ v → (t ∩ U ∩ x).Nonempty
⊢ ∀ (i : Set α) (j : i ∈ v), Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ i).Nonempty} t

Tactic:
simpa only [inter_eq_left.mpr htU] using ht

Premises used: Set.inter_eq_left, Iff.mpr
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ IsTopologicalBasis.{u_1} (α := Set α)
    ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
      {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})

Tactic:
isTopologicalBasis.isTopologicalBasis_of_exists_subset ?_ ?_

Premises used: TopologicalSpace.vietoris.isTopologicalBasis, TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
refine_1 :
  ∀ (u : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
        u →
      IsOpen[TopologicalSpace.vietoris α] u
refine_2 :
  ∀ (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 →
      ∀ x ∈ u,
        ∃ (v : Set (Set α)),
          Membership.mem (γ := Set (Set (Set α)))
              ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
                {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
              v ∧
            x ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u_1} (α := Set α)
    ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
      {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})

Tactic:
refine isTopologicalBasis.isTopologicalBasis_of_exists_subset ?_ ?_

Premises used: TopologicalSpace.vietoris.isTopologicalBasis, TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
refine_1 :
  ∀ ⦃x : Set α × Set (Set α)⦄,
    Membership.mem (γ := Set (Set α × Set (Set α)))
        {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} x →
      IsOpen[TopologicalSpace.vietoris α] {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}
⊢ ∀ (u : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
        u →
      IsOpen[TopologicalSpace.vietoris α] u

Tactic:
rw [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
refine_2 :
  ∀ ⦃x : Set (Set α)⦄,
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x →
      ∀ (x_1 : Set α),
        Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} x_1 →
          ∃ (v : Set (Set α)),
            Membership.mem (γ := Set (Set (Set α)))
                ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
                  {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
                v ∧
              x_1 ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}
⊢ ∀ (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 →
      ∀ x ∈ u,
        ∃ (v : Set (Set α)),
          Membership.mem (γ := Set (Set (Set α)))
              ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
                {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
              v ∧
            x ∈ v ∧ v ⊆ u

Tactic:
rw [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
refine_1 :
  ∀ (hV : IsOpen[inst] (V, u).1) (hu : (V, u).2.Finite) (huB : (V, u).2 ⊆ B),
    (∀ U ∈ (V, u).2, U ⊆ (V, u).1) →
      IsOpen[TopologicalSpace.vietoris α] {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}
⊢ Membership.mem (γ := Set (Set α × Set (Set α)))
      {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} (V, u) →
    IsOpen[TopologicalSpace.vietoris α] {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}

Tactic:
⟨hV, hu, huB, _⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] (V, u).1
hu : (V, u).2.Finite
huB : (V, u).2 ⊆ B
right : ∀ U ∈ (V, u).2, U ⊆ (V, u).1
refine_1 : IsOpen[TopologicalSpace.vietoris α] ({a : Set α | a ⊆ V} ∩ ⋂ i ∈ u, {x : Set α | (x ∩ i).Nonempty})
⊢ IsOpen[TopologicalSpace.vietoris α] {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}

Tactic:
simp_rw [setOf_and, setOf_forall]

Premises used: Set.setOf_and, Set.setOf_forall
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] (V, u).1
hu : (V, u).2.Finite
huB : (V, u).2 ⊆ B
right : ∀ U ∈ (V, u).2, U ⊆ (V, u).1
⊢ IsOpen[TopologicalSpace.vietoris α] ({a : Set α | a ⊆ V} ∩ ⋂ i ∈ u, {x : Set α | (x ∩ i).Nonempty})

Tactic:
hV.powerset_vietoris.inter <|
      hu.isOpen_biInter fun V hV => isOpen_inter_nonempty_of_isOpen <| hB.isOpen <| huB hV

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, setOf, Set.powerset, TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen, IsOpen.powerset_vietoris, IsOpen.inter, Set.Finite.isOpen_biInter
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] (V, u).1
hu : (V, u).2.Finite
huB : (V, u).2 ⊆ B
right : ∀ U ∈ (V, u).2, U ⊆ (V, u).1
⊢ IsOpen[TopologicalSpace.vietoris α] ({a : Set α | a ⊆ V} ∩ ⋂ i ∈ u, {x : Set α | (x ∩ i).Nonempty})

Tactic:
exact hV.powerset_vietoris.inter <|
      hu.isOpen_biInter fun V hV => isOpen_inter_nonempty_of_isOpen <| hB.isOpen <| huB hV

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen, IsOpen.powerset_vietoris, IsOpen.inter, Set.Finite.isOpen_biInter
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
refine_2 :
  ∀ (hu₁ : u.Finite) (hu₂ : ∀ U ∈ u, IsOpen[inst] U) (x : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty} x →
      ∃ (v : Set (Set α)),
        Membership.mem (γ := Set (Set (Set α)))
            ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
              {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
            v ∧
          x ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
⊢ Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} u →
    ∀ (x : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty} x →
        ∃ (v : Set (Set α)),
          Membership.mem (γ := Set (Set (Set α)))
              ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
                {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
              v ∧
            x ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
⟨hu₁, hu₂⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
refine_2 :
  ∀ (hs₁ : s ⊆ ⋃₀ u) (hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty),
    ∃ (v : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α)))
          ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
            {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
          v ∧
        s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty} s →
    ∃ (v : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α)))
          ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
            {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
          v ∧
        s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
⟨hs₁, hs₂⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
U : Set α
hU : U ∈ u
obtain : ∀ (x : α) (hxs : x ∈ s) (hxU : x ∈ U), ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty

Tactic:
obtain ⟨x, hxs, hxU⟩ := hs₂ U hU
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
U : Set α
hU : U ∈ u
x : α
hxs : x ∈ s
hxU : x ∈ U
obtain : ∀ (W : Set α) (hWB : W ∈ B) (hxW : x ∈ W) (hW : W ⊆ U), ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty

Tactic:
obtain ⟨W, hWB, hxW, hW⟩ := hB.exists_subset_of_mem_open hxU <| hu₂ U hU

Premises used: TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
U : Set α
hU : U ∈ u
x : α
hxs : x ∈ s
hxU : x ∈ U
W : Set α
hWB : W ∈ B
hxW : x ∈ W
hW : W ⊆ U
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty

Tactic:
⟨W, hWB, hW, x, hxs, hxW⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
U : Set α
hU : U ∈ u
x : α
hxs : x ∈ s
hxU : x ∈ U
W : Set α
hWB : W ∈ B
hxW : x ∈ W
hW : W ⊆ U
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty

Tactic:
exact ⟨W, hWB, hW, x, hxs, hxW⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
refine_2 :
  ∀ (f : (U : Set α) → Set α) (hfB : ∀ U ∈ u, f U ∈ B) (hfU : ∀ U ∈ u, f U ⊆ U) (hfs : ∀ U ∈ u, (s ∩ f U).Nonempty),
    ∃ (v : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α)))
          ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
            {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
          v ∧
        s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
⊢ ∃ (v : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
        v ∧
      s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
choose! f hfB hfU hfs using show ∀ U ∈ u, ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty by
      intro U hU
      obtain ⟨x, hxs, hxU⟩ := hs₂ U hU
      obtain ⟨W, hWB, hxW, hW⟩ := hB.exists_subset_of_mem_open hxU <| hu₂ U hU
      exact ⟨W, hWB, hW, x, hxs, hxW⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
refine_2 :
  ∃ (x : Set α × Set (Set α)),
    Membership.mem (γ := Set (Set α × Set (Set α)))
        {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} s ∧
        Subset.{u_1} (α := Set (Set α)) {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}
          {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
⊢ ∃ (v : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
        v ∧
      s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
rw [exists_mem_image]

Premises used: Set.exists_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
⊢ (⋃₀ u, f '' u).2 ⊆ B ∧ ∀ U ∈ (⋃₀ u, f '' u).2, U ⊆ (⋃₀ u, f '' u).1

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty} s

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
refine_2 :
  ∀ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty} t →
      ∀ (ht₁ : t ⊆ (⋃₀ u, f '' u).1) (ht₂ : ∀ U ∈ (⋃₀ u, f '' u).2, (t ∩ U).Nonempty) (U : Set α) (hU : U ∈ u),
        (t ∩ U).Nonempty
⊢ ∃ (x : Set α × Set (Set α)),
    Membership.mem (γ := Set (Set α × Set (Set α)))
        {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} s ∧
        Subset.{u_1} (α := Set (Set α)) {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}
          {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
refine ⟨⟨⋃₀ u, f '' u⟩, ⟨isOpen_sUnion hu₂, hu₁.image _, by grind⟩, by grind,
      fun t ⟨ht₁, ht₂⟩ => ⟨ht₁, fun U hU => ?_⟩⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
h : Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty} t
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ U ∈ (⋃₀ u, f '' u).2, (t ∩ U).Nonempty
U : Set α
hU : U ∈ u
refine_2 : ∀ (ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty) (U : Set α) (hU : U ∈ u), (t ∩ U).Nonempty
⊢ (t ∩ U).Nonempty

Tactic:
rw [forall_mem_image] at ht₂

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
h : Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty} t
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
refine_2 : (t ∩ f U).Nonempty
⊢ (t ∩ U).Nonempty

Tactic:
grw [← hfU U hU]