awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
n : ℕ
inr :
  ∀ (k : ℕ),
    Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ n} k →
      IsCompact (X := (i : ι) × X i) (Sigma.mk (β := fun (i : ι) ↦ X i) (f k) '' compactCovering (X (f k)) n)
⊢ IsCompact (X := (i : ι) × X i)
    ((fun (n : ℕ) ↦
        (⋃ (k : ℕ), ⋃ (_ : k ≤ n), Sigma.mk (β := fun (i : ι) ↦ X i) (f k) '' compactCovering (X (f k)) n :
          Set ((i : ι) × X i)))
      n)

Tactic:
refine (finite_le_nat _).isCompact_biUnion fun k _ => ?_

Premises used: Set.Finite.isCompact_biUnion, Set.finite_le_nat
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
n k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ n} k
⊢ IsCompact (X := (i : ι) × X i) (Sigma.mk (β := fun (i : ι) ↦ X i) (f k) '' compactCovering (X (f k)) n)

Tactic:
(isCompact_compactCovering _ _).image continuous_sigmaMk

Premises used: continuous_sigmaMk, isCompact_compactCovering, IsCompact.image
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
n k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ n} k
⊢ IsCompact (X := (i : ι) × X i) (Sigma.mk (β := fun (i : ι) ↦ X i) (f k) '' compactCovering (X (f k)) n)

Tactic:
exact (isCompact_compactCovering _ _).image continuous_sigmaMk

Premises used: continuous_sigmaMk, isCompact_compactCovering, IsCompact.image
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
inr :
  ∀ (x : ℕ) (b : X (f x)),
    ∃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i),
      Membership.mem (γ := Set ((i : ι) × X i))
        (Sigma.mk (β := fun (i : ι) ↦ X i) (f i_1) '' compactCovering (X (f i_1)) i)
        (Sigma.mk (β := fun (a : ι) ↦ X a) (f x) b)
⊢ Eq (α := Set ((i : ι) × X i))
    (⋃ (n : ℕ),
      (fun (n : ℕ) ↦
          (⋃ (k : ℕ), ⋃ (_ : k ≤ n), Sigma.mk (β := fun (i : ι) ↦ X i) (f k) '' compactCovering (X (f k)) n :
            Set ((i : ι) × X i)))
        n)
    univ

Tactic:
simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion, hf.forall]

Premises used: Function.Surjective.forall, Set.iUnion_eq_univ_iff, Set.mem_iUnion, Sigma.forall
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
k : ℕ
y : X (f k)
inr :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Set (X (f k))) (compactCovering (X (f k)) n) y),
    ∃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i),
      Membership.mem (γ := Set ((i : ι) × X i))
        (Sigma.mk (β := fun (i : ι) ↦ X i) (f i_1) '' compactCovering (X (f i_1)) i)
        (Sigma.mk (β := fun (a : ι) ↦ X a) (f k) y)
⊢ ∃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i),
    Membership.mem (γ := Set ((i : ι) × X i))
      (Sigma.mk (β := fun (i : ι) ↦ X i) (f i_1) '' compactCovering (X (f i_1)) i)
      (Sigma.mk (β := fun (a : ι) ↦ X a) (f k) y)

Tactic:
rcases exists_mem_compactCovering y with ⟨n, hn⟩

Premises used: exists_mem_compactCovering
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
k : ℕ
y : X (f k)
n : ℕ
hn : Membership.mem (γ := Set (X (f k))) (compactCovering (X (f k)) n) y
⊢ ∃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i),
    Membership.mem (γ := Set ((i : ι) × X i))
      (Sigma.mk (β := fun (i : ι) ↦ X i) (f i_1) '' compactCovering (X (f i_1)) i)
      (Sigma.mk (β := fun (a : ι) ↦ X a) (f k) y)

Tactic:
⟨max k n, k, le_max_left _ _, mem_image_of_mem _ ?_⟩

Premises used: Max.max, Set.mem_image_of_mem, Exists.intro, le_max_left
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
k : ℕ
y : X (f k)
n : ℕ
hn : Membership.mem (γ := Set (X (f k))) (compactCovering (X (f k)) n) y
inr : Membership.mem (γ := Set (X (f k))) (compactCovering (X (f k)) (max k n)) y
⊢ ∃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i),
    Membership.mem (γ := Set ((i : ι) × X i))
      (Sigma.mk (β := fun (i : ι) ↦ X i) (f i_1) '' compactCovering (X (f i_1)) i)
      (Sigma.mk (β := fun (a : ι) ↦ X a) (f k) y)

