awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : T2Space X
inst_3 : ParacompactSpace X
⊢ T4Space X
have this : ∀ (s t : Set X),
  IsClosed[inst] s →
    (∀ 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
Tactic: have : ∀ s t : Set X, IsClosed s →
      (∀ x ∈ s, ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v := fun s t hs H ↦ by
    /- For each `x ∈ s` we choose open disjoint `u x ∋ x` and `v x ⊇ t`. The sets `u x` form an
        open covering of `s`. We choose a locally finite refinement `u' : s → Set X`, then
        `⋃ i, u' i` and `(closure (⋃ i, u' i))ᶜ` are disjoint open neighborhoods of `s` and `t`. -/
    choose u v hu hv hxu htv huv using SetCoe.forall'.1 H
    rcases precise_refinement_set hs u hu fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, hxu _⟩ with
      ⟨u', hu'o, hcov', hu'fin, hsub⟩
    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)⟩
    rw [hu'fin.closure_iUnion, compl_iUnion, subset_iInter_iff]
    refine fun i x hxt hxu ↦
      absurd (htv i hxt) (closure_minimal ?_ (isClosed_compl_iff.2 <| hv _) hxu)
    exact fun y hyu hyv ↦ (huv i).le_bot ⟨hsub _ hyu, 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 : T2Space X
inst_3 : ParacompactSpace X
this :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      (∀ 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
⊢ T4Space X
have refine : ∀ (s t : Set X) (hs : IsClosed[inst] s) (ht : IsClosed[inst] t) (hst : Disjoint s t) (x : X) (hx : x ∈ s),
  ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
Tactic: refine { normal := fun s t hs ht hst ↦ this s t hs fun 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 : T2Space X
inst_3 : ParacompactSpace X
this :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      (∀ 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
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
x : X
hx : x ∈ s
y : X
hy : y ∈ t
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ y ∈ u ∧ {x} ⊆ v ∧ Disjoint u v
have simp_rw : ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ y ∈ u ∧ x ∈ v ∧ Disjoint u v
Tactic: simp_rw [singleton_subset_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
this :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      (∀ 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
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
x : X
hx : x ∈ s
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
have rcases : ∀ (v u : Set X) (hv : IsOpen[inst] v) (hu : IsOpen[inst] u) (htv : t ⊆ v) (hxu : {x} ⊆ u) (huv : Disjoint v u),
  ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
Tactic: rcases this t {x} ht fun y hy ↦ (by
    simp_rw [singleton_subset_iff]
    exact t2_separation (hst.symm.ne_of_mem hy hx))
    with ⟨v, u, hv, hu, htv, hxu, huv⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
have inl : IsEmpty ι → IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
Tactic: rcases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
inl : IsEmpty ι → IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
have inr : Nonempty ι → IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
Tactic: rcases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h : Nonempty ι
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
have inr : ∀ (f : ℕ → ι) (hf : Function.Surjective f), IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
Tactic: obtain ⟨f, hf⟩ := countable_iff_exists_surjective.mp hι
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
⊢ IsSigmaCompact (⋃₀ S)
have this : Countable.{u_1 + 1} (↑S : Type u_1)
Tactic: have : Countable S := countable_coe_iff.mpr hc
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
this : Countable.{u_1 + 1} (↑S : Type u_1)
⊢ IsSigmaCompact (⋃₀ S)
have rw : IsSigmaCompact.{u_1} (X := X) (⋃ (i : (↑S : Type u_1)), (↑i : Set X))
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsSigmaCompact (s i)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
have choose : ∀ (K : (i : ι) → ℕ → Set X) (hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)) (hcov : ∀ (i : ι), ⋃ (n : ℕ), K i n = s i),
  IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
Tactic: choose K hcomp hcov using fun i ↦ hcomp i
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : Countable ι
s : ι → Set X
hcomp_1 : ∀ (i : ι), IsSigmaCompact (s i)
K : (i : ι) → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ (n : ℕ), K i n = s i
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), ⋃ (n : ℕ), K i n) (⋃ (i : ι), ⋃ (n : ℕ), Function.uncurry K (i, n))
have rw : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), ⋃ (n : ℕ), K i n) (⋃ (i : ι), ⋃ (n : ℕ), (fun (p : ι × ℕ) ↦ K p.1 p.2) (i, n))
Tactic: rw [Function.uncurry_def]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : Countable ι
s : ι → Set X
hcomp_1 : ∀ (i : ι), IsSigmaCompact (s i)
K : (i : ι) → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ (n : ℕ), K i n = s i
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), ⋃ (n : ℕ), Function.uncurry K (i, n)) (⋃ (x : ι × ℕ), Function.uncurry K x)
have rw : Eq.{u_1 + 1} (α := Set X) (⋃ (x : ι × ℕ), Function.uncurry K x) (⋃ (x : ι × ℕ), Function.uncurry K x)
Tactic: rw [← iUnion_prod']
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (hypothesis)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : Countable ι
s : ι → Set X
hcomp_1 : ∀ (i : ι), IsSigmaCompact (s i)
K : (i : ι) → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ (n : ℕ), K i n = s i
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
have this : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), s i) (⋃ (x : ι × ℕ), Function.uncurry K x)
Tactic: have := calc
    ⋃ i, s i
    _ = ⋃ i, ⋃ n, (K i n) := by simp_rw [hcov]
    _ = ⋃ (i) (n : ℕ), (K.uncurry ⟨i, n⟩) := by rw [Function.uncurry_def]
    _ = ⋃ x, K.uncurry x := by rw [← iUnion_prod']
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : Countable ι
s : ι → Set X
hcomp_1 : ∀ (i : ι), IsSigmaCompact (s i)
K : (i : ι) → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ (n : ℕ), K i n = s i
this : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), s i) (⋃ (x : ι × ℕ), Function.uncurry K x)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
have rw : IsSigmaCompact.{u_1} (X := X) (⋃ (x : ι × ℕ), Function.uncurry K x)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ (s : (↑S : Type u_1)), IsSigmaCompact (↑s : Set X)
⊢ IsSigmaCompact (⋃₀ S)
have this : Countable.{u_1 + 1} (↑S : Type u_1)
Tactic: have : Countable S := countable_coe_iff.mpr hc
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (hypothesis)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ i ∈ s, S i)
have this : Countable.{u_3 + 1} (↑s : Type u_3)
Tactic: have : Countable ↑s := countable_coe_iff.mpr hc
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable.{u_3 + 1} (↑s : Type u_3)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ i ∈ s, S i)
have rw : IsSigmaCompact.{u_1} (X := X) (⋃ (x : (↑s : Type u_3)), S (↑x : ι))
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
ht : IsSigmaCompact t
hs : IsClosed[inst] s
h : s ⊆ t
⊢ IsSigmaCompact s
have rcases : ∀ (K : ℕ → Set X) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hcov : ⋃ (n : ℕ), K n = t), IsSigmaCompact s
Tactic: rcases ht with ⟨K, hcompact, hcov⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsClosed[inst] s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ (n : ℕ), K n = t
⊢ IsSigmaCompact s
have refine : ⋃ (n : ℕ), (fun (n : ℕ) ↦ s ∩ K n) n = s
Tactic: refine ⟨(fun n ↦ s ∩ (K n)), fun n ↦ (hcompact n).inter_left hs, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsClosed[inst] s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ (n : ℕ), K n = t
⊢ ⋃ (n : ℕ), (fun (n : ℕ) ↦ s ∩ K n) n = s
have rw : s ∩ t = s
Tactic: rw [← inter_iUnion, hcov]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsSigmaCompact s
hf : ContinuousOn f s
⊢ IsSigmaCompact (f '' s)
have rcases : ∀ (K : ℕ → Set X) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hcov : ⋃ (n : ℕ), K n = s), IsSigmaCompact (f '' s)
Tactic: rcases hs with ⟨K, hcompact, hcov⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : ContinuousOn f s
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ (n : ℕ), K n = s
⊢ IsSigmaCompact (f '' s)
have refine : ∀ (n : ℕ), IsCompact.{u_2} (X := Y) ((fun (n : ℕ) ↦ f '' K n) n)
Tactic: refine ⟨fun n ↦ f '' K n, ?_, hcov.symm ▸ image_iUnion.symm⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s ↔ IsSigmaCompact (f '' s)
have mp : IsSigmaCompact s → IsSigmaCompact (f '' s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
mp : IsSigmaCompact s → IsSigmaCompact (f '' s)
⊢ IsSigmaCompact s ↔ IsSigmaCompact (f '' s)
have mpr : IsSigmaCompact (f '' s) → IsSigmaCompact s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
⊢ IsSigmaCompact s
have mpr : ∀ (n : ℕ), IsCompact.{u_1} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n)
Tactic: refine ⟨fun n ↦ f ⁻¹' (L n) ∩ s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
mpr : ∀ (n : ℕ), IsCompact.{u_1} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n)
⊢ IsSigmaCompact s
have mpr₁ : ⋃ (n : ℕ), (fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n = s
Tactic: refine ⟨fun n ↦ f ⁻¹' (L n) ∩ s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
n : ℕ
⊢ f '' (f ⁻¹' L n ∩ s) = L n
have rw : L n ⊆ f '' s
Tactic: rw [image_preimage_inter, inter_eq_left.mpr]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
n : ℕ
⊢ IsCompact.{u_1} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n)
have this : f '' (f ⁻¹' L n ∩ s) = L n
Tactic: have : f '' (f ⁻¹' (L n) ∩ s) = L n := by
        rw [image_preimage_inter, inter_eq_left.mpr]
        exact (subset_iUnion _ n).trans hcov.le
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
⊢ ⋃ (n : ℕ), f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s
have rw : ⋃ (n : ℕ), f ⁻¹' L n ∩ s = (⋃ (i : ℕ), f ⁻¹' L i) ∩ s
Tactic: rw [preimage_iUnion, iUnion_inter]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
rw : ⋃ (n : ℕ), f ⁻¹' L n ∩ s = (⋃ (i : ℕ), f ⁻¹' L i) ∩ s
⊢ ⋃ (n : ℕ), f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s
have rw₁ : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), f ⁻¹' L n ∩ s) (⋃ (i : ℕ), f ⁻¹' L i ∩ s)
Tactic: rw [preimage_iUnion, iUnion_inter]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
⊢ (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s = f ⁻¹' f '' s ∩ s
have rw : f ⁻¹' f '' s ∩ s = f ⁻¹' f '' s ∩ s
Tactic: rw [hcov]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
⊢ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n = s
have calc : ⋃ (n : ℕ), f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s
Tactic: calc ⋃ n, f ⁻¹' L n ∩ s
        _ = f ⁻¹' (⋃ n, L n) ∩ s := by rw [preimage_iUnion, iUnion_inter]
        _ = f ⁻¹' (f '' s) ∩ s := by rw [hcov]
        _ = s := inter_eq_right.mpr (subset_preimage_image _ _)
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
calc : ⋃ (n : ℕ), f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s
⊢ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n = s
have calc₁ : (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s = f ⁻¹' f '' s ∩ s
Tactic: calc ⋃ n, f ⁻¹' L n ∩ s
        _ = f ⁻¹' (⋃ n, L n) ∩ s := by rw [preimage_iUnion, iUnion_inter]
        _ = f ⁻¹' (f '' s) ∩ s := by rw [hcov]
        _ = s := inter_eq_right.mpr (subset_preimage_image _ _)
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ SigmaCompactSpace X ↔
    ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ
have rw : IsSigmaCompact.{u_1} (X := X) univ ↔
  ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ
Tactic: rw [← isSigmaCompact_univ_iff, IsSigmaCompact]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
rw :
  IsSigmaCompact.{u_1} (X := X) univ ↔
    ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ
⊢ SigmaCompactSpace X ↔
    ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ
have rw₁ : (∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ) ↔
  ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ
Tactic: rw [← isSigmaCompact_univ_iff, IsSigmaCompact]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsSigmaCompact s ↔ IsSigmaCompact.{u_1} (X := (↑s : Type u_1)) univ
have rw : IsSigmaCompact s ↔
  IsSigmaCompact.{u_1} (X := X) (image (α := { a : X // a ∈ s }) (Subtype.val (p := fun (a : X) ↦ a ∈ s)) univ)
Tactic: rw [Subtype.isSigmaCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw :
  IsSigmaCompact s ↔
    IsSigmaCompact.{u_1} (X := X) (image (α := { a : X // a ∈ s }) (Subtype.val (p := fun (a : X) ↦ a ∈ s)) univ)
⊢ IsSigmaCompact s ↔ IsSigmaCompact.{u_1} (X := (↑s : Type u_1)) univ
have rw₁ : IsSigmaCompact s ↔
  IsSigmaCompact.{u_1} (X := X) (range (ι := { a : X // a ∈ s }) (Subtype.val (p := fun (a : X) ↦ a ∈ s)))
Tactic: rw [Subtype.isSigmaCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw :
  IsSigmaCompact s ↔
    IsSigmaCompact.{u_1} (X := X) (image (α := { a : X // a ∈ s }) (Subtype.val (p := fun (a : X) ↦ a ∈ s)) univ)
rw₁ :
  IsSigmaCompact s ↔
    IsSigmaCompact.{u_1} (X := X) (range (ι := { a : X // a ∈ s }) (Subtype.val (p := fun (a : X) ↦ a ∈ s)))
⊢ IsSigmaCompact s ↔ IsSigmaCompact.{u_1} (X := (↑s : Type u_1)) univ
have rw₂ : IsSigmaCompact s ↔ IsSigmaCompact s
Tactic: rw [Subtype.isSigmaCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : LocallyCompactSpace X
inst_3 : SecondCountableTopology X
⊢ SigmaCompactSpace X
have choose : ∀ (K : (x : X) → Set X) (hKc : ∀ (x : X), IsCompact (K x)) (hxK : ∀ (x : X), K x ∈ 𝓝 x), SigmaCompactSpace X
Tactic: choose K hKc hxK using fun x : X => exists_compact_mem_nhds x
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : LocallyCompactSpace X
inst_3 : SecondCountableTopology X
K : (x : X) → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
⊢ SigmaCompactSpace X
have rcases : ∀ (s : Set X) (hsc : s.Countable) (hsU : Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, K x) univ), SigmaCompactSpace X
Tactic: rcases countable_cover_nhds hxK with ⟨s, hsc, hsU⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : LocallyCompactSpace X
inst_3 : SecondCountableTopology X
K : (x : X) → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
s : Set X
hsc : s.Countable
hsU : Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, K x) univ
⊢ SigmaCompactSpace X
have refine : ⋃₀ (K '' s) = univ
Tactic: refine SigmaCompactSpace.of_countable _ (hsc.image K) (forall_mem_image.2 fun x _ => hKc x) ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), compactCovering X n) univ
have rw : Eq.{u_1 + 1} (α := Set X)
  (⋃ (x : ℕ),
    Exists.choose (p := fun (K : ℕ → Set X) ↦
      (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ) sorry x)
  univ
Tactic: rw [compactCovering, iUnion_accumulate]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Finite ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
⊢ SigmaCompactSpace ((i : ι) → X i)
have refine : Eq (α := Set ((i : ι) → X i))
  (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := X) univ fun (i : ι) ↦ compactCovering (X i) n : Set ((i : ι) → X i))) n) univ
Tactic: refine ⟨⟨fun n => Set.pi univ fun i => compactCovering (X i) n,
    fun n => isCompact_univ_pi fun i => isCompact_compactCovering (X i) _, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Finite ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
⊢ Eq (α := Set ((i : ι) → X i))
    (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := X) univ fun (i : ι) ↦ compactCovering (X i) n : Set ((i : ι) → X i))) n)
    univ
have rw : Eq (α := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ ⋃ (j : ℕ), compactCovering (X i) j) univ
Tactic: rw [iUnion_univ_pi_of_monotone]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Finite ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
rw : Eq (α := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ ⋃ (j : ℕ), compactCovering (X i) j) univ
⊢ Eq (α := Set ((i : ι) → X i))
    (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := X) univ fun (i : ι) ↦ compactCovering (X i) n : Set ((i : ι) → X i))) n)
    univ
have rw₁ : ∀ (i : ι), Monotone.{0, u_4} (β := Set (X i)) (compactCovering (X i))
Tactic: rw [iUnion_univ_pi_of_monotone]