Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: 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

pp: 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'

pp: 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

Tactic:
<;>

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