Tactic:
refine ⟨max k n, k, le_max_left _ _, mem_image_of_mem _ ?_⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
k : ℕ
y : X (f k)
n : ℕ
hn : Membership.mem (γ := Set (X (f k))) (compactCovering (X (f k)) n) y
⊢ Membership.mem (γ := Set (X (f k))) (compactCovering (X (f k)) (max k n)) y

Tactic:
compactCovering_subset _ (le_max_right _ _) hn

Premises used: le_max_right, Set.Mem, compactCovering_subset
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
k : ℕ
y : X (f k)
n : ℕ
hn : Membership.mem (γ := Set (X (f k))) (compactCovering (X (f k)) n) y
⊢ Membership.mem (γ := Set (X (f k))) (compactCovering (X (f k)) (max k n)) y

Tactic:
exact compactCovering_subset _ (le_max_right _ _) hn

Premises used: le_max_right, compactCovering_subset
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
rw : e ⁻¹' ⋃ (i : ℕ), compactCovering X i = univ
rw₁ : e ⁻¹' univ = univ
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set Y) univ univ
⊢ Eq.{u_2 + 1} (α := Set Y) (⋃ (n : ℕ), (fun (n : ℕ) ↦ e ⁻¹' compactCovering X n) n) univ

Tactic:
rw [← preimage_iUnion, iUnion_compactCovering, preimage_univ]

Premises used: iUnion_compactCovering, Set.preimage_univ, Set.preimage_iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
s : Set X
hs : IsClosed[inst] s
⊢ SigmaCompactSpace.{u_1} (↑s : Type u_1)

Tactic:
hs.isClosedEmbedding_subtypeVal.sigmaCompactSpace

Premises used: IsClosed.isClosedEmbedding_subtypeVal, Topology.IsClosedEmbedding.sigmaCompactSpace
-- Module: Mathlib.Topology.Compactness.SigmaCompact
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 : SigmaCompactSpace X
inst_3 : SigmaCompactSpace Y
⊢ SigmaCompactSpace (ULift.{u, u_2} Y)

Tactic:
IsClosedEmbedding.uliftDown.sigmaCompactSpace

Premises used: Topology.IsClosedEmbedding.sigmaCompactSpace, Topology.IsClosedEmbedding.uliftDown
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
⊢ ∀ (n : ℕ), Set.Finite.{u_3} (α := ι) {i : ι | (f i ∩ compactCovering X n).Nonempty}

Tactic:
have := fun n => hf.finite_nonempty_inter_compact (isCompact_compactCovering X n)
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), Set.Finite.{u_3} (α := ι) {i : ι | (f i ∩ compactCovering X n).Nonempty}
⊢ Set.Countable.{u_3} (α := ι) univ

Tactic:
(countable_iUnion fun n => (this n).countable).mono fun i _ => ?_

Premises used: Set.countable_iUnion, Set.Countable.mono, Set.Finite.countable
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), Set.Finite.{u_3} (α := ι) {i : ι | (f i ∩ compactCovering X n).Nonempty}
refine :
  ∀ (i : ι),
    Membership.mem (γ := Set ι) univ i →
      Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i
⊢ Set.Countable.{u_3} (α := ι) univ

Tactic:
refine (countable_iUnion fun n => (this n).countable).mono fun i _ => ?_

Premises used: Set.countable_iUnion, Set.Countable.mono, Set.Finite.countable
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), Set.Finite.{u_3} (α := ι) {i : ι | (f i ∩ compactCovering X n).Nonempty}
i : ι
h : Membership.mem (γ := Set ι) univ i
rcases :
  ∀ (x : X) (hx : x ∈ f i),
    Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i
⊢ Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i

Tactic:
rcases hne i with ⟨x, hx⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), Set.Finite.{u_3} (α := ι) {i : ι | (f i ∩ compactCovering X n).Nonempty}
i : ι
h : Membership.mem (γ := Set ι) univ i
x : X
hx : x ∈ f i
rcases :
  ∀ (n : ℕ) (hn : x ∈ compactCovering X n),
    Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i
⊢ Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i

Tactic:
rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering X) x with ⟨n, hn⟩

Premises used: Set.iUnion_eq_univ_iff, iUnion_compactCovering, Iff.mp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), Set.Finite.{u_3} (α := ι) {i : ι | (f i ∩ compactCovering X n).Nonempty}
i : ι
h : Membership.mem (γ := Set ι) univ i
x : X
hx : x ∈ f i
n : ℕ
hn : x ∈ compactCovering X n
⊢ Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i

Tactic:
mem_iUnion.2 ⟨n, x, hx, hn⟩

