Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
s : Set α
x✝ : s ∈ {t | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty}
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst✝³] s, isCompact' := ⋯ }
⊢ ∃ y ∈ SetLike.coe '' {K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty}, s ⤳ y

Tactic:
refine ⟨s', mem_image_of_mem _ ⟨inter_subset_left, fun U hU => (hsu hU).mono ?_⟩,
      vietoris.specializes_of_subset_closure ?_ ?_⟩

Goal state after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
s : Set α
x✝ : s ∈ {t | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty}
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst✝³] s, isCompact' := ⋯ }
U : Set α
hU : U ∈ u
⊢ s ∩ M U ⊆ ↑s' ∩ M U

case refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
s : Set α
x✝ : s ∈ {t | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty}
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst✝³] s, isCompact' := ⋯ }
⊢ s ⊆ ↑s'

case refine_2.refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
s : Set α
x✝ : s ∈ {t | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty}
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst✝³] s, isCompact' := ⋯ }
⊢ ↑s' ⊆ closure[inst✝³] s