awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
rwa : Eq.{v + 1} (α := Set X) (⋃₀ range fun (r : (↑(range u) : Type v)) ↦ (↑r : Set X)) univ
rwa₁ rwa₂ rwa₃ rwa₄ : ⋃₀ range u = univ
⊢ Eq.{v + 1} (α := Set X) (⋃ (a : (↑(range u) : Type v)), (fun (r : (↑(range u) : Type v)) ↦ (↑r : Set X)) a) univ

Tactic:
rwa [← sUnion_range, Subtype.range_coe]

Premises used: Set.sUnion_range, Subtype.range_coe
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
⊢ ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧
        LocallyFinite t ∧
          ∀ (b : β), ∃ (a : (↑(range u) : Type v)), t b ⊆ (fun (r : (↑(range u) : Type v)) ↦ (↑r : Set X)) a

Tactic:
have := ParacompactSpace.locallyFinite_refinement (range u) (fun r ↦ (r : Set X))
    (forall_subtype_range_iff.2 uo) (by rwa [← sUnion_range, Subtype.range_coe])
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
this :
  ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧
        LocallyFinite t ∧
          ∀ (b : β), ∃ (a : (↑(range u) : Type v)), t b ⊆ (fun (r : (↑(range u) : Type v)) ↦ (↑r : Set X)) a
⊢ ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      (∀ (x : X), ∃ (i : β), x ∈ t i) ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (i : ι), t b ⊆ u i

Tactic:
simp only [exists_subtype_range_iff, iUnion_eq_univ_iff] at this

Premises used: Set.iUnion_eq_univ_iff, Set.exists_subtype_range_iff
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
this :
  ∃ (β : Type v) (t : β → Set X),
    (∀ (b : β), IsOpen[inst] (t b)) ∧
      (∀ (x : X), ∃ (i : β), x ∈ t i) ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (i : ι), t b ⊆ u i
choose :
  ∀ (α : Type v) (t : α → Set X) (hto : ∀ (b : α), IsOpen[inst] (t b)) (hXt : ∀ (x : X), ∃ (i : α), x ∈ t i)
    (htf : LocallyFinite t) (ind : (b : α) → ι) (hind : ∀ (b : α), t b ⊆ u (ind b)),
    ∃ (v : ι → Set X),
      (∀ (a : ι), IsOpen[inst] (v a)) ∧
        Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a

Tactic:
choose α t hto hXt htf ind hind using this
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
hXt : ∀ (x : X), ∃ (i : α), x ∈ t i
htf : LocallyFinite t
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
choose :
  ∀ (t_inv : (x : X) → α) (ht_inv : ∀ (x : X), x ∈ t (t_inv x)),
    ∃ (v : ι → Set X),
      (∀ (a : ι), IsOpen[inst] (v a)) ∧
        Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a

Tactic:
choose t_inv ht_inv using hXt
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
htf : LocallyFinite t
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
choose :
  ∀ (U : (x : X) → Set X) (hxU : ∀ (x : X), U x ∈ 𝓝 x)
    (hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}),
    ∃ (v : ι → Set X),
      (∀ (a : ι), IsOpen[inst] (v a)) ∧
        Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a

Tactic:
choose U hxU hU using htf
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a

Tactic:
⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, ?_, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
refine_1 : ∀ (a : ι), IsOpen[inst] ((fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) a)
refine_2 : Eq.{v + 1} (α := Set X) (⋃ (i : ι), (fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) i) univ
refine_3 : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ ⋃ (a : α), ⋃ (_ : ind a = i), t a
refine_4 : ∀ (a : ι), (fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) a ⊆ u a
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a

Tactic:
refine ⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
⊢ ∀ (a : ι), IsOpen[inst] ((fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) a)

Tactic:
fun a ↦ isOpen_iUnion fun a ↦ isOpen_iUnion fun _ ↦ hto a

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
⊢ ∀ (a : ι), IsOpen[inst] ((fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) a)

Tactic:
exact fun a ↦ isOpen_iUnion fun a ↦ isOpen_iUnion fun _ ↦ hto a

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
refine_2 : ∀ (x : X), ∃ (i : ι) (i_1 : α) (_ : ind i_1 = i), x ∈ t i_1
⊢ Eq.{v + 1} (α := Set X) (⋃ (i : ι), (fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) i) univ

Tactic:
simp only [eq_univ_iff_forall, mem_iUnion]

