awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s.Nonempty
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)
have ht₃ : u.Finite ∧ v.Finite
Tactic: rw [finite_union] at ht₁
Cleared hypotheses: ht₁, ht₂, hs
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s.Nonempty
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.Finite ∧ 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)
have refine_2 : ∀ (u : Set (Set α)) (hu₁ : u ⊆ {U : Set α | IsOpen[inst] U}) (hu₂ : u.Finite)
  (hu : powerset '' u ⊆ powerset '' {U : Set α | IsOpen[inst] U}) (ht₁ : (powerset '' u).Finite ∧ v.Finite)
  (ht₂ :
    powerset '' u ∪ v ⊆
      powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
  (hs : s ∈ ⋂₀ (powerset '' 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} ⊆ ⋂₀ (powerset '' u ∪ v)
Tactic: obtain ⟨u, hu₁, hu₂, rfl⟩ := exists_subset_image_finite_and.mp ⟨u, hu, ht₁.1, rfl⟩
Cleared hypotheses: u, hu, ht₁, ht₂, hs
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s.Nonempty
v : Set (Set (Set α))
hv : v ⊆ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}
u : Set (Set α)
hu₁ : u ⊆ {U : Set α | IsOpen[inst] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U : Set α | IsOpen[inst] U}
ht₁ : (powerset '' u).Finite ∧ v.Finite
ht₂ :
  powerset '' u ∪ v ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hs : s ∈ ⋂₀ (powerset '' 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} ⊆ ⋂₀ (powerset '' u ∪ v)
have refine_2 : ∀ (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})
  (hs : s ∈ ⋂₀ (powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' 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} ⊆
          ⋂₀ (powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
Tactic: obtain ⟨v, hv₁, hv₂, rfl⟩ := exists_subset_image_finite_and.mp ⟨v, hv, ht₁.2, rfl⟩
Cleared hypotheses: v, hv, ht₁, ht₂, hs
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
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}
hs : s ∈ ⋂₀ (powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
U : Set α := ⋂₀ u
⊢ ∃ (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} ⊆
          ⋂₀ (powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
have hU : IsOpen[inst] U
Tactic: have hU : IsOpen U := hu₂.isOpen_sInter hu₁
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
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 ∈ ⋂₀ (powerset '' u) ∩ ⋂₀ ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
⊢ ⋂₀ (powerset '' u) = 𝒫 U
have h : ∀ (x : Set α), x ∈ ⋂₀ (powerset '' u) ↔ x ∈ 𝒫 U
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
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}
hs : s ∈ ⋂₀ (powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
U : Set α := ⋂₀ u
hU : IsOpen[inst] U
⊢ ∃ (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} ⊆
          ⋂₀ (powerset '' u ∪ (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' v)
have refine_2 : ∀ (hs : s ∈ 𝒫 U ∩ ⋂ a ∈ v, {s : Set α | (s ∩ a).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} ⊆ 𝒫 U ∩ ⋂ a ∈ v, {s : Set α | (s ∩ a).Nonempty}
Tactic: simp_rw [sInter_union, show ⋂₀ (powerset '' u) = U.powerset by ext; simp [U], sInter_image]
      at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
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 ∩ ⋂ a ∈ v, {s : Set α | (s ∩ a).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} ⊆ 𝒫 U ∩ ⋂ a ∈ v, {s : Set α | (s ∩ a).Nonempty}
have hs₁ : s ⊆ U ∧ ∀ (i : Set α) (j : i ∈ v), Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ i).Nonempty} s
Tactic: rw [mem_inter_iff, mem_powerset_iff, mem_iInter₂] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
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
⊢ ∃ (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 ∩ ⋂ a ∈ v, {s : Set α | (s ∩ a).Nonempty}
have refine_2 : 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: exists insert U ((U ∩ ·) '' v)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
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
⊢ 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}
have 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}
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]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
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
⊢ (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}
have 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
Tactic: refine ⟨⟨hv₂.image _, hU, fun V hV => hU.inter (hv₁ hV)⟩, by grind,
      fun t ⟨htU, _, ht⟩ => ⟨htU, mem_iInter₂_of_mem ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
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})
have 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
Tactic: refine isTopologicalBasis.isTopologicalBasis_of_exists_subset ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
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
⊢ 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})
have 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
Tactic: refine isTopologicalBasis.isTopologicalBasis_of_exists_subset ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ (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
have 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}
Tactic: rw [forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ (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
have 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}
Tactic: rw [forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : 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} (V, u) →
    IsOpen[TopologicalSpace.vietoris α] {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}
have 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}
Tactic: ⟨hV, hu, huB, _⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
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 α] {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}
have refine_1 : IsOpen[TopologicalSpace.vietoris α] ({a : Set α | a ⊆ V} ∩ ⋂ 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 α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
⊢ 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}
have 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}
Tactic: ⟨hu₁, hu₂⟩