awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
refine :
  ∀ (s : Set α) (hs : s ∈ 𝒫 K), ∃ y ∈ image (α := Compacts α) SetLike.coe {L : Compacts α | (↑L : Set α) ⊆ K}, s ⤳ y
⊢ IsCompact (image (α := Compacts α) SetLike.coe {L : Compacts α | (↑L : Set α) ⊆ K})

Tactic:
refine .of_subset_of_specializes hK.powerset_vietoris (by grind) (fun s hs => ?_)
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set α
hs : s ∈ 𝒫 K
L : Compacts α := { carrier := K ∩ closure[inst] s, isCompact' := ⋯ }
⊢ ∃ y ∈ image (α := Compacts α) SetLike.coe {L : Compacts α | (↑L : Set α) ⊆ K}, s ⤳ y

Tactic:
⟨L, mem_image_of_mem _ inter_subset_left,
    vietoris.specializes_of_subset_closure (subset_inter hs subset_closure) inter_subset_right⟩

Premises used: TopologicalSpace.vietoris.specializes_of_subset_closure, subset_closure, Set.inter_subset_left, Set.subset_inter, SetLike.coe, Set.mem_image_of_mem, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set α
hs : s ∈ 𝒫 K
L : Compacts α := { carrier := K ∩ closure[inst] s, isCompact' := ⋯ }
⊢ ∃ y ∈ image (α := Compacts α) SetLike.coe {L : Compacts α | (↑L : Set α) ⊆ K}, s ⤳ y

Tactic:
exact ⟨L, mem_image_of_mem _ inter_subset_left,
    vietoris.specializes_of_subset_closure (subset_inter hs subset_closure) inter_subset_right⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : CompactSpace α
⊢ IsCompact.{u_1} (X := Compacts α) univ

Tactic:
simpa using isCompact_subsets_of_isCompact isCompact_univ

Premises used: isCompact_univ, TopologicalSpace.Compacts.isCompact_subsets_of_isCompact
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
rw :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) →
      Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ (i : ι), U i) →
        ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)
⊢ IsCompact.{u_1} (X := α) (⋃ K ∈ S, (↑K : Set α))

Tactic:
rw [isCompact_iff_finite_subcover]

Premises used: isCompact_iff_finite_subcover
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ (i : ι), U i)
⊢ ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i

Tactic:
rw [iUnion₂_subset_iff] at h

Premises used: Set.iUnion₂_subset_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i
obtain :
  ∀ (s : Finset (Finset ι)) (hs : S ⊆ ⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}),
    ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)
⊢ ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)

Tactic:
obtain ⟨s, hs⟩ := hS.elim_finite_subcover
    (fun s : Finset ι => {K | (K : Set α) ⊆ ⋃ i ∈ s, U i})
    (fun s => isOpen_subsets_of_isOpen <| isOpen_biUnion fun _ _ => hU _)
    (fun K hK => mem_iUnion.mpr <| K.isCompact.elim_finite_subcover U hU <| h K hK)

Premises used: Iff.mpr, setOf, Set.mem_iUnion, HasSubset.Subset, IsCompact.elim_finite_subcover, SetLike.coe, TopologicalSpace.Compacts.isCompact, TopologicalSpace.Compacts.isOpen_subsets_of_isOpen, isOpen_biUnion, Set.iUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}
⊢ ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)

Tactic:
⟨s.biUnion id, (biUnion_subset_biUnion_left hs).trans ?_⟩

Premises used: HasSubset.Subset.trans, id, Finset.biUnion, Exists.intro, Set.biUnion_subset_biUnion_left
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}
refine :
  Subset.{u_1} (α := Set α)
    (⋃ (x : Compacts α),
      ⋃ (_ : Membership.mem (γ := Set (Compacts α)) (⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}) x),
        (↑x : Set α))
    (⋃ i ∈ s.biUnion id, U i)
⊢ ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)