Premises used: Iff.mpr, Set.mem_iUnion, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
this : ∀ (n : ℕ), Set.Finite.{u_3} (α := ι) {i : ι | (f i ∩ compactCovering X n).Nonempty}
i : ι
h : Membership.mem (γ := Set ι) univ i
x : X
hx : x ∈ f i
n : ℕ
hn : x ∈ compactCovering X n
⊢ Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i

Tactic:
exact mem_iUnion.2 ⟨n, x, hx, hn⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst] s
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∀ x ∈ s, {x_1 : X | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x

Tactic:
simp only [nhdsWithin, mem_inf_principal] at hf

Premises used: nhdsWithin, Filter.mem_inf_principal
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst] s
hf : ∀ x ∈ s, {x_1 : X | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
choose :
  ∀ (t : (n : ℕ) → Finset X) (ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s)
    (hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 : X | x_1 ∈ s → x_1 ∈ f x}),
    ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
choose t ht hsub using fun n =>
    ((isCompact_compactCovering X n).inter_right hs).elim_nhds_subcover _ fun x hx => hf x hx.right

Premises used: setOf, isCompact_compactCovering, IsCompact.elim_nhds_subcover, And.right, IsCompact.inter_right
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst] s
hf : ∀ x ∈ s, {x_1 : X | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : (n : ℕ) → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 : X | x_1 ∈ s → x_1 ∈ f x}
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
⟨⋃ n, (t n : Set X), iUnion_subset fun n x hx => (ht n x hx).2,
      countable_iUnion fun n => (t n).countable_toSet, fun x hx => mem_iUnion₂.2 ?_⟩

Premises used: Iff.mpr, Set.iUnion_subset, Set.mem_iUnion₂, Set.countable_iUnion, SetLike.coe, And.right, And.intro, Exists.intro, Finset.countable_toSet, Set.iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst] s
hf : ∀ x ∈ s, {x_1 : X | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : (n : ℕ) → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 : X | x_1 ∈ s → x_1 ∈ f x}
n : ∀ (x : X) (hx : x ∈ s), ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
refine
    ⟨⋃ n, (t n : Set X), iUnion_subset fun n x hx => (ht n x hx).2,
      countable_iUnion fun n => (t n).countable_toSet, fun x hx => mem_iUnion₂.2 ?_⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst] s
hf : ∀ x ∈ s, {x_1 : X | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : (n : ℕ) → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 : X | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
rcases :
  ∀ (n : ℕ) (hn : x ∈ compactCovering X n),
    ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i
⊢ ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i

Tactic:
rcases exists_mem_compactCovering x with ⟨n, hn⟩

Premises used: exists_mem_compactCovering
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst] s
hf : ∀ x ∈ s, {x_1 : X | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : (n : ℕ) → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 : X | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
n : ℕ
hn : x ∈ compactCovering X n
rcases :
  ∀ (y : X) (hyt : y ∈ t n) (hyf : x ∈ s → x ∈ f y),
    ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i
⊢ ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i

Tactic:
rcases mem_iUnion₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩

Premises used: Set.mem_iUnion₂, And.intro, Iff.mp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst] s
hf : ∀ x ∈ s, {x_1 : X | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : (n : ℕ) → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 : X | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
n : ℕ
hn : x ∈ compactCovering X n
y : X
hyt : y ∈ t n
hyf : x ∈ s → x ∈ f y
⊢ ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i

Tactic:
⟨y, mem_iUnion.2 ⟨n, hyt⟩, hyf hx⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst] s
hf : ∀ x ∈ s, {x_1 : X | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : (n : ℕ) → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 : X | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
n : ℕ
hn : x ∈ compactCovering X n
y : X
hyt : y ∈ t n
hyf : x ∈ s → x ∈ f y
⊢ ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i

Tactic:
exact ⟨y, mem_iUnion.2 ⟨n, hyt⟩, hyf hx⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝 x
⊢ ∀ (x : X), f x ∈ 𝓝[univ] x

Tactic:
simp only [← nhdsWithin_univ] at hf

Premises used: nhdsWithin_univ
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
rcases :
  ∀ (s : Set X) (hsc : s.Countable) (hsU : Subset.{u_1} (α := Set X) univ (⋃ x ∈ s, f x)),
    ∃ (s : Set X), s.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, f x) univ
⊢ ∃ (s : Set X), s.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, f x) univ

Tactic:
rcases countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ fun x _ => hf x with
    ⟨s, -, hsc, hsU⟩

Premises used: isClosed_univ, countable_cover_nhdsWithin_of_sigmaCompact
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
s : Set X
hsc : s.Countable
hsU : Subset.{u_1} (α := Set X) univ (⋃ x ∈ s, f x)
⊢ ∃ (s : Set X), s.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, f x) univ

