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
x_1 : (y : Y) × ↥(T y)
y : Y
x : X
hx : x ∈ T y
refine_3 :
  E
      (Sigma.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))) ⊆
    V x 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:
refine ⟨a x y, (Set.prod_mono Subset.rfl ?_).trans (hUV x y)⟩
-- 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
⊢ E
      (Sigma.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))) ⊆
    V x y

Tactic:
(hEA _).trans (iInter₂_subset x hx)

Premises used: Set.iInter₂_subset, HasSubset.Subset.trans
-- 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
⊢ E
      (Sigma.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))) ⊆
    V x y

Tactic:
exact (hEA _).trans (iInter₂_subset x hx)

Premises used: Set.iInter₂_subset, HasSubset.Subset.trans
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ParacompactSpace X
inst_3 : CompactSpace Y
⊢ ParacompactSpace (X × Y)

Tactic:
(Homeomorph.prodComm X Y).paracompactSpace_iff.2 inferInstance

Premises used: Iff.mpr, inferInstance, Homeomorph.prodComm, Homeomorph.paracompactSpace_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
⊢ ParacompactSpace X

Tactic:
⟨fun ι s ho hu ↦ ?_⟩

Premises used: ParacompactSpace.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
refine :
  ∀ (ι : Type v) (s : ι → Set X) (ho : ∀ (a : ι), IsOpen[inst] (s a))
    (hu : Eq.{v + 1} (α := Set X) (⋃ (a : ι), s a) univ),
    ∃ (β : Type v) (t : β → Set X),
      (∀ (b : β), IsOpen[inst] (t b)) ∧
        Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
⊢ ParacompactSpace X

Tactic:
refine ⟨fun ι s ho hu ↦ ?_⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι_1 : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
ι : Type v
s : ι → Set X
ho : ∀ (a : ι), IsOpen[inst] (s a)
hu : Eq.{v + 1} (α := Set X) (⋃ (a : ι), s a) univ
rcases :
  ∀ (T : Finset ι) (hT : Subset.{v} (α := Set X) univ (⋃ i ∈ T, s i)),
    ∃ (β : Type v) (t : β → Set X),
      (∀ (b : β), IsOpen[inst] (t b)) ∧
        Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
⊢ ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a

Tactic:
rcases isCompact_univ.elim_finite_subcover _ ho hu.ge with ⟨T, hT⟩

Premises used: Eq.ge, IsCompact.elim_finite_subcover, isCompact_univ
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι_1 : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
ι : Type v
s : ι → Set X
ho : ∀ (a : ι), IsOpen[inst] (s a)
hu : Eq.{v + 1} (α := Set X) (⋃ (a : ι), s a) univ
T : Finset ι
hT : Subset.{v} (α := Set X) univ (⋃ i ∈ T, s i)
⊢ ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a

Tactic:
⟨(T : Set ι), fun t ↦ s t, fun t ↦ ho _, ?_, locallyFinite_of_finite _,
    fun t ↦ ⟨t, Subset.rfl⟩⟩

Premises used: locallyFinite_of_finite, Set.Elem, Set.Subset.rfl, SetLike.coe, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι_1 : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
ι : Type v
s : ι → Set X
ho : ∀ (a : ι), IsOpen[inst] (s a)
hu : Eq.{v + 1} (α := Set X) (⋃ (a : ι), s a) univ
T : Finset ι
hT : Subset.{v} (α := Set X) univ (⋃ i ∈ T, s i)
refine :
  Eq.{v + 1} (α := Set X) (⋃ (b : (↑(↑T : Set ι) : Type v)), (fun (t : (↑(↑T : Set ι) : Type v)) ↦ s (↑t : ι)) b) univ
⊢ ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a

Tactic:
refine ⟨(T : Set ι), fun t ↦ s t, fun t ↦ ho _, ?_, locallyFinite_of_finite _,
    fun t ↦ ⟨t, Subset.rfl⟩⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι_1 : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