Tactic:
refine ⟨s.biUnion id, (biUnion_subset_biUnion_left hs).trans ?_⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}
simp_rw :
  ∀ (i : Finset ι) (i_1 : i ∈ s) (i_2 : Compacts α)
    (i : Membership.mem (γ := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_3 ∈ i, U i_3} i_2),
    (↑i_2 : Set α) ⊆ ⋃ x ∈ s, ⋃ y ∈ id x, U y
⊢ Subset.{u_1} (α := Set α)
    (⋃ (x : Compacts α),
      ⋃ (_ : Membership.mem (γ := Set (Compacts α)) (⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}) x),
        (↑x : Set α))
    (⋃ i ∈ s.biUnion id, U i)

Tactic:
simp_rw [biUnion_iUnion, iUnion_subset_iff, Finset.set_biUnion_biUnion]

Premises used: Finset.set_biUnion_biUnion, Set.iUnion_subset_iff, Set.biUnion_iUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}
⊢ ∀ (i : Finset ι) (i_1 : i ∈ s) (i_2 : Compacts α)
    (i : Membership.mem (γ := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_3 ∈ i, U i_3} i_2),
    (↑i_2 : Set α) ⊆ ⋃ x ∈ s, ⋃ y ∈ id x, U y

Tactic:
fun t ht K hK => subset_iUnion₂_of_subset t ht hK

Premises used: Set.subset_iUnion₂_of_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}
⊢ ∀ (i : Finset ι) (i_1 : i ∈ s) (i_2 : Compacts α)
    (i : Membership.mem (γ := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_3 ∈ i, U i_3} i_2),
    (↑i_2 : Set α) ⊆ ⋃ x ∈ s, ⋃ y ∈ id x, U y

Tactic:
exact fun t ht K hK => subset_iUnion₂_of_subset t ht hK

Premises used: Set.subset_iUnion₂_of_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}
refine :
  Subset.{u_1} (α := Set α)
    (⋃ (x : Compacts α),
      ⋃ (_ : Membership.mem (γ := Set (Compacts α)) (⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}) x),
        (↑x : Set α))
    (⋃ i ∈ s.biUnion id, U i)
refine₁ :
  ∀ (i : Finset ι) (i_1 : i ∈ s) (i_2 : Compacts α)
    (i : Membership.mem (γ := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_3 ∈ i, U i_3} i_2),
    (↑i_2 : Set α) ⊆ ⋃ x ∈ s, ⋃ y ∈ id x, U y
⊢ ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)

Tactic:
classical
  refine ⟨s.biUnion id, (biUnion_subset_biUnion_left hs).trans ?_⟩
  simp_rw [biUnion_iUnion, iUnion_subset_iff, Finset.set_biUnion_biUnion]
  exact fun t ht K hK => subset_iUnion₂_of_subset t ht hK

Premises used: Finset.set_biUnion_biUnion, Set.iUnion_subset_iff, Set.biUnion_iUnion, Set.subset_iUnion₂_of_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ CompactSpace.{u_1} (Compacts α) ↔ CompactSpace α

Tactic:
⟨fun h => ⟨?_⟩, fun _ => inferInstance⟩

Premises used: inferInstance, CompactSpace.mk, Iff.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
refine : ∀ (h : CompactSpace.{u_1} (Compacts α)), IsCompact.{u_1} (X := α) univ
⊢ CompactSpace.{u_1} (Compacts α) ↔ CompactSpace α

Tactic:
refine ⟨fun h => ⟨?_⟩, fun _ => inferInstance⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (Compacts α)
⊢ IsCompact.{u_1} (X := α) (⋃ (K : Compacts α), ⋃ (_ : Membership.mem (γ := Set (Compacts α)) univ K), (↑K : Set α))

Tactic:
isCompact_biUnion_coe_of_isCompact (α := α) isCompact_univ

Premises used: isCompact_univ, TopologicalSpace.Compacts.isCompact_biUnion_coe_of_isCompact
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (Compacts α)
h₁ :
  Eq.{u_1 + 1} (α := Set α) univ
    (⋃ (K : Compacts α), ⋃ (_ : Membership.mem (γ := Set (Compacts α)) univ K), (↑K : Set α))