Premises used: Set.eq_univ_iff_forall, Set.mem_iUnion
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
⊢ ∀ (x : X), ∃ (i : ι) (i_1 : α) (_ : ind i_1 = i), x ∈ t i_1

Tactic:
fun x ↦ ⟨ind (t_inv x), _, rfl, ht_inv _⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
⊢ ∀ (x : X), ∃ (i : ι) (i_1 : α) (_ : ind i_1 = i), x ∈ t i_1

Tactic:
exact fun x ↦ ⟨ind (t_inv x), _, rfl, ht_inv _⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
⊢ LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ ⋃ (a : α), ⋃ (_ : ind a = i), t a

Tactic:
fun x ↦ ⟨U x, hxU x, ((hU x).image ind).subset ?_⟩

Premises used: Set.Finite.subset, Set.Finite.image, LocallyFinite, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
refine_3 :
  ∀ (x : X),
    {i : ι | ((fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) i ∩ U x).Nonempty} ⊆
      ind '' {i : α | (t i ∩ U x).Nonempty}
⊢ LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ ⋃ (a : α), ⋃ (_ : ind a = i), t a

Tactic:
refine fun x ↦ ⟨U x, hxU x, ((hU x).image ind).subset ?_⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
x : X
refine_3 :
  ∀ (x_1 : ι),
    (∃ (x_2 : X), (∃ (i : α) (_ : ind i = x_1), x_2 ∈ t i) ∧ x_2 ∈ U x) → x_1 ∈ ind '' {i : α | ∃ x_2 ∈ t i, x_2 ∈ U x}
⊢ {i : ι | ((fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) i ∩ U x).Nonempty} ⊆
    ind '' {i : α | (t i ∩ U x).Nonempty}

Tactic:
simp only [subset_def, mem_iUnion, mem_setOf_eq, Set.Nonempty, mem_inter_iff]

Premises used: Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion, Set.mem_setOf_eq, Set.Nonempty
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
x y : X
hyU : y ∈ U x
a : α
hya : y ∈ t a
⊢ ind a ∈ ind '' {i : α | ∃ x_1 ∈ t i, x_1 ∈ U x}

Tactic:
mem_image_of_mem _ ⟨y, hya, hyU⟩

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
x y : X
hyU : y ∈ U x
a : α
hya : y ∈ t a
⊢ ind a ∈ ind '' {i : α | ∃ x_1 ∈ t i, x_1 ∈ U x}

Tactic:
exact mem_image_of_mem _ ⟨y, hya, hyU⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
refine_4 : ∀ (a : ι) (x : X), (∃ (i : α) (_ : ind i = a), x ∈ t i) → x ∈ u a
⊢ ∀ (a : ι), (fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) a ⊆ u a

Tactic:
simp only [subset_def, mem_iUnion]

Premises used: Set.subset_def, Set.mem_iUnion
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
x : X
a : α
hxa : x ∈ t a
⊢ x ∈ u (ind a)

Tactic:
hind _ hxa
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst] (u a)
uc : Eq.{v + 1} (α := Set X) (⋃ (i : ι), u i) univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst] (t b)
ind : (b : α) → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : (x : X) → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite.{v} (α := α) {i : α | (t i ∩ U x).Nonempty}
x : X
a : α
hxa : x ∈ t a
⊢ x ∈ u (ind a)

Tactic:
exact hind _ hxa
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
apply : Subset.{v} (α := Set X) univ (⋃ (i : Option ι), Option.elim' sᶜ u i)
⊢ Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), Option.elim' sᶜ u i) univ

Tactic:
apply Subset.antisymm (subset_univ _)