ι : Type v
s : ι → Set X
ho : ∀ (a : ι), IsOpen[inst] (s a)
hu : Eq.{v + 1} (α := Set X) (⋃ (a : ι), s a) univ
T : Finset ι
hT : Subset.{v} (α := Set X) univ (⋃ i ∈ T, s i)
⊢ Eq.{v + 1} (α := Set X) (⋃ (b : (↑(↑T : Set ι) : Type v)), (fun (t : (↑(↑T : Set ι) : Type v)) ↦ s (↑t : ι)) b) univ

Tactic:
simpa only [iUnion_coe_set, ← univ_subset_iff]

Premises used: Set.univ_subset_iff, Set.iUnion_coe_set
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : SigmaCompactSpace X
inst_3 : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
hB : ∀ (x : X), (𝓝 x).HasBasis (p x) (B x)
⊢ ∃ (α : Type v) (c : α → X) (r : (a : α) → ι (c a)),
    (∀ (a : α), p (c a) (r a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (a : α), B (c a) (r a)) univ ∧ LocallyFinite (X := X) fun (a : α) ↦ B (c a) (r a)

Tactic:
let ⟨α, c, r, hp, hU, hfin⟩ :=
    refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set isClosed_univ fun x _ ↦ hB x
  ⟨α, c, r, fun a ↦ (hp a).2, univ_subset_iff.1 hU, hfin⟩

Premises used: isClosed_univ, Set.univ_subset_iff, Set.univ, Exists, refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set, LocallyFinite, And, And.right, And.intro, Exists.intro, Iff.mp, _private.0.refinement_of_locallyCompact_sigmaCompact_of_nhds_basis.match_1, Eq, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : SigmaCompactSpace X
inst_4 : T2Space X
⊢ ParacompactSpace X

Tactic:
⟨fun α s ho hc ↦ ?_⟩

Premises used: ParacompactSpace.mk
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : SigmaCompactSpace X
inst_4 : T2Space X
refine :
  ∀ (α : Type v) (s : α → Set X) (ho : ∀ (a : α), IsOpen[inst] (s a))
    (hc : Eq.{v + 1} (α := Set X) (⋃ (a : α), s a) univ),
    ∃ (β : Type v) (t : β → Set X),
      (∀ (b : β), IsOpen[inst] (t b)) ∧
        Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a
⊢ ParacompactSpace X

Tactic:
refine ⟨fun α s ho hc ↦ ?_⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : SigmaCompactSpace X
inst_4 : T2Space X
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
hc : Eq.{v + 1} (α := Set X) (⋃ (a : α), s a) univ
choose :
  ∀ (i : (x : X) → α) (hi : ∀ (x : X), x ∈ s (i x)),
    ∃ (β : Type v) (t : β → Set X),
      (∀ (b : β), IsOpen[inst] (t b)) ∧
        Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a
⊢ ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a

Tactic:
choose i hi using iUnion_eq_univ_iff.1 hc

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 : WeaklyLocallyCompactSpace X
inst_3 : SigmaCompactSpace X
inst_4 : T2Space X
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
hc : Eq.{v + 1} (α := Set X) (⋃ (a : α), s a) univ
i : (x : X) → α
hi : ∀ (x : X), x ∈ s (i x)
⊢ ∀ (x : X), (𝓝 x).HasBasis (fun (t : Set X) ↦ (x ∈ t ∧ IsOpen[inst] t) ∧ t ⊆ s (i x)) id

Tactic:
have : ∀ x : X, (𝓝 x).HasBasis (fun t : Set X ↦ (x ∈ t ∧ IsOpen t) ∧ t ⊆ s (i x)) id :=
    fun x : X ↦ (nhds_basis_opens x).restrict_subset (IsOpen.mem_nhds (ho (i x)) (hi x))
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : SigmaCompactSpace X
inst_4 : T2Space X
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
hc : Eq.{v + 1} (α := Set X) (⋃ (a : α), s a) univ
i : (x : X) → α
hi : ∀ (x : X), x ∈ s (i x)
this : ∀ (x : X), (𝓝 x).HasBasis (fun (t : Set X) ↦ (x ∈ t ∧ IsOpen[inst] t) ∧ t ⊆ s (i x)) id
rcases :
  ∀ (β : Type v) (c : β → X) (t : (a : β) → Set X)
    (hto : ∀ (a : β), (c a ∈ t a ∧ IsOpen[inst] (t a)) ∧ t a ⊆ s (i (c a)))
    (htc : Eq.{v + 1} (α := Set X) (⋃ (a : β), id (t a)) univ) (htf : LocallyFinite (X := X) fun (a : β) ↦ id (t a)),
    ∃ (β : Type v) (t : β → Set X),
      (∀ (b : β), IsOpen[inst] (t b)) ∧
        Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a
⊢ ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a

Tactic:
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis this with
    ⟨β, c, t, hto, htc, htf⟩

Premises used: refinement_of_locallyCompact_sigmaCompact_of_nhds_basis
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : SigmaCompactSpace X
inst_4 : T2Space X
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
hc : Eq.{v + 1} (α := Set X) (⋃ (a : α), s a) univ
i : (x : X) → α
hi : ∀ (x : X), x ∈ s (i x)
this : ∀ (x : X), (𝓝 x).HasBasis (fun (t : Set X) ↦ (x ∈ t ∧ IsOpen[inst] t) ∧ t ⊆ s (i x)) id
β : Type v
c : β → X
t : (a : β) → Set X
hto : ∀ (a : β), (c a ∈ t a ∧ IsOpen[inst] (t a)) ∧ t a ⊆ s (i (c a))
htc : Eq.{v + 1} (α := Set X) (⋃ (a : β), id (t a)) univ
htf : LocallyFinite (X := X) fun (a : β) ↦ id (t a)
⊢ ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a

Tactic:
⟨β, t, fun x ↦ (hto x).1.2, htc, htf, fun b ↦ ⟨i <| c b, (hto b).2⟩⟩

Premises used: And.right, And.left, 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 : WeaklyLocallyCompactSpace X
inst_3 : SigmaCompactSpace X
inst_4 : T2Space X
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
hc : Eq.{v + 1} (α := Set X) (⋃ (a : α), s a) univ
i : (x : X) → α
hi : ∀ (x : X), x ∈ s (i x)
this : ∀ (x : X), (𝓝 x).HasBasis (fun (t : Set X) ↦ (x ∈ t ∧ IsOpen[inst] t) ∧ t ⊆ s (i x)) id
β : Type v
c : β → X
t : (a : β) → Set X
hto : ∀ (a : β), (c a ∈ t a ∧ IsOpen[inst] (t a)) ∧ t a ⊆ s (i (c a))
htc : Eq.{v + 1} (α := Set X) (⋃ (a : β), id (t a)) univ
htf : LocallyFinite (X := X) fun (a : β) ↦ id (t a)
⊢ ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a

Tactic:
exact ⟨β, t, fun x ↦ (hto x).1.2, htc, htf, fun b ↦ ⟨i <| c b, (hto b).2⟩⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : ParacompactSpace X
s t : Set X
hs : IsClosed[inst] s
H : ∀ x ∈ s, ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
choose :
  ∀ (u v : (x : (↑s : Type v)) → Set X) (hu : ∀ (x : (↑s : Type v)), IsOpen[inst] (u x))
    (hv : ∀ (x : (↑s : Type v)), IsOpen[inst] (v x)) (hxu : ∀ (x : (↑s : Type v)), (↑x : X) ∈ u x)
    (htv : ∀ (x : (↑s : Type v)), t ⊆ v x) (huv : ∀ (x : (↑s : Type v)), Disjoint (u x) (v x)),
    ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
choose u v hu hv hxu htv huv using SetCoe.forall'.1 H

Premises used: Iff.mp, SetCoe.forall'
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : ParacompactSpace X
s t : Set X
hs : IsClosed[inst] s
H : ∀ x ∈ s, ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : (x : (↑s : Type v)) → Set X
hu : ∀ (x : (↑s : Type v)), IsOpen[inst] (u x)
hv : ∀ (x : (↑s : Type v)), IsOpen[inst] (v x)
hxu : ∀ (x : (↑s : Type v)), (↑x : X) ∈ u x
htv : ∀ (x : (↑s : Type v)), t ⊆ v x
huv : ∀ (x : (↑s : Type v)), Disjoint (u x) (v x)
rcases :
  ∀ (u' : (↑s : Type v) → Set X) (hu'o : ∀ (i : (↑s : Type v)), IsOpen[inst] (u' i))
    (hcov' : s ⊆ ⋃ (i : (↑s : Type v)), u' i) (hu'fin : LocallyFinite u') (hsub : ∀ (i : (↑s : Type v)), u' i ⊆ u i),
    ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
rcases precise_refinement_set hs u hu fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, hxu _⟩ with
      ⟨u', hu'o, hcov', hu'fin, hsub⟩

Premises used: Iff.mpr, Set.mem_iUnion, Subtype.mk, precise_refinement_set, 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 : T2Space X
inst_3 : ParacompactSpace X
s t : Set X
hs : IsClosed[inst] s
H : ∀ x ∈ s, ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : (x : (↑s : Type v)) → Set X
hu : ∀ (x : (↑s : Type v)), IsOpen[inst] (u x)
hv : ∀ (x : (↑s : Type v)), IsOpen[inst] (v x)
hxu : ∀ (x : (↑s : Type v)), (↑x : X) ∈ u x
htv : ∀ (x : (↑s : Type v)), t ⊆ v x
huv : ∀ (x : (↑s : Type v)), Disjoint (u x) (v x)
u' : (↑s : Type v) → Set X
hu'o : ∀ (i : (↑s : Type v)), IsOpen[inst] (u' i)
hcov' : s ⊆ ⋃ (i : (↑s : Type v)), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : (↑s : Type v)), u' i ⊆ u i
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
⟨⋃ i, u' i, (closure (⋃ i, u' i))ᶜ, isOpen_iUnion hu'o, isClosed_closure.isOpen_compl,
      hcov', ?_, disjoint_compl_right.mono le_rfl (compl_le_compl subset_closure)⟩

Premises used: le_rfl, IsClosed.isOpen_compl, subset_closure, Compl.compl, compl_le_compl, closure, isOpen_iUnion, And.intro, Exists.intro, disjoint_compl_right, Disjoint.mono, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : ParacompactSpace X
s t : Set X
hs : IsClosed[inst] s
H : ∀ x ∈ s, ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : (x : (↑s : Type v)) → Set X
hu : ∀ (x : (↑s : Type v)), IsOpen[inst] (u x)
hv : ∀ (x : (↑s : Type v)), IsOpen[inst] (v x)
hxu : ∀ (x : (↑s : Type v)), (↑x : X) ∈ u x
htv : ∀ (x : (↑s : Type v)), t ⊆ v x
huv : ∀ (x : (↑s : Type v)), Disjoint (u x) (v x)
u' : (↑s : Type v) → Set X
hu'o : ∀ (i : (↑s : Type v)), IsOpen[inst] (u' i)
hcov' : s ⊆ ⋃ (i : (↑s : Type v)), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : (↑s : Type v)), u' i ⊆ u i
refine : t ⊆ (closure[inst] (⋃ (i : (↑s : Type v)), u' i))ᶜ
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
refine ⟨⋃ i, u' i, (closure (⋃ i, u' i))ᶜ, isOpen_iUnion hu'o, isClosed_closure.isOpen_compl,
      hcov', ?_, disjoint_compl_right.mono le_rfl (compl_le_compl subset_closure)⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : ParacompactSpace X
