awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
⊢ SigmaCompactSpace ((i : ι) × X i)
have inl : IsEmpty ι → SigmaCompactSpace ((i : ι) × X i)
Tactic: cases isEmpty_or_nonempty ι
-- 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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
inl : IsEmpty ι → SigmaCompactSpace ((i : ι) × X i)
⊢ SigmaCompactSpace ((i : ι) × X i)
have inr : Nonempty ι → SigmaCompactSpace ((i : ι) × X i)
Tactic: cases isEmpty_or_nonempty ι
-- 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 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
⊢ SigmaCompactSpace ((i : ι) × X i)
have inr : ∀ (f : ℕ → ι) (hf : Function.Surjective f), SigmaCompactSpace ((i : ι) × X i)
Tactic: rcases exists_surjective_nat ι with ⟨f, hf⟩
-- 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 : 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
⊢ SigmaCompactSpace ((i : ι) × X i)
have inr : ∀ (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 ⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => ?_, ?_⟩⟩
-- 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 : 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 :
  ∀ (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)
⊢ SigmaCompactSpace ((i : ι) × X i)
have inr₁ : 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: refine ⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => ?_, ?_⟩⟩
-- 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 : 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 : ℕ
⊢ 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)
have 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)
Tactic: refine (finite_le_nat _).isCompact_biUnion fun k _ => ?_
-- 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 : 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
⊢ 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
have 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)
Tactic: simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion, hf.forall]
-- 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 : 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)
⊢ ∃ (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)
have 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)
Tactic: rcases exists_mem_compactCovering y with ⟨n, hn⟩
-- 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 : 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)
have inr : Membership.mem (γ := Set (X (f k))) (compactCovering (X (f k)) (max k n)) y
Tactic: refine ⟨max k n, k, le_max_left _ _, mem_image_of_mem _ ?_⟩
-- 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
inst_2 : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
⊢ Eq.{u_2 + 1} (α := Set Y) (⋃ (n : ℕ), (fun (n : ℕ) ↦ e ⁻¹' compactCovering X n) n) univ
have rw : e ⁻¹' ⋃ (i : ℕ), compactCovering X i = univ
Tactic: rw [← preimage_iUnion, iUnion_compactCovering, preimage_univ]
-- 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
inst_2 : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
rw : e ⁻¹' ⋃ (i : ℕ), compactCovering X i = univ
⊢ Eq.{u_2 + 1} (α := Set Y) (⋃ (n : ℕ), (fun (n : ℕ) ↦ e ⁻¹' compactCovering X n) n) univ
have rw₁ : e ⁻¹' univ = univ
Tactic: rw [← preimage_iUnion, iUnion_compactCovering, preimage_univ]
-- 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
inst_2 : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
rw : e ⁻¹' ⋃ (i : ℕ), compactCovering X i = univ
rw₁ : e ⁻¹' univ = univ
⊢ Eq.{u_2 + 1} (α := Set Y) (⋃ (n : ℕ), (fun (n : ℕ) ↦ e ⁻¹' compactCovering X n) n) univ
have rw₂ : Eq.{u_2 + 1} (α := Set Y) univ univ
Tactic: rw [← preimage_iUnion, iUnion_compactCovering, preimage_univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (hypothesis)
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
⊢ Set.Countable.{u_3} (α := ι) univ
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
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
have refine : ∀ (i : ι),
  Membership.mem (γ := Set ι) univ i →
    Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i
Tactic: refine (countable_iUnion fun n => (this n).countable).mono fun i _ => ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
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
⊢ Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i
have rcases : ∀ (x : X) (hx : x ∈ f i), Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i
Tactic: rcases hne i with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
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
⊢ Membership.mem (γ := Set ι) (⋃ (i : ℕ), {i_1 : ι | (f i_1 ∩ compactCovering X i).Nonempty}) i
have rcases : ∀ (n : ℕ) (hn : x ∈ compactCovering X n),
  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⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (hypothesis)
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
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
have hf₁ : ∀ x ∈ s, {x_1 : X | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
Tactic: simp only [nhdsWithin, mem_inf_principal] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
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 ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
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
have n : ∀ (x : X) (hx : x ∈ s), ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i
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 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
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
⊢ ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i
have rcases : ∀ (n : ℕ) (hn : x ∈ compactCovering X n),
  ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i
Tactic: rcases exists_mem_compactCovering x with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
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
⊢ ∃ (i : X) (_ : Membership.mem (γ := Set X) (⋃ (n : ℕ), (↑(t n) : Set X)) i), x ∈ f i
have 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
Tactic: rcases mem_iUnion₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝 x
⊢ ∃ (s : Set X), s.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, f x) univ
have hf₁ : ∀ (x : X), f x ∈ 𝓝[univ] x
Tactic: simp only [← nhdsWithin_univ] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
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), s.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, f x) univ
have 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
Tactic: rcases countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ fun x _ => hf x with
    ⟨s, -, hsc, hsU⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ∃ (n : ℕ), Membership.mem (α := Set X) (𝓝 x) ((K : (a : ℕ) → Set X) n : Set X)
have 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)
Tactic: rcases K.exists_mem x with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ ∃ (n : ℕ), s ⊆ (K : (a : ℕ) → Set X) n
have suffices : ∃ (n : ℕ), s ⊆ interior ((K : (a : ℕ) → Set X) n)
Tactic: suffices ∃ n, s ⊆ interior (K n) from this.imp fun _ ↦ (Subset.trans · interior_subset)
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
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)
have refine_1 : s ⊆ ⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i
Tactic: refine hs.elim_directed_cover (interior ∘ K) (fun _ ↦ isOpen_interior) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
refine_1 : s ⊆ ⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i
⊢ ∃ (n : ℕ), s ⊆ interior ((K : (a : ℕ) → Set X) n)
have refine_2 : Directed (ι := ℕ) (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) (interior ∘ (⇑K : (a : ℕ) → Set X))
Tactic: refine hs.elim_directed_cover (interior ∘ K) (fun _ ↦ isOpen_interior) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.SigmaCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
h : x ∈ s
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i) x
have refine_1 : ∀ (k : ℕ) (hk : Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) k : Set X) x),
  Membership.mem (γ := Set X) (⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i) x