⊢ IsCompact.{u_1} (X := α) univ

Tactic:
convert! isCompact_biUnion_coe_of_isCompact (α := α) isCompact_univ

Premises used: isCompact_univ, TopologicalSpace.Compacts.isCompact_biUnion_coe_of_isCompact
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (Compacts α)
h₁ :
  Eq.{u_1 + 1} (α := Set α) (⋃ (K : Compacts α), ⋃ (_ : Membership.mem (γ := Set (Compacts α)) univ K), (↑K : Set α))
    univ
⊢ Eq.{u_1 + 1} (α := Set α) univ
    (⋃ (K : Compacts α), ⋃ (_ : Membership.mem (γ := Set (Compacts α)) univ K), (↑K : Set α))

Tactic:
symm
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (Compacts α)
h₁ : ∀ (x : α), ∃ (i : Compacts α), x ∈ (↑i : Set α)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (K : Compacts α), ⋃ (_ : Membership.mem (γ := Set (Compacts α)) univ K), (↑K : Set α))
    univ

Tactic:
simp_rw [biUnion_univ, eq_univ_iff_forall, mem_iUnion]

Premises used: Set.eq_univ_iff_forall, Set.mem_iUnion, Set.biUnion_univ
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (Compacts α)
⊢ ∀ (x : α), ∃ (i : Compacts α), x ∈ (↑i : Set α)

Tactic:
fun x => ⟨{x}, Set.mem_singleton x⟩

Premises used: Set.mem_singleton, Exists.intro, Singleton.singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (Compacts α)
⊢ ∀ (x : α), ∃ (i : Compacts α), x ∈ (↑i : Set α)

Tactic:
exact fun x => ⟨{x}, Set.mem_singleton x⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw : ¬CompactSpace.{u_1} (Compacts α) ↔ ¬CompactSpace α
⊢ NoncompactSpace.{u_1} (Compacts α) ↔ NoncompactSpace α

Tactic:
simp_rw [← not_compactSpace_iff, compactSpace_iff]

Premises used: TopologicalSpace.Compacts.compactSpace_iff, not_compactSpace_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : NoncompactSpace α
⊢ NoncompactSpace.{u_1} (Compacts α)

Tactic:
noncompactSpace_iff.mpr ‹_›

Premises used: Iff.mpr, TopologicalSpace.Compacts.noncompactSpace_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
⊢ LocallyCompactSpace.{u_1} (Compacts α)

Tactic:
⟨fun K U hU => ?_⟩

Premises used: LocallyCompactSpace.mk
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
refine : ∀ (K : Compacts α) (U : Set (Compacts α)) (hU : U ∈ 𝓝 K), ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
⊢ LocallyCompactSpace.{u_1} (Compacts α)

Tactic:
refine ⟨fun K U hU => ?_⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU : U ∈ 𝓝 K
⊢ ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Compacts α))
          {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} K ∧
        {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} ⊆ U

Tactic:
rw [isTopologicalBasis.mem_nhds_iff, exists_mem_image] at hU

Premises used: TopologicalSpace.Compacts.isTopologicalBasis, Set.exists_mem_image, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU :
  ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Compacts α))
          {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} K ∧
        {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} ⊆ U