s t : Set X
hs : IsClosed[inst] s
H : ∀ x ∈ s, ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : (x : (↑s : Type v)) → Set X
hu : ∀ (x : (↑s : Type v)), IsOpen[inst] (u x)
hv : ∀ (x : (↑s : Type v)), IsOpen[inst] (v x)
hxu : ∀ (x : (↑s : Type v)), (↑x : X) ∈ u x
htv : ∀ (x : (↑s : Type v)), t ⊆ v x
huv : ∀ (x : (↑s : Type v)), Disjoint (u x) (v x)
u' : (↑s : Type v) → Set X
hu'o : ∀ (i : (↑s : Type v)), IsOpen[inst] (u' i)
hcov' : s ⊆ ⋃ (i : (↑s : Type v)), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : (↑s : Type v)), u' i ⊆ u i
rw : ∀ (i : (↑s : Type v)), t ⊆ (closure[inst] (u' i))ᶜ
⊢ t ⊆ (closure[inst] (⋃ (i : (↑s : Type v)), u' i))ᶜ

Tactic:
rw [hu'fin.closure_iUnion, compl_iUnion, subset_iInter_iff]

Premises used: Set.subset_iInter_iff, LocallyFinite.closure_iUnion, Set.compl_iUnion
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : ParacompactSpace X
s t : Set X
hs : IsClosed[inst] s
H : ∀ x ∈ s, ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : (x : (↑s : Type v)) → Set X
hu : ∀ (x : (↑s : Type v)), IsOpen[inst] (u x)
hv : ∀ (x : (↑s : Type v)), IsOpen[inst] (v x)
hxu : ∀ (x : (↑s : Type v)), (↑x : X) ∈ u x
htv : ∀ (x : (↑s : Type v)), t ⊆ v x
huv : ∀ (x : (↑s : Type v)), Disjoint (u x) (v x)
u' : (↑s : Type v) → Set X
hu'o : ∀ (i : (↑s : Type v)), IsOpen[inst] (u' i)
hcov' : s ⊆ ⋃ (i : (↑s : Type v)), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : (↑s : Type v)), u' i ⊆ u i
⊢ ∀ (i : (↑s : Type v)), t ⊆ (closure[inst] (u' i))ᶜ

Tactic:
fun i x hxt hxu ↦
      absurd (htv i hxt) (closure_minimal ?_ (isClosed_compl_iff.2 <| hv _) hxu)

Premises used: Iff.mpr, Set.Mem, closure_minimal, setOf, Set.Subset, absurd, Not, isClosed_compl_iff
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : ParacompactSpace X
s t : Set X
hs : IsClosed[inst] s
H : ∀ x ∈ s, ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : (x : (↑s : Type v)) → Set X
hu : ∀ (x : (↑s : Type v)), IsOpen[inst] (u x)
hv : ∀ (x : (↑s : Type v)), IsOpen[inst] (v x)
hxu : ∀ (x : (↑s : Type v)), (↑x : X) ∈ u x
htv : ∀ (x : (↑s : Type v)), t ⊆ v x
huv : ∀ (x : (↑s : Type v)), Disjoint (u x) (v x)
u' : (↑s : Type v) → Set X
hu'o : ∀ (i : (↑s : Type v)), IsOpen[inst] (u' i)
hcov' : s ⊆ ⋃ (i : (↑s : Type v)), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : (↑s : Type v)), u' i ⊆ u i
refine : ∀ (i : (↑s : Type v)) (x : X) (hxt : x ∈ t) (hxu : x ∈ closure[inst] (u' i)), u' i ⊆ (v i)ᶜ
⊢ ∀ (i : (↑s : Type v)), t ⊆ (closure[inst] (u' i))ᶜ

Tactic:
refine fun i x hxt hxu ↦
      absurd (htv i hxt) (closure_minimal ?_ (isClosed_compl_iff.2 <| hv _) hxu)

Premises used: Iff.mpr, closure_minimal, absurd, isClosed_compl_iff
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : ParacompactSpace X
s t : Set X
hs : IsClosed[inst] s
H : ∀ x ∈ s, ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : (x : (↑s : Type v)) → Set X
hu : ∀ (x : (↑s : Type v)), IsOpen[inst] (u x)
hv : ∀ (x : (↑s : Type v)), IsOpen[inst] (v x)
hxu_1 : ∀ (x : (↑s : Type v)), (↑x : X) ∈ u x
htv : ∀ (x : (↑s : Type v)), t ⊆ v x
huv : ∀ (x : (↑s : Type v)), Disjoint (u x) (v x)
u' : (↑s : Type v) → Set X
hu'o : ∀ (i : (↑s : Type v)), IsOpen[inst] (u' i)
hcov' : s ⊆ ⋃ (i : (↑s : Type v)), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : (↑s : Type v)), u' i ⊆ u i
i : (↑s : Type v)
x : X
hxt : x ∈ t
hxu : x ∈ closure[inst] (u' i)
⊢ u' i ⊆ (v i)ᶜ

Tactic:
fun y hyu hyv ↦ (huv i).le_bot ⟨hsub _ hyu, hyv⟩

Premises used: Disjoint.le_bot, Set.Mem, setOf, Set.Subset, And.intro, Not