awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
⊢ LocallyCompactSpace X
have this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
Tactic: have (x : X) : (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U)
      (fun s ↦ f ⁻¹' (s ∩ Z)) := by
    have H : U ∈ 𝓝 (f x) := hU.mem_nhds (hUZ.subset <| mem_range_self _).1
    rw [hf.nhds_eq_comap, ← comap_nhdsWithin_range, hUZ,
      nhdsWithin_inter_of_mem (nhdsWithin_le_nhds H)]
    exact (nhdsWithin_hasBasis ((compact_basis_nhds (f x)).restrict_subset H) _).comap _
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
⊢ LocallyCompactSpace X
have refine : ∀ (x : X) (s : Set Y),
  (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U → s ∈ 𝓝 (f x) → ∀ (hs : IsCompact s) (hsU : s ⊆ U), IsCompact (f ⁻¹' (s ∩ Z))
Tactic: refine .of_hasBasis this fun x s ⟨⟨_, hs⟩, hsU⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
h : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ IsCompact (f ⁻¹' (s ∩ Z))
have rw : IsCompact (s ∩ Z)
Tactic: rw [hf.isCompact_preimage_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
h : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
rw : IsCompact (s ∩ Z)
⊢ IsCompact (f ⁻¹' (s ∩ Z))
have rw₁ : s ∩ Z ⊆ range f
Tactic: rw [hf.isCompact_preimage_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyFinite (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hf : LocallyFinite f
hs : IsCompact s
⊢ Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}
have choose : ∀ (U : (x : X) → Set X) (hxU : ∀ (x : X), U x ∈ nhds x)
  (hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}),
  Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}
Tactic: choose U hxU hUf using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyFinite (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}
⊢ Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}
have rcases : ∀ (t : Finset X) (hsU : s ⊆ ⋃ x ∈ t, U x), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}
Tactic: rcases hs.elim_nhds_subcover U fun x _ => hxU x with ⟨t, -, hsU⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyFinite (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
⊢ Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}
have refine : Subset.{u_2} (α := Set ι) {i : ι | (f i ∩ s).Nonempty} (⋃ i ∈ (↑t : Set X), {i_1 : ι | (f i_1 ∩ U i).Nonempty})
Tactic: refine (t.finite_toSet.biUnion fun x _ => hUf x).subset ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyFinite (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
⊢ Membership.mem (γ := Set ι) (⋃ i ∈ (↑t : Set X), {i_1 : ι | (f i_1 ∩ U i).Nonempty}) i
have rcases : ∀ (c : X) (hct : c ∈ t) (hcx : x ∈ U c),
  Membership.mem (γ := Set ι) (⋃ i ∈ (↑t : Set X), {i_1 : ι | (f i_1 ∩ U i).Nonempty}) i
Tactic: rcases mem_iUnion₂.1 (hsU hx.2) with ⟨c, hct, hcx⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.NhdsKer (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsCompact (nhdsKer s) ↔ IsCompact s
have simp : (∀ {ι : Type u_1} (U : ι → Set X),
    (∀ (i : ι), IsOpen (U i)) → nhdsKer s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔
  ∀ {ι : Type u_1} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
Tactic: simp only [isCompact_iff_finite_subcover]
-- Lean 4 proof step from Mathlib.Topology.Compactness.NhdsKer (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (∀ {ι : Type u_1} (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) → nhdsKer s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔
    ∀ {ι : Type u_1} (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
have h : ∀ (ι : Type u_1) (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen (U i)),
  (nhdsKer s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔
    s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
Tactic: peel with ι U hUo
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ Eq.{v + 1} (α := Set X) (⋃ (a : (↑(range u) : Type v)), (fun (r : (↑(range u) : Type v)) ↦ (↑r : Set X)) a) univ
have rwa : Eq.{v + 1} (α := Set X) (⋃₀ range fun (r : (↑(range u) : Type v)) ↦ (↑r : Set X)) univ
Tactic: rwa [← sUnion_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ Eq.{v + 1} (α := Set X) (⋃ (a : (↑(range u) : Type v)), (fun (r : (↑(range u) : Type v)) ↦ (↑r : Set X)) a) univ
have rwa₁ : ⋃₀ range u = univ
Tactic: rwa [← sUnion_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (hypothesis)
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
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
have 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
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])
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (hypothesis)
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
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
have 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
Tactic: simp only [exists_subtype_range_iff, iUnion_eq_univ_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
have 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
Tactic: choose α t hto hXt htf ind hind using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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)
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
have 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
Tactic: choose t_inv ht_inv using hXt
Cleared hypotheses: hXt
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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)
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
have 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
Tactic: choose U hxU hU using htf
Cleared hypotheses: htf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
have refine_1 : ∀ (a : ι), IsOpen[inst] ((fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) a)
Tactic: refine ⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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)
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
have refine_2 : Eq.{v + 1} (α := Set X) (⋃ (i : ι), (fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) i) univ
Tactic: refine ⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
have refine_3 : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ ⋃ (a : α), ⋃ (_ : ind a = i), t a
Tactic: refine ⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ ∃ (v : ι → Set X),
    (∀ (a : ι), IsOpen[inst] (v a)) ∧
      Eq.{v + 1} (α := Set X) (⋃ (i : ι), v i) univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
have refine_4 : ∀ (a : ι), (fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) a ⊆ u a
Tactic: refine ⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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}
⊢ Eq.{v + 1} (α := Set X) (⋃ (i : ι), (fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) i) univ
have refine_2 : ∀ (x : X), ∃ (i : ι) (i_1 : α) (_ : ind i_1 = i), x ∈ t i_1
Tactic: simp only [eq_univ_iff_forall, mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
have 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}
Tactic: refine fun x ↦ ⟨U x, hxU x, ((hU x).image ind).subset ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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 : ι | ((fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) i ∩ U x).Nonempty} ⊆
    ind '' {i : α | (t i ∩ U x).Nonempty}
have 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}
Tactic: simp only [subset_def, mem_iUnion, mem_setOf_eq, Set.Nonempty, mem_inter_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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 : ι), (fun (i : ι) ↦ (⋃ (a : α), ⋃ (_ : ind a = i), t a : Set X)) a ⊆ u a
have refine_4 : ∀ (a : ι) (x : X), (∃ (i : α) (_ : ind i = a), x ∈ t i) → x ∈ u a
Tactic: simp only [subset_def, mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
have apply : Subset.{v} (α := Set X) univ (⋃ (i : Option ι), Option.elim' sᶜ u i)
Tactic: apply Subset.antisymm (subset_univ _)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
⊢ Subset.{v} (α := Set X) univ (⋃ (i : Option ι), Option.elim' sᶜ u i)
have simp_rw : sᶜ ∪ s ⊆ sᶜ ∪ ⋃ (a : ι), u a
Tactic: simp_rw [← compl_union_self s, Option.elim', iUnion_option]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (hypothesis)
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
⊢ ∃ (v : ι → Set X), (∀ (i : ι), IsOpen[inst] (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
have uc : 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
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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 : ι → Set X), (∀ (i : ι), IsOpen[inst] (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
have 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
Tactic: rcases precise_refinement (Option.elim' sᶜ u) (Option.forall.2 ⟨isOpen_compl_iff.2 hs, uo⟩)
      uc with
    ⟨v, vo, vc, vf, vu⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (goal)
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
have refine : s ⊆ ⋃ (i : ι), (v ∘ some) i
Tactic: refine ⟨v ∘ some, fun i ↦ vo _, ?_, vf.comp_injective (Option.some_injective _), fun i ↦ vu _⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (hypothesis)
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
⊢ s ⊆ ⋃ (i : ι), (v ∘ some) i
have vc₁ : (v none)ᶜ ⊆ ⋃ (i : ι), v (some i)
Tactic: simp only [iUnion_option, ← compl_subset_iff_union] at vc
Cleared hypotheses: vc
-- Lean 4 proof step from Mathlib.Topology.Compactness.Paracompact (hypothesis)
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
⊢ ∃ (β : 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), ∃ (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)