Module: Mathlib.Topology.Compactness.Paracompact

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

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

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

Tactic:
· rcases iUnion_eq_univ_iff.1 hE y with ⟨b, hb⟩
      rcases iUnion₂_eq_univ_iff.1 (hT b) x with ⟨a, ha, hx⟩
      exact ⟨⟨b, a, ha⟩, hx, hb⟩

Goal state after:
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