Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : ⋃ a, s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst✝³] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst✝²] (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ x ∈ T y, U x y = ⊤
W : Y → Set Y := fun y ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst✝²] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst✝²] (E a)
hE : ⋃ i, E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
⊢ ∃ β t,
    (∀ (b : β), IsOpen[instTopologicalSpaceProd] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a

Tactic:
refine ⟨Σ y, T y, fun z ↦ U z.2.1 z.1 ×ˢ E z.1, fun _ ↦ (hUo _ _).prod (hEo _),
      iUnion_eq_univ_iff.2 fun (x, y) ↦ ?_, fun (x, y) ↦ ?_, fun ⟨y, x, hx⟩ ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : ⋃ a, s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst✝³] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst✝²] (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ x ∈ T y, U x y = ⊤
W : Y → Set Y := fun y ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst✝²] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst✝²] (E a)
hE : ⋃ i, E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y : Y
⊢ ∃ i, (x, y) ∈ U (↑i.snd) i.fst ×ˢ E i.fst

case refine_2
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : ⋃ a, s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst✝³] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst✝²] (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ x ∈ T y, U x y = ⊤
W : Y → Set Y := fun y ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst✝²] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst✝²] (E a)
hE : ⋃ i, E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y : Y
⊢ ∃ t ∈ 𝓝 (x, y), {i | ((fun z ↦ U (↑z.snd) z.fst ×ˢ E z.fst) i ∩ t).Nonempty}.Finite

case refine_3
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : ⋃ a, s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst✝³] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst✝²] (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ x ∈ T y, U x y = ⊤
W : Y → Set Y := fun y ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst✝²] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst✝²] (E a)
hE : ⋃ i, E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : (y : Y) × ↥(T y)
y : Y
x : X
hx : x ∈ T y
⊢ ∃ a, (fun z ↦ U (↑z.snd) z.fst ×ˢ E z.fst) ⟨y, ⟨x, hx⟩⟩ ⊆ s a