awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Paracompact
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_1 : ∀ (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)
x : X
hxt : x ∈ t
hxu : x ∈ closure[inst] (u' i)
⊢ u' i ⊆ (v i)ᶜ

Tactic:
exact fun y hyu hyv ↦ (huv i).le_bot ⟨hsub _ hyu, hyv⟩

Premises used: Disjoint.le_bot, And.intro
-- Module: Mathlib.Topology.Compactness.Paracompact
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),
    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⟩
-- Module: Mathlib.Topology.Compactness.Paracompact
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

Tactic:
{ normal := fun s t hs ht hst ↦ this s t hs fun x hx ↦ ?_ }

Premises used: T4Space.mk
-- Module: Mathlib.Topology.Compactness.Paracompact
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
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
⊢ T4Space X

Tactic:
refine { normal := fun s t hs ht hst ↦ this s t hs fun x hx ↦ ?_ }
-- Module: Mathlib.Topology.Compactness.Paracompact
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
simp_rw : ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ y ∈ u ∧ x ∈ v ∧ Disjoint u v
⊢ ∃ (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]

Premises used: Set.singleton_subset_iff
-- Module: Mathlib.Topology.Compactness.Paracompact
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

Tactic:
t2_separation (hst.symm.ne_of_mem hy hx)

Premises used: Disjoint.symm, Disjoint.ne_of_mem, t2_separation
-- Module: Mathlib.Topology.Compactness.Paracompact
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

Tactic:
exact t2_separation (hst.symm.ne_of_mem hy hx)

Premises used: Disjoint.symm, Disjoint.ne_of_mem, t2_separation
-- Module: Mathlib.Topology.Compactness.Paracompact
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
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
⊢ ∃ (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⟩

Premises used: Singleton.singleton
-- Module: Mathlib.Topology.Compactness.Paracompact
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
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:
⟨u, v, hu, hv, singleton_subset_iff.1 hxu, htv, huv.symm⟩

Premises used: Set.singleton_subset_iff, Disjoint.symm, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Compactness.Paracompact
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
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:
exact ⟨u, v, hu, hv, singleton_subset_iff.1 hxu, htv, huv.symm⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
⊢ IsSigmaCompact s

Tactic:
⟨fun _ => s, fun _ => hs, iUnion_const _⟩

Premises used: IsSigmaCompact, Set.iUnion_const, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsSigmaCompact.{u_1} (X := X) ∅

Tactic:
IsCompact.isSigmaCompact isCompact_empty

Premises used: IsCompact.isSigmaCompact, isCompact_empty
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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)
inr : Nonempty ι → IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
rcases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h : IsEmpty ι
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
simp only [iUnion_of_empty, isSigmaCompact_empty]

Premises used: Set.iUnion_of_empty, isSigmaCompact_empty
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h : Nonempty ι
inr : ∀ (f : ℕ → ι) (hf : Function.Surjective f), IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
obtain ⟨f, hf⟩ := countable_iff_exists_surjective.mp hι

Premises used: countable_iff_exists_surjective, Iff.mp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
⟨s ∘ f, fun n ↦ hcomp (f n), Function.Surjective.iUnion_comp hf _⟩

Premises used: IsSigmaCompact, Function.comp, And.intro, Exists.intro, Function.Surjective.iUnion_comp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
exact ⟨s ∘ f, fun n ↦ hcomp (f n), Function.Surjective.iUnion_comp hf _⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
⊢ Countable.{u_1 + 1} (↑S : Type u_1)

Tactic:
have : Countable S := countable_coe_iff.mpr hc
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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)
rw : IsSigmaCompact.{u_1} (X := X) (⋃ (i : (↑S : Type u_1)), (↑i : Set X))
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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.{u_1} (X := X) (⋃ (i : (↑S : Type u_1)), (↑i : Set X))

Tactic:
apply isSigmaCompact_iUnion_of_isCompact _ (fun ⟨s, hs⟩ ↦ hcomp s hs)

Premises used: isSigmaCompact_iUnion_of_isCompact
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsSigmaCompact (s i)
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)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
choose K hcomp hcov using fun i ↦ hcomp i
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : ι), s i) (⋃ (i : ι), ⋃ (n : ℕ), K i n)

Tactic:
simp_rw [hcov]
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
rw rw₁ :
  Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), ⋃ (n : ℕ), K i n) (⋃ (i : ι), ⋃ (n : ℕ), (fun (p : ι × ℕ) ↦ K p.1 p.2) (i, n))
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), ⋃ (n : ℕ), K i n) (⋃ (i : ι), ⋃ (n : ℕ), Function.uncurry K (i, n))

Tactic:
rw [Function.uncurry_def]

Premises used: Function.uncurry_def
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
rw rw₁ : Eq.{u_1 + 1} (α := Set X) (⋃ (x : ι × ℕ), Function.uncurry K x) (⋃ (x : ι × ℕ), Function.uncurry K x)
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), ⋃ (n : ℕ), Function.uncurry K (i, n)) (⋃ (x : ι × ℕ), Function.uncurry K x)

Tactic:
rw [← iUnion_prod']

Premises used: Set.iUnion_prod'
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : ι), 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']
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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)
rw : IsSigmaCompact.{u_1} (X := X) (⋃ (x : ι × ℕ), Function.uncurry K x)
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ (i : ι), s i)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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) (⋃ (x : ι × ℕ), Function.uncurry K x)

