awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (β : 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
have 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
Tactic: choose a f hp hsub using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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 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
have 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
Tactic: rcases h f hp with ⟨β, t, hto, ht, htf, hts⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
have refine_1 : Eq.{v + 1} (α := Set X) (⋃ (b : (↑(range t) : Type v)), (↑b : Set X)) univ
Tactic: refine ⟨range t, Subtype.val, forall_subtype_range_iff.2 hto, ?_, htf.on_range,
      forall_subtype_range_iff.2 fun b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (β : 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
have refine_2 : ∀ (b : β), ∃ (a : α), (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ range t) (t b) sorry) : Set X) ⊆ S a
Tactic: refine ⟨range t, Subtype.val, forall_subtype_range_iff.2 hto, ?_, htf.on_range,
      forall_subtype_range_iff.2 fun b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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)
⊢ Eq.{v + 1} (α := Set X) (⋃ (b : (↑(range t) : Type v)), (↑b : Set X)) univ
have 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
Tactic: rwa [iUnion_subtype, biUnion_range]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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 : β
⊢ ∃ (a : α), (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ range t) (t b) ⋯) : Set X) ⊆ S a
have refine_2 : ∀ (x : X) (hx : t b ⊆ s x (f x)), ∃ (a : α), (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ range t) (t b) sorry) : Set X) ⊆ S a
Tactic: rcases hts b with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (β : 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
have 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
Tactic: choose U hUo hU using fun a ↦ he.isOpen_iff.1 (ho a)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (β : 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
have 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
Tactic: simp only [← hU] at hu ⊢
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (hypothesis)
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
⊢ ∃ (β : 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
have heU : 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
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (β : 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
have 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
Tactic: rcases precise_refinement_set he.isClosed_range U hUo heU with ⟨V, hVo, heV, hVf, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
have refine : Eq.{v + 1} (α := Set X) (⋃ (b : α), (fun (a : α) ↦ e ⁻¹' V a) b) univ
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)⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (hypothesis)
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
⊢ ∃ (β : 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
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (β : 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
have 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
Tactic: choose a U V hUo hVo hxU hyV hUV using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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)
⊢ ∃ (β : 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
have 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
Tactic: choose T hT using fun y ↦ CompactSpace.elim_nhds_subcover (U · y) fun x ↦
      (hUo x y).mem_nhds (hxU x y)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (hypothesis)
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
⊢ ∃ (β : 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
have hWo : ∀ (y : Y), IsOpen[inst_1] (W y)
Tactic: have hWo : ∀ y, IsOpen (W y) := fun y ↦ isOpen_biInter_finset fun _ _ ↦ hVo _ _
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (hypothesis)
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)
⊢ ∃ (β : 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
have hW : ∀ (y : Y), y ∈ W y
Tactic: have hW : ∀ y, y ∈ W y := fun _ ↦ mem_iInter₂.2 fun _ _ ↦ hyV _ _
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (β : 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
have 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
Tactic: rcases precise_refinement W hWo (iUnion_eq_univ_iff.2 fun y ↦ ⟨y, hW y⟩)
      with ⟨E, hEo, hE, hEf, hEA⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
have 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)))
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⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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)))
⊢ ∃ (β : 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
have 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}
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⟩ ↦ ?_⟩