Tactic:
⟨s, hsc, univ_subset_iff.1 hsU⟩

Premises used: Set.univ_subset_iff, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
s : Set X
hsc : s.Countable
hsU : Subset.{u_1} (α := Set X) univ (⋃ x ∈ s, f x)
⊢ ∃ (s : Set X), s.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, f x) univ

Tactic:
exact ⟨s, hsc, univ_subset_iff.1 hsU⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
⊢ K.toFun = (⇑K : (a : ℕ) → Set X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
n : ℕ
⊢ IsCompact.{u_1} (X := X) ((K : (a : ℕ) → Set X) n)

Tactic:
K.isCompact' n

Premises used: CompactExhaustion.isCompact'
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
n : ℕ
⊢ Subset (α := Set X) ((K : (a : ℕ) → Set X) n : Set X) (interior ((K : (a : ℕ) → Set X) (n + 1)) : Set X)

Tactic:
K.subset_interior_succ' n

Premises used: CompactExhaustion.subset_interior_succ'
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
m n : ℕ
h : m ≤ n
⊢ Subset (α := Set X) ((K : (a : ℕ) → Set X) m : Set X) ((K : (a : ℕ) → Set X) n : Set X)

Tactic:
OrderHomClass.mono K h

Premises used: OrderHomClass.mono
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
n : ℕ
⊢ Subset (α := Set X) ((K : (a : ℕ) → Set X) n : Set X) ((K : (a : ℕ) → Set X) (n + 1) : Set X)

Tactic:
K.subset n.le_succ

Premises used: CompactExhaustion.subset, Nat.le_succ
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
m n : ℕ
h : m < n
⊢ Subset (α := Set X) ((K : (a : ℕ) → Set X) m : Set X) (interior ((K : (a : ℕ) → Set X) n) : Set X)

Tactic:
Subset.trans (K.subset_interior_succ m) <| interior_mono <| K.subset h

Premises used: interior_mono, Set.Subset.trans, CompactExhaustion.subset, CompactExhaustion.subset_interior_succ
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), (K : (a : ℕ) → Set X) n) univ

Tactic:
K.iUnion_eq'

Premises used: CompactExhaustion.iUnion_eq'
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ∃ (n : ℕ), Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) n : Set X) x

Tactic:
iUnion_eq_univ_iff.1 K.iUnion_eq x

Premises used: Set.iUnion_eq_univ_iff, CompactExhaustion.iUnion_eq, Iff.mp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
rcases :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) n : Set X) x),
    ∃ (n : ℕ), Membership.mem (α := Set X) (𝓝 x) ((K : (a : ℕ) → Set X) n : Set X)
⊢ ∃ (n : ℕ), Membership.mem (α := Set X) (𝓝 x) ((K : (a : ℕ) → Set X) n : Set X)

Tactic:
rcases K.exists_mem x with ⟨n, hn⟩

Premises used: CompactExhaustion.exists_mem
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
hn : Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) n : Set X) x
⊢ ∃ (n : ℕ), Membership.mem (α := Set X) (𝓝 x) ((K : (a : ℕ) → Set X) n : Set X)

Tactic:
⟨n + 1, mem_interior_iff_mem_nhds.mp <| K.subset_interior_succ n hn⟩

Premises used: mem_interior_iff_mem_nhds, HAdd.hAdd, Exists.intro, Iff.mp, CompactExhaustion.subset_interior_succ, OfNat.ofNat
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
hn : Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) n : Set X) x
⊢ ∃ (n : ℕ), Membership.mem (α := Set X) (𝓝 x) ((K : (a : ℕ) → Set X) n : Set X)

Tactic:
exact ⟨n + 1, mem_interior_iff_mem_nhds.mp <| K.subset_interior_succ n hn⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
suffices : ∃ (n : ℕ), s ⊆ interior ((K : (a : ℕ) → Set X) n)
⊢ ∃ (n : ℕ), s ⊆ (K : (a : ℕ) → Set X) n

Tactic:
suffices ∃ n, s ⊆ interior (K n) from this.imp fun _ ↦ (Subset.trans · interior_subset)
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ ∃ (n : ℕ), s ⊆ interior ((K : (a : ℕ) → Set X) n)

Tactic:
hs.elim_directed_cover (interior ∘ K) (fun _ ↦ isOpen_interior) ?_ ?_

Premises used: isOpen_interior, Set.sUnion, Function.comp, interior, DFunLike.coe, IsCompact.elim_directed_cover