awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
⊢ ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' F}

Tactic:
exact fun U hU => (hU.preimage hf).powerset_vietoris
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
eq_induced : TopologicalSpace.vietoris α = induced (fun (x : Set α) ↦ f '' x) (TopologicalSpace.vietoris β)
⊢ IsInducing.{u_1, u_2} (Y := Set β) fun (x : Set α) ↦ f '' x

Tactic:
constructor
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
⊢ Eq.{u_1 + 1} (α := Set (Set α)) {U : Set α | IsOpen[inst] U}
    ((fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V})

Tactic:
have : {U : Set α | IsOpen U} = (f ⁻¹' ·) '' {V : Set β | IsOpen V} :=
    Set.ext fun _ => hf.isOpen_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
⊢ IsCompact.{u_1} (X := Set α) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}

Tactic:
isCompact_generateFrom rfl fun S hS hKS => ?_

Premises used: isCompact_generateFrom, rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
refine :
  ∀ (S : Set (Set (Set α)))
    (hS :
      S ⊆
        powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
    (hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S),
    ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ IsCompact.{u_1} (X := Set α) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}

Tactic:
refine isCompact_generateFrom rfl fun S hS hKS => ?_

Premises used: isCompact_generateFrom, rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
pos : ∀ (hsu : ∃ L ∈ s, L ⊆ ⋃₀ u), ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
neg :
  ∀ (hsu : ∀ (L : Set α) (_ : L ∈ s), ¬L ⊆ ⋃₀ u),
    ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
by_cases! hsu : ∃ L ∈ s, L ⊆ ⋃₀ u
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∃ L ∈ s, L ⊆ ⋃₀ u
pos :
  ∀ (L : Set α) (hL : L ∈ s) (hLu : L ⊆ ⋃₀ u),
    ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
obtain ⟨L, hL, hLu⟩ := hsu
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃₀ u
⊢ L ⊆ ⋃ i ∈ u, i

Tactic:
rw [sUnion_eq_biUnion] at hLu

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
pos :
  ∀ (T : Set (Set α)) (hTS : T ⊆ u) (hT : T.Finite) (hLT : L ⊆ ⋃ i ∈ T, i),
    ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
obtain ⟨T, hTS, hT, hLT⟩ := (hs L hL).elim_finite_subcover_image (fun _ h => h.1) hLu

Premises used: IsCompact.elim_finite_subcover_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ (fun (U : Set α) ↦ {s : Set α | (s ∩ U).Nonempty}) '' T ⊆ S