Premises used: Set.Subset.antisymm, Set.subset_univ
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
simp_rw : sᶜ ∪ s ⊆ sᶜ ∪ ⋃ (a : ι), u a
⊢ Subset.{v} (α := Set X) univ (⋃ (i : Option ι), Option.elim' sᶜ u i)

Tactic:
simp_rw [← compl_union_self s, Option.elim', iUnion_option]

Premises used: Option.elim', Set.iUnion_option, Set.compl_union_self
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ sᶜ ∪ s ⊆ sᶜ ∪ ⋃ (a : ι), u a

Tactic:
apply union_subset_union_right sᶜ us

Premises used: Compl.compl, Set.union_subset_union_right
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), Option.elim' sᶜ u i) univ

Tactic:
have uc : (iUnion fun i => Option.elim' sᶜ u i) = univ := by
    apply Subset.antisymm (subset_univ _)
    · simp_rw [← compl_union_self s, Option.elim', iUnion_option]
      apply union_subset_union_right sᶜ us
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), Option.elim' sᶜ u i) univ
rcases :
  ∀ (v : Option ι → Set X) (vo : ∀ (a : Option ι), IsOpen[inst] (v a))
    (vc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), v i) univ) (vf : LocallyFinite v)
    (vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a),
    ∃ (v : ι → Set X), (∀ (i : ι), IsOpen[inst] (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
⊢ ∃ (v : ι → Set X), (∀ (i : ι), IsOpen[inst] (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i

Tactic:
rcases precise_refinement (Option.elim' sᶜ u) (Option.forall.2 ⟨isOpen_compl_iff.2 hs, uo⟩)
      uc with
    ⟨v, vo, vc, vf, vu⟩

Premises used: Iff.mpr, Option.elim', precise_refinement, Compl.compl, Option.forall, And.intro, isOpen_compl_iff
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), Option.elim' sᶜ u i) univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen[inst] (v a)
vc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), v i) univ
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a
⊢ ∃ (v : ι → Set X), (∀ (i : ι), IsOpen[inst] (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i

Tactic:
⟨v ∘ some, fun i ↦ vo _, ?_, vf.comp_injective (Option.some_injective _), fun i ↦ vu _⟩

Premises used: Option.some, Function.comp, And.intro, Exists.intro, Option.some_injective, LocallyFinite.comp_injective
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), Option.elim' sᶜ u i) univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen[inst] (v a)
vc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), v i) univ
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a
refine : s ⊆ ⋃ (i : ι), (v ∘ some) i
⊢ ∃ (v : ι → Set X), (∀ (i : ι), IsOpen[inst] (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i

Tactic:
refine ⟨v ∘ some, fun i ↦ vo _, ?_, vf.comp_injective (Option.some_injective _), fun i ↦ vu _⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), Option.elim' sᶜ u i) univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen[inst] (v a)
vc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), v i) univ
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a
⊢ (v none)ᶜ ⊆ ⋃ (i : ι), v (some i)

Tactic:
simp only [iUnion_option, ← compl_subset_iff_union] at vc

Premises used: Set.compl_subset_iff_union, Set.iUnion_option
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), Option.elim' sᶜ u i) univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen[inst] (v a)
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a
vc : (v none)ᶜ ⊆ ⋃ (i : ι), v (some i)
⊢ s ⊆ ⋃ (i : ι), (v ∘ some) i

Tactic:
Subset.trans (subset_compl_comm.1 <| vu Option.none) vc

Premises used: Set.Subset.trans, Set.subset_compl_comm, Option.none, Iff.mp
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
inst_1 : ParacompactSpace X
s : Set X
hs : IsClosed[inst] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst] (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : Eq.{v + 1} (α := Set X) (⋃ (i : Option ι), Option.elim' sᶜ u i) univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen[inst] (v a)
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a
vc : (v none)ᶜ ⊆ ⋃ (i : ι), v (some i)
⊢ s ⊆ ⋃ (i : ι), (v ∘ some) i

Tactic:
exact Subset.trans (subset_compl_comm.1 <| vu Option.none) vc

Premises used: Set.Subset.trans, Set.subset_compl_comm, Option.none, Iff.mp
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
inst : TopologicalSpace X
ι : X → Sort u_1
p : (x : X) → ι x → Prop
s : (x : X) → ι x → Set X
hb : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h :
  ∀ (f : (x : X) → ι x),
    (∀ (x : X), p x (f x)) →
      ∃ (β : Type u) (t : β → Set X),
        (∀ (b : β), IsOpen[inst] (t b)) ∧
          Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (x : X), t b ⊆ s x (f x)
α : Type v
S : α → Set X
ho : ∀ (a : α), IsOpen[inst] (S a)
hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), S a) univ
⊢ ∀ (x : X), ∃ (a : α) (i : ι x), p x i ∧ s x i ⊆ S a

Tactic:
have := fun x ↦ (iUnion_eq_univ_iff.1 hu x).imp fun a ha ↦ (hb _).mem_iff.1 ((ho a).mem_nhds ha)