Tactic:
isSigmaCompact_iUnion_of_isCompact K.uncurry fun x ↦ (hcomp x.1 x.2)

Premises used: isSigmaCompact_iUnion_of_isCompact, Prod.fst, Function.uncurry, Prod.snd
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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) (⋃ (x : ι × ℕ), Function.uncurry K x)

Tactic:
exact isSigmaCompact_iUnion_of_isCompact K.uncurry fun x ↦ (hcomp x.1 x.2)

Premises used: isSigmaCompact_iUnion_of_isCompact, Prod.fst, Function.uncurry, Prod.snd
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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)
⊢ Countable.{u_1 + 1} (↑S : Type u_1)

Tactic:
have : Countable S := countable_coe_iff.mpr hc
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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)
this : Countable.{u_1 + 1} (↑S : Type u_1)
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
apply sUnion_eq_iUnion.symm ▸ isSigmaCompact_iUnion _ hcomp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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)
⊢ Countable.{u_3 + 1} (↑s : Type u_3)

Tactic:
have : Countable ↑s := countable_coe_iff.mpr hc
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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)
rw : IsSigmaCompact.{u_1} (X := X) (⋃ (x : (↑s : Type u_3)), S (↑x : ι))
⊢ IsSigmaCompact.{u_1} (X := X) (⋃ i ∈ s, S i)

Tactic:
rw [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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) (⋃ (x : (↑s : Type u_3)), S (↑x : ι))

Tactic:
isSigmaCompact_iUnion _ (fun ⟨i', hi'⟩ ↦ hcomp i' hi')

Premises used: IsSigmaCompact, isSigmaCompact_iUnion, _private.0.isSigmaCompact_biUnion.match_1, Subtype.val
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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) (⋃ (x : (↑s : Type u_3)), S (↑x : ι))

Tactic:
exact isSigmaCompact_iUnion _ (fun ⟨i', hi'⟩ ↦ hcomp i' hi')

Premises used: isSigmaCompact_iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
ht : IsSigmaCompact t
hs : IsClosed[inst] s
h : s ⊆ t
rcases : ∀ (K : ℕ → Set X) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hcov : ⋃ (n : ℕ), K n = t), IsSigmaCompact s
⊢ IsSigmaCompact s

Tactic:
rcases ht with ⟨K, hcompact, hcov⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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

Tactic:
⟨(fun n ↦ s ∩ (K n)), fun n ↦ (hcompact n).inter_left hs, ?_⟩

Premises used: IsCompact.inter_left, IsSigmaCompact, Inter.inter, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
refine : ⋃ (n : ℕ), (fun (n : ℕ) ↦ s ∩ K n) n = s
⊢ IsSigmaCompact s

Tactic:
refine ⟨(fun n ↦ s ∩ (K n)), fun n ↦ (hcompact n).inter_left hs, ?_⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
rw : s ∩ t = s
⊢ ⋃ (n : ℕ), (fun (n : ℕ) ↦ s ∩ K n) n = s

Tactic:
rw [← inter_iUnion, hcov]

Premises used: Set.inter_iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
⊢ s ∩ t = s

Tactic:
inter_eq_left.mpr h

Premises used: Set.inter_eq_left, Iff.mpr
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
⊢ s ∩ t = s

Tactic:
exact inter_eq_left.mpr h

Premises used: Set.inter_eq_left, Iff.mpr
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
rcases : ∀ (K : ℕ → Set X) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hcov : ⋃ (n : ℕ), K n = s), IsSigmaCompact (f '' s)
⊢ IsSigmaCompact (f '' s)

Tactic:
rcases hs with ⟨K, hcompact, hcov⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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)

Tactic:
⟨fun n ↦ f '' K n, ?_, hcov.symm ▸ image_iUnion.symm⟩

Premises used: IsSigmaCompact, Eq.rec, Set.image_iUnion, And.intro, Exists.intro, Set.image, Eq.symm
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
refine : ∀ (n : ℕ), IsCompact.{u_2} (X := Y) ((fun (n : ℕ) ↦ f '' K n) n)
⊢ IsSigmaCompact (f '' s)

Tactic:
refine ⟨fun n ↦ f '' K n, ?_, hcov.symm ▸ image_iUnion.symm⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
⊢ ∀ (n : ℕ), IsCompact.{u_2} (X := Y) ((fun (n : ℕ) ↦ f '' K n) n)

Tactic:
fun n ↦ (hcompact n).image_of_continuousOn (hf.mono (hcov.symm ▸ subset_iUnion K n))

Premises used: Eq.rec, Set.subset_iUnion, IsCompact.image_of_continuousOn, ContinuousOn.mono, Eq.symm
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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
⊢ ∀ (n : ℕ), IsCompact.{u_2} (X := Y) ((fun (n : ℕ) ↦ f '' K n) n)

Tactic:
exact fun n ↦ (hcompact n).image_of_continuousOn (hf.mono (hcov.symm ▸ subset_iUnion K n))

Premises used: Eq.rec, Set.subset_iUnion, IsCompact.image_of_continuousOn, ContinuousOn.mono, Eq.symm
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
s : Set X
hs : IsSigmaCompact s
⊢ IsSigmaCompact (f '' s)

Tactic:
hs.image_of_continuousOn hf.continuousOn

Premises used: Continuous.continuousOn, IsSigmaCompact.image_of_continuousOn
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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)
mpr : IsSigmaCompact (f '' s) → IsSigmaCompact s
⊢ IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Tactic:
constructor