Tactic:
grind [image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
pos :
  Subset (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
    (⋃₀ ((fun (U : Set α) ↦ {s : Set α | (s ∩ U).Nonempty}) '' T))
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
refine ⟨(fun U => {s | (s ∩ U).Nonempty}) '' T, by grind [image_subset_iff], hT.image _, ?_⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
pos :
  Subset.{u_1} (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
    {x : Set α | (x ∩ ⋃ i ∈ T, i).Nonempty}
⊢ Subset (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
    (⋃₀ ((fun (U : Set α) ↦ {s : Set α | (s ∩ U).Nonempty}) '' T))

Tactic:
simp_rw [sUnion_image, ← setOf_exists, ← nonempty_iUnion, ← inter_iUnion]

Premises used: Set.nonempty_iUnion, Set.setOf_exists, Set.sUnion_image, Set.inter_iUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
pos : Subset.{u_1} (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} {x : Set α | (x ∩ L).Nonempty}
⊢ Subset.{u_1} (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
    {x : Set α | (x ∩ ⋃ i ∈ T, i).Nonempty}

Tactic:
grw [← hLT]
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ Subset.{u_1} (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} {x : Set α | (x ∩ L).Nonempty}

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (_ : L ∈ s), ¬L ⊆ ⋃₀ u
⊢ ∀ (L : Set α) (_ : L ∈ s), (L \ ⋃₀ u).Nonempty

Tactic:
simp_rw [← diff_nonempty] at hsu

Premises used: Set.diff_nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (_ : L ∈ s), (L \ ⋃₀ u).Nonempty
L : Set α
h : L ∈ s
⊢ L \ ⋃₀ u ⊆ K \ ⋃₀ u ∩ L

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (_ : L ∈ s), (L \ ⋃₀ u).Nonempty
⊢ ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty

Tactic:
replace hsu L (h : L ∈ s) : (K \ ⋃₀ u ∩ L).Nonempty := (hsu L h).mono <| by grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
neg :
  ∀ (w : Set (Set α)) (hUS : w ∈ S) (hUu : K \ ⋃₀ u ∈ w),
    ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
obtain ⟨_, hUS, hUu⟩ := mem_sUnion.mp <| hKS ⟨diff_subset, hsu⟩

Premises used: Set.diff_subset, And.intro, Iff.mp, Set.mem_sUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
w : Set (Set α)
hUS : w ∈ S
hUu : K \ ⋃₀ u ∈ w
neg :
  ∀ (U : Set α) (hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U) (hUS : 𝒫 U ∈ S)
    (hUu : K \ ⋃₀ u ∈ 𝒫 U), ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
neg₁ :
  ∀ (U : Set α) (hU : Membership.mem (γ := Set (Set α)) {V : Set α | IsOpen[inst] V} U)
    (hUS : (fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U ∈ S)
    (hUu :
      Membership.mem (γ := Set (Set α)) ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U)
        (K \ ⋃₀ u)),
    ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
rcases hS hUS with ⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ ⋃₀ u ∈ 𝒫 U
⊢ K \ U ⊆ ⋃ i ∈ u, i

Tactic:
rw [mem_powerset_iff, diff_subset_comm, sUnion_eq_biUnion] at hUu

Premises used: Set.mem_powerset_iff, Set.diff_subset_comm, Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
neg :
  ∀ (T : Set (Set α)) (hTS : T ⊆ u) (hT : T.Finite) (hKT : K \ U ⊆ ⋃ i ∈ T, i),
    ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
obtain ⟨T, hTS, hT, hKT⟩ := (hK.diff hU).elim_finite_subcover_image (fun _ h => h.1) hUu

Premises used: IsCompact.elim_finite_subcover_image, IsCompact.diff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
⟨insert U.powerset ((fun V => {s | (s ∩ V).Nonempty}) '' T),
        insert_subset hUS <| Set.image_subset_iff.mpr <| hTS.trans fun _ h => h.2,
        (hT.image _).insert _, ?_⟩

Premises used: Iff.mpr, setOf, Set.powerset, HasSubset.Subset.trans, Insert.insert, Set.Finite.image, Inter.inter, Set.Nonempty, And.right, And.intro, Exists.intro, Set.image, Set.image_subset_iff, Set.Finite.insert, Set.insert_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
neg :
  Subset (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
    (⋃₀ insert (𝒫 U) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' T))
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
refine ⟨insert U.powerset ((fun V => {s | (s ∩ V).Nonempty}) '' T),
        insert_subset hUS <| Set.image_subset_iff.mpr <| hTS.trans fun _ h => h.2,
        (hT.image _).insert _, ?_⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
neg : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} \ 𝒫 U ⊆ ⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}
⊢ Subset (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
    (⋃₀ insert (𝒫 U) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' T))

Tactic:
rw [sUnion_insert, ← diff_subset_iff, sUnion_image]

Premises used: Set.diff_subset_iff, Set.sUnion_insert, Set.sUnion_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htU : t ∉ 𝒫 U
htK : t ⊆ K
⊢ ∃ a ∈ t, a ∉ U

Tactic:
rw [mem_powerset_iff, not_subset] at htU

Premises used: Set.mem_powerset_iff, Set.not_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htU : t ∉ 𝒫 U
htK : t ⊆ K
htU₁ : ∃ a ∈ t, a ∉ U
⊢ t ⊆ K

Tactic:
rw [mem_powerset_iff, not_subset] at htU

Premises used: Set.mem_powerset_iff, Set.not_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htU : ∃ a ∈ t, a ∉ U
htK : t ⊆ K
neg :
  ∀ (x : α) (hxt : x ∈ t) (hxU : x ∉ U), Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t
⊢ Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t

Tactic:
obtain ⟨x, hxt, hxU⟩ := htU
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htK : t ⊆ K
x : α
hxt : x ∈ t
hxU : x ∉ U
neg :
  ∀ (V : Set α) (hVT : V ∈ T) (hxV : x ∈ V),
    Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t
⊢ Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t

Tactic:
obtain ⟨V, hVT, hxV⟩ := mem_iUnion₂.mp <| hKT ⟨htK hxt, hxU⟩

Premises used: Set.mem_iUnion₂, And.intro, Iff.mp
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htK : t ⊆ K
x : α
hxt : x ∈ t
hxU : x ∉ U
V : Set α
hVT : V ∈ T
hxV : x ∈ V
⊢ Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t

Tactic:
mem_biUnion hVT ⟨x, hxt, hxV⟩

Premises used: Set.mem_biUnion, And.intro, Exists.intro