awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : ∀ (x : X), ∃ (a : α) (i : ι x), p x i ∧ s x i ⊆ S a
choose :
  ∀ (a : (x : X) → α) (f : (x : X) → ι x) (hp : ∀ (x : X), p x (f x)) (hsub : ∀ (x : X), s x (f x) ⊆ S (a 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 a f hp hsub using this
-- 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
a : (x : X) → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
rcases :
  ∀ (β : Type u) (t : β → Set X) (hto : ∀ (b : β), IsOpen[inst] (t b))
    (ht : Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ) (htf : LocallyFinite t)
    (hts : ∀ (b : β), ∃ (x : X), t b ⊆ s x (f 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:
rcases h f hp with ⟨β, t, hto, ht, htf, hts⟩
-- 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
a : (x : X) → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst] (t b)
ht : Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ (x : X), t b ⊆ s x (f 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

Tactic:
⟨range t, Subtype.val, forall_subtype_range_iff.2 hto, ?_, htf.on_range,
      forall_subtype_range_iff.2 fun b ↦ ?_⟩

Premises used: Iff.mpr, LocallyFinite.on_range, Set.Elem, And.intro, Exists.intro, Set.range, Subtype.val, Set.forall_subtype_range_iff
-- 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
a : (x : X) → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst] (t b)
ht : Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ (x : X), t b ⊆ s x (f x)
refine_1 : Eq.{v + 1} (α := Set X) (⋃ (b : (↑(range t) : Type v)), (↑b : Set X)) univ
refine_2 : ∀ (b : β), ∃ (a : α), (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ range t) (t b) ⋯) : Set X) ⊆ 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:
refine ⟨range t, Subtype.val, forall_subtype_range_iff.2 hto, ?_, htf.on_range,
      forall_subtype_range_iff.2 fun b ↦ ?_⟩
-- 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
a : (x : X) → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst] (t b)
ht : Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ (x : X), t b ⊆ s x (f x)
refine_1 :
  Eq.{v + 1} (α := Set X)
    (⋃ (x : Set X), ⋃ (hx : x ∈ range t), (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ range t) x hx) : Set X)) univ
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : Eq.{v + 1} (α := Set X) (⋃ (y : β), t y) univ
⊢ Eq.{v + 1} (α := Set X) (⋃ (b : (↑(range t) : Type v)), (↑b : Set X)) univ

Tactic:
rwa [iUnion_subtype, biUnion_range]

Premises used: Set.biUnion_range, Set.iUnion_subtype
-- 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
a : (x : X) → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst] (t b)
ht : Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ (x : X), t b ⊆ s x (f x)
b : β
refine_2 :
  ∀ (x : X) (hx : t b ⊆ s x (f x)),
    ∃ (a : α), (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ range t) (t b) ⋯) : Set X) ⊆ S a
⊢ ∃ (a : α), (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ range t) (t b) ⋯) : Set X) ⊆ S a

Tactic:
rcases hts b with ⟨x, hx⟩
-- 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
a : (x : X) → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst] (t b)
ht : Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ (x : X), t b ⊆ s x (f x)
b : β
x : X
hx : t b ⊆ s x (f x)
⊢ ∃ (a : α), (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ range t) (t b) ⋯) : Set X) ⊆ S a

Tactic:
⟨_, hx.trans (hsub _)⟩

Premises used: HasSubset.Subset.trans, Exists.intro
-- 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
a : (x : X) → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst] (t b)
ht : Eq.{v + 1} (α := Set X) (⋃ (b : β), t b) univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ (x : X), t b ⊆ s x (f x)
b : β
x : X
hx : t b ⊆ s x (f x)
⊢ ∃ (a : α), (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ range t) (t b) ⋯) : Set X) ⊆ S a

Tactic:
exact ⟨_, hx.trans (hsub _)⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), s a) univ
choose :
  ∀ (U : (a : α) → Set Y) (hUo : ∀ (a : α), IsOpen[inst_1] (U a)) (hU : ∀ (a : α), e ⁻¹' U a = 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
⊢ ∃ (β : 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 U hUo hU using fun a ↦ he.isOpen_iff.1 (ho a)

Premises used: Topology.IsInducing.isOpen_iff, Topology.IsClosedEmbedding.toIsEmbedding, Iff.mp, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), s a) univ
U : (a : α) → Set Y
hUo : ∀ (a : α), IsOpen[inst_1] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
simp :
  ∀ (hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), e ⁻¹' U 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 ⊆ e ⁻¹' U 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:
simp only [← hU] at hu ⊢
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
U : (a : α) → Set Y
hUo : ∀ (a : α), IsOpen[inst_1] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), e ⁻¹' U a) univ
⊢ range e ⊆ ⋃ (i : α), U i

Tactic:
simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using hu

Premises used: Set.iUnion_eq_univ_iff, Set.mem_iUnion, Set.range_subset_iff
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
U : (a : α) → Set Y
hUo : ∀ (a : α), IsOpen[inst_1] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), e ⁻¹' U a) univ
⊢ range e ⊆ ⋃ (i : α), U i