Tactic: rcases K.exists_mem x with ⟨k, hk⟩
-- 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
K : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
⊢ CompactExhaustion X
have a : Nonempty.{u_4 + 1} (CompactExhaustion X)
Tactic: apply Classical.choice
-- 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
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
⊢ Nonempty.{u_4 + 1} (CompactExhaustion X)
have a : ∀ (n : ℕ),
  Subset.{u_4} (α := Set X) ((fun (n : ℕ) ↦ (↑(K n) : Set X)) n) (interior ((fun (n : ℕ) ↦ (↑(K n) : Set X)) (n + 1)))
Tactic: refine ⟨⟨fun n ↦ (K n).1, fun n => (K n).2, fun n ↦ ?_, ?_⟩⟩
-- 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
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
a :
  ∀ (n : ℕ),
    Subset.{u_4} (α := Set X) ((fun (n : ℕ) ↦ (↑(K n) : Set X)) n) (interior ((fun (n : ℕ) ↦ (↑(K n) : Set X)) (n + 1)))
⊢ Nonempty.{u_4 + 1} (CompactExhaustion X)
have a₁ : Eq.{u_4 + 1} (α := Set X) (⋃ (n : ℕ), (fun (n : ℕ) ↦ (↑(K n) : Set X)) n) univ
Tactic: refine ⟨⟨fun n ↦ (K n).1, fun n => (K n).2, fun n ↦ ?_, ?_⟩⟩
-- 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
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
⊢ Eq.{u_4 + 1} (α := Set X) (⋃ (n : ℕ), (fun (n : ℕ) ↦ (↑(K n) : Set X)) n) univ
have a : Subset.{u_4} (α := Set X) (⋃ (n : ℕ), compactCovering X n) (⋃ (n : ℕ), (fun (n : ℕ) ↦ (↑(K n) : Set X)) n)
Tactic: refine univ_subset_iff.1 (iUnion_compactCovering X ▸ ?_)
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ x ∈ s
have rcases : ∀ (t : Set α) (ts : t ⊆ s) (xt : x ∈ t), x ∈ s
Tactic: rcases H y ys with ⟨t, ts, xt, -, -⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty
have xs : x ∈ s
Tactic: have xs : x ∈ s := by
    rcases H y ys with ⟨t, ts, xt, -, -⟩
    exact ts xt
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty
have inl : ∀ (t : Set α) (ts : t ⊆ s) (xt : x ∈ t) (yt : y ∈ t) (ht : IsPreconnected t), (s ∩ (u ∩ v)).Nonempty
Tactic: rcases H y ys with ⟨t, ts, xt, yt, ht⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
⊢ (s ∩ (u ∩ v)).Nonempty
have this : (t ∩ (u ∩ v)).Nonempty
Tactic: have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty
have inr : ∀ (t : Set α) (ts : t ⊆ s) (xt : x ∈ t) (zt : z ∈ t) (ht : IsPreconnected t), (s ∩ (u ∩ v)).Nonempty
Tactic: rcases H z zs with ⟨t, ts, xt, zt, ht⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
⊢ (s ∩ (u ∩ v)).Nonempty
have this : (t ∩ (v ∩ u)).Nonempty
Tactic: have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
⊢ (s ∩ (u ∩ v)).Nonempty
have x₁ : x ∈ u ∪ v
Tactic: cases hs xs with
  | inl xu =>
    rcases H y ys with ⟨t, ts, xt, yt, ht⟩
    have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
    exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩
  | inr xv =>
    rcases H z zs with ⟨t, ts, xt, zt, ht⟩
    have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
    exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