awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
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}
⊢ ∃ (β : 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_3 : ∀ (x : (y : Y) × ↥(T y)) (y : Y) (x : X) (hx : x ∈ T y),
  ∃ (a : α),
    (fun (z : (y : Y) × ↥(T y)) ↦
          U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
            E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
        (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) y (Subtype.mk (p := fun (x : X) ↦ x ∈ T y) x hx)) ⊆
      s a
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
x_1 : 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)))
have refine_1 : ∀ (b : Y) (hb : y ∈ E b),
  ∃ (i : (y : Y) × ↥(T y)),
    (x, y) ∈
      U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
        E (i.fst (β := fun (y : Y) ↦ ↥(T y)))
Tactic: rcases iUnion_eq_univ_iff.1 hE y with ⟨b, hb⟩
-- 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
x_1 : X × Y
x : X
y b : Y
hb : y ∈ E b
⊢ ∃ (i : (y : Y) × ↥(T y)),
    (x, y) ∈
      U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
        E (i.fst (β := fun (y : Y) ↦ ↥(T y)))
have refine_1 : ∀ (a : X) (ha : a ∈ T b) (hx : x ∈ U a b),
  ∃ (i : (y : Y) × ↥(T y)),
    (x, y) ∈
      U (↑(i.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (i.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
        E (i.fst (β := fun (y : Y) ↦ ↥(T y)))
Tactic: rcases iUnion₂_eq_univ_iff.1 (hT b) x with ⟨a, ha, 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
x_1 : 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}
have refine_2 : ∀ (t : Set Y) (ht : t ∈ 𝓝 y) (htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}),
  ∃ t ∈ 𝓝 (x, y),
    Set.Finite (α := (y : Y) × ↥(T y))
      {i : (y : Y) × ↥(T y) |
        ((fun (z : (y : Y) × ↥(T y)) ↦
                U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                  E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
              i ∩
            t).Nonempty}
Tactic: rcases hEf y with ⟨t, ht, htf⟩
-- 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
x_1 : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 (x, y),
    Set.Finite (α := (y : Y) × ↥(T y))
      {i : (y : Y) × ↥(T y) |
        ((fun (z : (y : Y) × ↥(T y)) ↦
                U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                  E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
              i ∩
            t).Nonempty}
have refine_2 : Set.Finite (α := (y : Y) × ↥(T y))
  {i : (y : Y) × ↥(T y) |
    ((fun (z : (y : Y) × ↥(T y)) ↦
            U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
              E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
          i ∩
        SProd.sprod (α := Set X) univ t).Nonempty}
Tactic: refine ⟨univ ×ˢ t, prod_mem_nhds univ_mem ht, ?_⟩
-- 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
x_1 : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite.{w} (α := Y) {i : Y | (E i ∩ t).Nonempty}
⊢ Set.Finite (α := (y : Y) × ↥(T y))
    {i : (y : Y) × ↥(T y) |
      ((fun (z : (y : Y) × ↥(T y)) ↦
              U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
                E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
            i ∩
          SProd.sprod (α := Set X) univ t).Nonempty}
have refine_2 : Subset (α := Set ((y : Y) × ↥(T y)))
  {i : (y : Y) × ↥(T y) |
    ((fun (z : (y : Y) × ↥(T y)) ↦
            U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
              E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
          i ∩
        SProd.sprod (α := Set X) univ t).Nonempty}
  (⋃ (i : Y),
    ⋃ (_ : Membership.mem (γ := Set Y) {i : Y | (E i ∩ t).Nonempty} i), range (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) i))
Tactic: refine (htf.biUnion fun y _ ↦ finite_range (Sigma.mk y)).subset ?_
-- 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
x_1 : (y : Y) × ↥(T y)
y : Y
x : X
hx : x ∈ T y
⊢ ∃ (a : α),
    (fun (z : (y : Y) × ↥(T y)) ↦
          U (↑(z.snd (β := fun (y : Y) ↦ ↥(T y))) : X) (z.fst (β := fun (y : Y) ↦ ↥(T y))) ×ˢ
            E (z.fst (β := fun (y : Y) ↦ ↥(T y))))
        (Sigma.mk (β := fun (y : Y) ↦ ↥(T y)) y (Subtype.mk (p := fun (x : X) ↦ x ∈ T y) x hx)) ⊆
      s a
have 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
Tactic: refine ⟨a x y, (Set.prod_mono Subset.rfl ?_).trans (hUV x y)⟩
-- 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
⊢ ParacompactSpace X
have 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
Tactic: refine ⟨fun ι s ho hu ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (β : 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 : ∀ (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: rcases isCompact_univ.elim_finite_subcover _ ho hu.ge with ⟨T, hT⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
have refine : Eq.{v + 1} (α := Set X) (⋃ (b : (↑(↑T : Set ι) : Type v)), (fun (t : (↑(↑T : Set ι) : Type v)) ↦ s (↑t : ι)) b) univ
Tactic: refine ⟨(T : Set ι), fun t ↦ s t, fun t ↦ ho _, ?_, locallyFinite_of_finite _,
    fun t ↦ ⟨t, Subset.rfl⟩⟩
-- 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 : WeaklyLocallyCompactSpace X
inst_3 : SigmaCompactSpace X
inst_4 : T2Space X
⊢ ParacompactSpace X
have 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
Tactic: refine ⟨fun α s ho hc ↦ ?_⟩
-- 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 : 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
⊢ ∃ (β : 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 : ∀ (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
Tactic: choose i hi using iUnion_eq_univ_iff.1 hc
-- 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 : 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)
⊢ ∃ (β : 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 this : ∀ (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))
-- 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 : 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) (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 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: rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis this with
    ⟨β, c, t, hto, htc, htf⟩
-- 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 : 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 : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
have 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
Tactic: choose u v hu hv hxu htv huv using SetCoe.forall'.1 H
-- 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 : 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 : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
have 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
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⟩
-- 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 : 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
have refine : t ⊆ (closure[inst] (⋃ (i : (↑s : Type v)), u' i))ᶜ
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)⟩
-- 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 : 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
⊢ t ⊆ (closure[inst] (⋃ (i : (↑s : Type v)), u' i))ᶜ
have rw : ∀ (i : (↑s : Type v)), t ⊆ (closure[inst] (u' i))ᶜ
Tactic: rw [hu'fin.closure_iUnion, compl_iUnion, subset_iInter_iff]
-- 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 : 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))ᶜ
have refine : ∀ (i : (↑s : Type v)) (x : X) (hxt : x ∈ t) (hxu : x ∈ closure[inst] (u' i)), u' i ⊆ (v i)ᶜ
Tactic: refine fun i x hxt hxu ↦
      absurd (htv i hxt) (closure_minimal ?_ (isClosed_compl_iff.2 <| hv _) hxu)