awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
⊢ ∃ (β : Type (max v w)) (t : β → Set (X × Y)),
    (∀ (b : β), IsOpen[instTopologicalSpaceProd] (t b)) ∧
      Eq (α := Set (X × Y)) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a

Tactic:
⟨Σ 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⟩ ↦ ?_⟩

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff, SProd.sprod, setOf, Set.Finite, Membership.mem, Exists, nhds, Subtype, HasSubset.Subset, Sigma.fst, _private.0.instParacompactSpaceProdOfCompactSpace.match_2, Inter.inter, And, Set.Nonempty, And.intro, Exists.intro, Sigma.snd, Subtype.val, _private.0.instParacompactSpaceProdOfCompactSpace.match_1, Sigma, IsOpen.prod
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
refine_1 :
  ∀ (x : X × Y) (x : X) (y : Y),
    ∃ (i : (y : Y) × ↥(T y)),
      (x, y) ∈
        U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
          E (i.fst (β := fun (y : Y) ↦ ↥(T y)))
refine_2 :
  ∀ (x : X × Y) (x : X) (y : Y),
    ∃ t ∈ 𝓝 (x, y),
      Set.Finite (α := (y : Y) × ↥(T y))
        {i : (y : Y) × ↥(T y) |
          ((fun (z : (y : Y) × ↥(T y)) ↦
                  U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                    E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
                i ∩
              t).Nonempty}
refine_3 :
  ∀ (x : (y : Y) × ↥(T y)) (y : Y) (x : X) (hx : x ∈ T y),
    ∃ (a : α),
      (fun (z : (y : Y) × ↥(T y)) ↦
            U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
              E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
          (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) y (Subtype.mk (p := fun (x : X) ↦ x ∈ T y) x hx)) ⊆
        s a
⊢ ∃ (β : Type (max v w)) (t : β → Set (X × Y)),
    (∀ (b : β), IsOpen[instTopologicalSpaceProd] (t b)) ∧
      Eq (α := Set (X × Y)) (⋃ (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⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y : Y
refine_1 :
  ∀ (b : Y) (hb : y ∈ E b),
    ∃ (i : (y : Y) × ↥(T y)),
      (x, y) ∈
        U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
          E (i.fst (β := fun (y : Y) ↦ ↥(T y)))
⊢ ∃ (i : (y : Y) × ↥(T y)),
    (x, y) ∈
      U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
        E (i.fst (β := fun (y : Y) ↦ ↥(T y)))

Tactic:
rcases iUnion_eq_univ_iff.1 hE y with ⟨b, hb⟩

Premises used: Set.iUnion_eq_univ_iff, Iff.mp
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y b : Y
hb : y ∈ E b
refine_1 :
  ∀ (a : X) (ha : a ∈ T b) (hx : x ∈ U a b),
    ∃ (i : (y : Y) × ↥(T y)),
      (x, y) ∈
        U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
          E (i.fst (β := fun (y : Y) ↦ ↥(T y)))
⊢ ∃ (i : (y : Y) × ↥(T y)),
    (x, y) ∈
      U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
        E (i.fst (β := fun (y : Y) ↦ ↥(T y)))

Tactic:
rcases iUnion₂_eq_univ_iff.1 (hT b) x with ⟨a, ha, hx⟩

Premises used: Iff.mp, Set.iUnion₂_eq_univ_iff
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a_1 : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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_1 x y)
T : (y : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y b : Y
hb : y ∈ E b
a : X
ha : a ∈ T b
hx : x ∈ U a b
⊢ ∃ (i : (y : Y) × ↥(T y)),
    (x, y) ∈
      U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
        E (i.fst (β := fun (y : Y) ↦ ↥(T y)))

Tactic:
⟨⟨b, a, ha⟩, hx, hb⟩

Premises used: Subtype.mk, And.intro, Exists.intro, Sigma.mk
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a_1 : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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_1 x y)
T : (y : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y b : Y
hb : y ∈ E b
a : X
ha : a ∈ T b
hx : x ∈ U a b
⊢ ∃ (i : (y : Y) × ↥(T y)),
    (x, y) ∈
      U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
        E (i.fst (β := fun (y : Y) ↦ ↥(T y)))

Tactic:
exact ⟨⟨b, a, ha⟩, hx, hb⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y : Y
refine_2 :
  ∀ (t : Set Y) (ht : t ∈ 𝓝 y) (htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}),
    ∃ t ∈ 𝓝 (x, y),
      Set.Finite (α := (y : Y) × ↥(T y))
        {i : (y : Y) × ↥(T y) |
          ((fun (z : (y : Y) × ↥(T y)) ↦
                  U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                    E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
                i ∩
              t).Nonempty}
⊢ ∃ t ∈ 𝓝 (x, y),
    Set.Finite (α := (y : Y) × ↥(T y))
      {i : (y : Y) × ↥(T y) |
        ((fun (z : (y : Y) × ↥(T y)) ↦
                U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                  E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
              i ∩
            t).Nonempty}

Tactic:
rcases hEf y with ⟨t, ht, htf⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 (x, y),
    Set.Finite (α := (y : Y) × ↥(T y))
      {i : (y : Y) × ↥(T y) |
        ((fun (z : (y : Y) × ↥(T y)) ↦
                U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                  E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
              i ∩
            t).Nonempty}

Tactic:
⟨univ ×ˢ t, prod_mem_nhds univ_mem ht, ?_⟩

Premises used: prod_mem_nhds, SProd.sprod, Set.univ, And.intro, Exists.intro, Filter.univ_mem
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}
refine_2 :
  Set.Finite (α := (y : Y) × ↥(T y))
    {i : (y : Y) × ↥(T y) |
      ((fun (z : (y : Y) × ↥(T y)) ↦
              U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
            i ∩
          SProd.sprod (α := Set X) univ t).Nonempty}
⊢ ∃ t ∈ 𝓝 (x, y),
    Set.Finite (α := (y : Y) × ↥(T y))
      {i : (y : Y) × ↥(T y) |
        ((fun (z : (y : Y) × ↥(T y)) ↦
                U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                  E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
              i ∩
            t).Nonempty}

Tactic:
refine ⟨univ ×ˢ t, prod_mem_nhds univ_mem ht, ?_⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}
⊢ Set.Finite (α := (y : Y) × ↥(T y))
    {i : (y : Y) × ↥(T y) |
      ((fun (z : (y : Y) × ↥(T y)) ↦
              U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
            i ∩
          SProd.sprod (α := Set X) univ t).Nonempty}

Tactic:
(htf.biUnion fun y _ ↦ finite_range (Sigma.mk y)).subset ?_

Premises used: Set.finite_range, Set.Finite.subset, Set.Finite.biUnion, Sigma.mk
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}
refine_2 :
  Subset (α := Set ((y : Y) × ↥(T y)))
    {i : (y : Y) × ↥(T y) |
      ((fun (z : (y : Y) × ↥(T y)) ↦
              U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
            i ∩
          SProd.sprod (α := Set X) univ t).Nonempty}
    (⋃ (i : Y),
      ⋃ (_ : Membership.mem (γ := Set Y) {i : Y | (E i ∩ t).Nonempty} i),
        range (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) i))
⊢ Set.Finite (α := (y : Y) × ↥(T y))
    {i : (y : Y) × ↥(T y) |
      ((fun (z : (y : Y) × ↥(T y)) ↦
              U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
            i ∩
          SProd.sprod (α := Set X) univ t).Nonempty}

Tactic:
refine (htf.biUnion fun y _ ↦ finite_range (Sigma.mk y)).subset ?_

Premises used: Set.finite_range, Set.Finite.subset, Set.Finite.biUnion, Sigma.mk
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a_1 : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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_1 x y)
T : (y : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}
b : Y
a : X
ha : a ∈ T b
c : X
d : Y
hd : d ∈ E b
hdt : d ∈ t
⊢ Membership.mem (γ := Set ((y : Y) × ↥(T y)))
    (⋃ (i : Y),
      ⋃ (_ : Membership.mem (γ := Set Y) {i : Y | (E i ∩ t).Nonempty} i),
        range (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) i))
    (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) b (Subtype.mk (p := fun (x : X) ↦ x ∈ T b) a ha))

Tactic:
mem_iUnion₂.2 ⟨b, ⟨d, hd, hdt⟩, mem_range_self _⟩

Premises used: Set.mem_range_self, Iff.mpr, Set.Mem, Set.mem_iUnion₂, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a_1 : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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_1 x y)
T : (y : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}
b : Y
a : X
ha : a ∈ T b
c : X
d : Y
hd : d ∈ E b
hdt : d ∈ t
⊢ Membership.mem (γ := Set ((y : Y) × ↥(T y)))
    (⋃ (i : Y),
      ⋃ (_ : Membership.mem (γ := Set Y) {i : Y | (E i ∩ t).Nonempty} i),
        range (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) i))
    (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) b (Subtype.mk (p := fun (x : X) ↦ x ∈ T b) a ha))

Tactic:
exact mem_iUnion₂.2 ⟨b, ⟨d, hd, hdt⟩, mem_range_self _⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : Eq (α := Set (X × Y)) (⋃ (a : α), s a) univ
a : (x : X) → (y : Y) → α
U : (x : X) → (y : Y) → Set X
V : (x : X) → (y : Y) → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst_1] (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 : Y) → Finset X
hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤
W : Y → Set Y := fun (y : Y) ↦ ⋂ x ∈ T y, V x y
hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen[inst_1] (E a)
hE : Eq.{w + 1} (α := Set Y) (⋃ (i : Y), E i) univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x_1 : (y : Y) × ↥(T y)
y : Y
x : X
hx : x ∈ T y
⊢ ∃ (a : α),
    (fun (z : (y : Y) × ↥(T y)) ↦
          U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
            E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
        (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) y (Subtype.mk (p := fun (x : X) ↦ x ∈ T y) x hx)) ⊆
      s a

Tactic:
⟨a x y, (Set.prod_mono Subset.rfl ?_).trans (hUV x y)⟩

Premises used: HasSubset.Subset.trans, Set.Subset.rfl, Exists.intro, Set.prod_mono