obtain :
  ∀ (u : Set (Set α)) (hu₁ : u.Finite) (hu₂ : ∀ U ∈ u, IsOpen[inst] U)
    (huU : {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ⊆ U)
    (hKu₁ : (↑K : Set α) ⊆ ⋃₀ u) (hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty), ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s

Tactic:
obtain ⟨u, ⟨hu₁, hu₂⟩, ⟨hKu₁, hKu₂⟩, huU⟩ := hU
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
huU : {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ⊆ U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
grw : ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s

Tactic:
grw [← huU]
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
obtain :
  ∀ (L : Set α) (hL : IsCompact L) (hLK : (↑K : Set α) ⊆ interior L) (hLu : L ⊆ ⋃₀ u),
    ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s

Tactic:
obtain ⟨L, hL, hLK, hLu⟩ := exists_compact_between K.isCompact (isOpen_sUnion hu₂) hKu₁

Premises used: exists_compact_between, TopologicalSpace.Compacts.isCompact, isOpen_sUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
obtain :
  ∀ (x : α) (hxK : x ∈ (↑K : Set α)) (hxU : x ∈ U),
    ∃ (M : Set α), IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ ((↑K : Set α) ∩ interior M).Nonempty
⊢ ∃ (M : Set α), IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ ((↑K : Set α) ∩ interior M).Nonempty

Tactic:
obtain ⟨x, hxK, hxU⟩ := hKu₂ U hU
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
x : α
hxK : x ∈ (↑K : Set α)
hxU : x ∈ U
obtain :
  ∀ (M : Set α) (hM : IsCompact M),
    x ∈ interior M ∧ M ⊆ U ∩ interior L →
      ∃ (M : Set α), IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ ((↑K : Set α) ∩ interior M).Nonempty
⊢ ∃ (M : Set α), IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ ((↑K : Set α) ∩ interior M).Nonempty

Tactic:
obtain ⟨M, hM, _⟩ := exists_compact_subset (U := U ∩ interior L)
        ((hu₂ U hU).inter isOpen_interior) ⟨hxU, hLK hxK⟩

Premises used: isOpen_interior, exists_compact_subset, And.intro, IsOpen.inter
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
x : α
hxK : x ∈ (↑K : Set α)
hxU : x ∈ U
M : Set α
hM : IsCompact M
right : x ∈ interior M ∧ M ⊆ U ∩ interior L
⊢ M ⊆ L

Tactic:
grind [interior_subset]

Premises used: interior_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
x : α
hxK : x ∈ (↑K : Set α)
hxU : x ∈ U
M : Set α
hM : IsCompact M
right : x ∈ interior M ∧ M ⊆ U ∩ interior L
⊢ M ⊆ U

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
x : α
hxK : x ∈ (↑K : Set α)
hxU : x ∈ U
M : Set α
hM : IsCompact M
right : x ∈ interior M ∧ M ⊆ U ∩ interior L
⊢ x ∈ (↑K : Set α) ∩ interior M

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
x : α
hxK : x ∈ (↑K : Set α)
hxU : x ∈ U
M : Set α
hM : IsCompact M
right : x ∈ interior M ∧ M ⊆ U ∩ interior L
⊢ ∃ (M : Set α), IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ ((↑K : Set α) ∩ interior M).Nonempty

Tactic:
exact ⟨M, hM, by grind [interior_subset], by grind, x, by grind⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
choose! :
  ∀ (M : (U : Set α) → Set α) (hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U))
    (hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L) (hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U)
    (hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty),
    ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s

Tactic:
choose! M hM hML hMU hMK using fun U (hU : U ∈ u) =>
    show ∃ M : Set α, IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ (↑K ∩ interior M).Nonempty by
      obtain ⟨x, hxK, hxU⟩ := hKu₂ U hU
      obtain ⟨M, hM, _⟩ := exists_compact_subset (U := U ∩ interior L)
        ((hu₂ U hU).inter isOpen_interior) ⟨hxU, hLK hxK⟩
      exact ⟨M, hM, by grind [interior_subset], by grind, x, by grind⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
a : ∀ (a : Compacts α), (↑a : Set α) ⊆ L → ∀ a ∈ u, M a ⊆ a
⊢ Subset.{u_1} (α := Set (Compacts α)) {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty}
    {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}

Tactic:
gcongr
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
a : Compacts α
h : (↑a : Set α) ⊆ L
a_1 : Set α
h_1 : a_1 ∈ u
⊢ M a_1 ⊆ a_1

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
refine_1 : {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty} ∈ 𝓝 K
refine_2 :
  IsCompact.{u_1} (X := Compacts α) {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty}
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s

Tactic:
refine ⟨{K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty}, ?_, by gcongr; grind, ?_⟩