Tactic:
have heU : range e ⊆ ⋃ i, U i := by
      simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using hu
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
U : (a : α) → Set Y
hUo : ∀ (a : α), IsOpen[inst_1] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), e ⁻¹' U a) univ
heU : range e ⊆ ⋃ (i : α), U i
rcases :
  ∀ (V : α → Set Y) (hVo : ∀ (i : α), IsOpen[inst_1] (V i)) (heV : range e ⊆ ⋃ (i : α), V i) (hVf : LocallyFinite V)
    (hVU : ∀ (i : α), V i ⊆ U 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 ⊆ e ⁻¹' U 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 ⊆ e ⁻¹' U a

Tactic:
rcases precise_refinement_set he.isClosed_range U hUo heU with ⟨V, hVo, heV, hVf, hVU⟩

Premises used: precise_refinement_set, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
U : (a : α) → Set Y
hUo : ∀ (a : α), IsOpen[inst_1] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), e ⁻¹' U a) univ
heU : range e ⊆ ⋃ (i : α), U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen[inst_1] (V i)
heV : range e ⊆ ⋃ (i : α), V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U 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 ⊆ e ⁻¹' U a

Tactic:
⟨α, fun a ↦ e ⁻¹' (V a), fun a ↦ (hVo a).preimage he.continuous, ?_,
      hVf.preimage_continuous he.continuous, fun a ↦ ⟨a, preimage_mono (hVU a)⟩⟩

Premises used: Topology.IsClosedEmbedding.continuous, Set.preimage_mono, Set.preimage, LocallyFinite.preimage_continuous, And.intro, Exists.intro, IsOpen.preimage
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
U : (a : α) → Set Y
hUo : ∀ (a : α), IsOpen[inst_1] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), e ⁻¹' U a) univ
heU : range e ⊆ ⋃ (i : α), U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen[inst_1] (V i)
heV : range e ⊆ ⋃ (i : α), V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U i
refine : Eq.{v + 1} (α := Set X) (⋃ (b : α), (fun (a : α) ↦ e ⁻¹' V a) 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 ⊆ e ⁻¹' U a

Tactic:
refine ⟨α, fun a ↦ e ⁻¹' (V a), fun a ↦ (hVo a).preimage he.continuous, ?_,
      hVf.preimage_continuous he.continuous, fun a ↦ ⟨a, preimage_mono (hVU a)⟩⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst] (s a)
U : (a : α) → Set Y
hUo : ∀ (a : α), IsOpen[inst_1] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : Eq.{v + 1} (α := Set X) (⋃ (a : α), e ⁻¹' U a) univ
heU : range e ⊆ ⋃ (i : α), U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen[inst_1] (V i)
heV : range e ⊆ ⋃ (i : α), V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U i
⊢ Eq.{v + 1} (α := Set X) (⋃ (b : α), (fun (a : α) ↦ e ⁻¹' V a) b) univ

Tactic:
simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using heV

Premises used: Set.iUnion_eq_univ_iff, Set.mem_iUnion, Set.range_subset_iff
-- Module: Mathlib.Topology.Compactness.Paracompact
Goal:
X : Type v
Y : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ₜ Y
⊢ ParacompactSpace X ↔ ParacompactSpace Y

Tactic:
⟨fun _ ↦ e.symm.isClosedEmbedding.paracompactSpace, fun _ ↦ e.isClosedEmbedding.paracompactSpace⟩

Premises used: Topology.IsClosedEmbedding.paracompactSpace, Homeomorph.symm, Iff.intro, Homeomorph.isClosedEmbedding
-- 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
⊢ ∀ (x : X) (y : Y), ∃ (a : α) (U : Set X) (V : Set Y), IsOpen[inst] U ∧ IsOpen[inst_1] V ∧ x ∈ U ∧ y ∈ V ∧ U ×ˢ V ⊆ s a

Tactic:
have : ∀ (x : X) (y : Y), ∃ (a : α) (U : Set X) (V : Set Y),
        IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ U ×ˢ V ⊆ s a := fun x y ↦
      (iUnion_eq_univ_iff.1 hu (x, y)).imp fun a ha ↦ isOpen_prod_iff.1 (ho a) x y ha
-- 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
this :
  ∀ (x : X) (y : Y), ∃ (a : α) (U : Set X) (V : Set Y), IsOpen[inst] U ∧ IsOpen[inst_1] V ∧ x ∈ U ∧ y ∈ V ∧ U ×ˢ V ⊆ s a
choose :
  ∀ (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)),
    ∃ (β : 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
⊢ ∃ (β : 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:
choose a U V hUo hVo hxU hyV hUV using this
-- 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)
choose :
  ∀ (T : (y : Y) → Finset X) (hT : ∀ (y : Y), Eq.{v + 1} (α := Set X) (⋃ x ∈ T y, U x y) ⊤),
    ∃ (β : 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
⊢ ∃ (β : 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:
choose T hT using fun y ↦ CompactSpace.elim_nhds_subcover (U · y) fun x ↦
      (hUo x y).mem_nhds (hxU x y)

Premises used: IsOpen.mem_nhds, CompactSpace.elim_nhds_subcover
-- 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
⊢ ∀ (y : Y), IsOpen[inst_1] (W y)

Tactic:
have hWo : ∀ y, IsOpen (W y) := fun y ↦ isOpen_biInter_finset fun _ _ ↦ hVo _ _
-- 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)
⊢ ∀ (y : Y), y ∈ W y

Tactic:
have hW : ∀ y, y ∈ W y := fun _ ↦ mem_iInter₂.2 fun _ _ ↦ hyV _ _
-- 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
rcases :
  ∀ (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
⊢ ∃ (β : 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:
rcases precise_refinement W hWo (iUnion_eq_univ_iff.2 fun y ↦ ⟨y, hW y⟩)
      with ⟨E, hEo, hE, hEf, hEA⟩

Premises used: Iff.mpr, precise_refinement, Set.iUnion_eq_univ_iff, Exists.intro