awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ
h₁ : ∀ (i : { U : Set X // U ∈ c }), (↑i : Set X)ᶜ.Nonempty
⊢ Set.Nonempty.{u} (α := X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ)
have h₂ : ∀ (i : { U : Set X // U ∈ c }), IsCompact (↑i : Set X)ᶜ
Tactic: apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ
h₁ : ∀ (i : { U : Set X // U ∈ c }), (↑i : Set X)ᶜ.Nonempty
h₂ : ∀ (i : { U : Set X // U ∈ c }), IsCompact (↑i : Set X)ᶜ
⊢ Set.Nonempty.{u} (α := X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ)
have h₃ : ∀ (i : { U : Set X // U ∈ c }), IsClosed[inst] (↑i : Set X)ᶜ
Tactic: apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
U : Set X
hU : U ∈ c
U' : Set X
hU' : U' ∈ c
⊢ ∃ (z : { U : Set X // U ∈ c }),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U hU))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z) ∧
      (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U' hU'))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z)
have h : ∀ (V : Set X) (hVc : V ∈ c) (hVU : U ⊆ V) (hVU' : U' ⊆ V),
  ∃ (z : { U : Set X // U ∈ c }),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U hU))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z) ∧
      (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U' hU'))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z)
Tactic: obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
have h : Sᶜ ∈ opens ∧ ∀ s ∈ c, s ⊆ Sᶜ
Tactic: use Sᶜ
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ Sᶜ ∈ opens ∧ ∀ s ∈ c, s ⊆ Sᶜ
have h : Sᶜᶜ.Nonempty
Tactic: refine ⟨⟨Set.Subset.refl _, isOpen_compl_iff.mpr hS, ?_⟩, fun U Uc => (hcne ⟨U, Uc⟩).elim⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V
have obtain : ∀ (U : Set X) (h : Maximal (fun (x : Set X) ↦ x ∈ opens) U),
  ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V
Tactic: obtain ⟨U, h⟩ :=
    zorn_subset opens fun c hc hz => by
      by_cases hcne : c.Nonempty
      · obtain ⟨U₀, hU₀⟩ := hcne
        haveI : Nonempty { U // U ∈ c } := ⟨⟨U₀, hU₀⟩⟩
        obtain ⟨U₀compl, -, -⟩ := hc hU₀
        use ⋃₀ c
        refine ⟨⟨?_, ?_, ?_⟩, fun U hU _ hx => ⟨U, hU, hx⟩⟩
        · exact fun _ hx => ⟨U₀, hU₀, U₀compl hx⟩
        · exact isOpen_sUnion fun _ h => (hc h).2.1
        · convert_to (⋂ U : { U // U ∈ c }, U.1ᶜ).Nonempty
          · ext
            simp only [not_exists, not_and, Set.mem_iInter, Subtype.forall,
              mem_compl_iff, mem_sUnion]
          apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
          · rintro ⟨U, hU⟩ ⟨U', hU'⟩
            obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'
            exact ⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩
          · exact fun U => (hc U.2).2.2
          · exact fun U => (hc U.2).2.1.isClosed_compl.isCompact
          · exact fun U => (hc U.2).2.1.isClosed_compl
      · use Sᶜ
        refine ⟨⟨Set.Subset.refl _, isOpen_compl_iff.mpr hS, ?_⟩, fun U Uc => (hcne ⟨U, Uc⟩).elim⟩
        rw [compl_compl]
        exact hne
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V
have Uc : Sᶜ ⊆ U
Tactic: obtain ⟨Uc, Uo, Ucne⟩ := h.prop
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V
have Uo : IsOpen[inst] U
Tactic: obtain ⟨Uc, Uo, Ucne⟩ := h.prop
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V
have Ucne : Uᶜ.Nonempty
Tactic: obtain ⟨Uc, Uo, Ucne⟩ := h.prop
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V
have refine : ∀ V' ⊆ Uᶜ, V'.Nonempty → IsClosed[inst] V' → V' = Uᶜ
Tactic: refine ⟨Uᶜ, Set.compl_subset_comm.mp Uc, Ucne, Uo.isClosed_compl, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
⊢ V'ᶜ = U
have refine_1 : Sᶜ ⊆ V'ᶜ
Tactic: refine h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
refine_1 : Sᶜ ⊆ V'ᶜ
⊢ V'ᶜ = U
have refine_2 : V'ᶜᶜ.Nonempty
Tactic: refine h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
⊢ V' = Uᶜ
have this : V'ᶜ = U
Tactic: have : V'ᶜ = U := by
    refine h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)
    · exact Set.Subset.trans Uc (Set.subset_compl_comm.mp V'sub)
    · simp only [compl_compl, V'ne]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
this : V'ᶜ = U
⊢ V' = Uᶜ
have rw : V' = V'ᶜᶜ
Tactic: rw [← this, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
this : V'ᶜ = U
rw : V' = V'ᶜᶜ
⊢ V' = Uᶜ
have rw₁ : V' = V'
Tactic: rw [← this, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), dissipate C n = ∅
have contrapose! : (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
hp : IsCompactSystem S
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
have revert : ∀ (h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty), Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
Tactic: revert h_nonempty
Cleared hypotheses: h_nonempty
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
hp : IsCompactSystem S
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
⊢ ∀ (h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty), Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
have contrapose! : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), dissipate C n = ∅
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) ∅
⊢ ∃ (n : ℕ), dissipate s n = ∅
have pos : ∀ (g : ∃ (n : ℕ), s n = ∅), ∃ (n : ℕ), dissipate s n = ∅
Tactic: by_cases! g : ∃ n, s n = ∅
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) ∅
pos : ∀ (g : ∃ (n : ℕ), s n = ∅), ∃ (n : ℕ), dissipate s n = ∅
⊢ ∃ (n : ℕ), dissipate s n = ∅
have neg : ∀ (g : ∀ (n : ℕ), (s n).Nonempty), ∃ (n : ℕ), dissipate s n = ∅
Tactic: by_cases! g : ∃ n, s n = ∅
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) ∅
g : ∃ (n : ℕ), s n = ∅
⊢ ∃ (n : ℕ), dissipate s n = ∅
have h₁ : dissipate s (g.choose (p := fun (n : ℕ) ↦ s n = ∅)) = ∅
Tactic: use g.choose
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) ∅
g : ∃ (n : ℕ), s n = ∅
⊢ dissipate s (g.choose (p := fun (n : ℕ) ↦ s n = ∅)) = ∅
have h₁ : ∀ (hd : Subset.{u_1} (α := Set α) (⋂ (i : ℕ), s i) ∅) (g : ∃ (n : ℕ), s n = ∅),
  dissipate s (g.choose (p := fun (n : ℕ) ↦ s n = ∅)) ⊆ ∅
Tactic: rw [← subset_empty_iff] at hd ⊢
Cleared hypotheses: hd, g
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
⊢ IsCompactSystem (insert Set.univ S)
have inl : ∀ (hα : IsEmpty α), IsCompactSystem (insert Set.univ S)
Tactic: rcases isEmpty_or_nonempty α with hα | _
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
inl : ∀ (hα : IsEmpty α), IsCompactSystem (insert Set.univ S)
⊢ IsCompactSystem (insert Set.univ S)
have inr : Nonempty α → IsCompactSystem (insert Set.univ S)
Tactic: rcases isEmpty_or_nonempty α with hα | _
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
h_1 : Nonempty α
⊢ IsCompactSystem (insert Set.univ S)
have inr : ∀
  (h :
    ∀ (C : ℕ → Set α),
      (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)),
  Nonempty α →
    ∀ (C : ℕ → Set α),
      (∀ (i : ℕ), C i ∈ insert Set.univ S) →
        (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
Tactic: rw [IsCompactSystem.iff_nonempty_iInter] at h ⊢
Cleared hypotheses: h, h_1
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), s i)
have pos : ∀ (h₀ : ∀ (n : ℕ), s n ∉ S), Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), s i)
Tactic: by_cases! h₀ : ∀ n, s n ∉ S
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
pos : ∀ (h₀ : ∀ (n : ℕ), s n ∉ S), Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), s i)
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), s i)
have neg : ∀ (h₀ : ∃ (n : ℕ), s n ∈ S), Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), s i)
Tactic: by_cases! h₀ : ∀ n, s n ∉ S
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (hypothesis)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), s i)
have h₁ : ∀ (i : ℕ), s' i ∈ S
Tactic: have h₁ : ∀ i, s' i ∈ S := by grind
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) (⋂ (i : ℕ), s' i)
have h₂ : ∀ (x : α), Membership.mem (γ := Set α) (⋂ (i : ℕ), s i) x ↔ Membership.mem (γ := Set α) (⋂ (i : ℕ), s' i) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
x : α
⊢ Membership.mem (γ := Set α) (⋂ (i : ℕ), s i) x ↔ Membership.mem (γ := Set α) (⋂ (i : ℕ), s' i) x
have h₂ : (∀ (i : ℕ), x ∈ s i) ↔ ∀ (i : ℕ), x ∈ s' i
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (hypothesis)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), s i)
have h₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) (⋂ (i : ℕ), s' i)
Tactic: have h₂ : ⋂ i, s i = ⋂ i, s' i := by ext; simp; grind
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) (⋂ (i : ℕ), s' i)
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), s i)
have neg : ∀ (n : ℕ), (dissipate s' n).Nonempty
Tactic: apply h₂ ▸ h s' h₁
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) (⋂ (i : ℕ), s' i)
⊢ ∀ (n : ℕ), (dissipate s' n).Nonempty
have neg : ∀ (j : ℕ) (hj : dissipate s' j = ∅), False
Tactic: by_contra! ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) (⋂ (i : ℕ), s' i)
j : ℕ
hj : dissipate s' j = ∅
v : ℕ
hv : n ≤ v
⊢ dissipate s v = dissipate s' v
have h₃ : ∀ (x : α), x ∈ dissipate s v ↔ x ∈ dissipate s' v
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) (⋂ (i : ℕ), s' i)
j : ℕ
hj : dissipate s' j = ∅
v : ℕ
hv : n ≤ v
x : α
⊢ x ∈ dissipate s v ↔ x ∈ dissipate s' v
have h₃ : (∀ y ≤ v, x ∈ s y) ↔ ∀ y ≤ v, x ∈ s' y
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (hypothesis)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) (⋂ (i : ℕ), s' i)
j : ℕ
hj : dissipate s' j = ∅
⊢ False
have h₃ : ∀ (v : ℕ) (hv : n ≤ v), dissipate s v = dissipate s' v
Tactic: have h₃ (v : ℕ) (hv : n ≤ v) : dissipate s v = dissipate s' v := by ext; simp; grind
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
h_1 : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ (n : ℕ), s n ∈ S
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ s n ∈ S) h₀
s' : (i : ℕ) → Set α := fun (i : ℕ) ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) (⋂ (i : ℕ), s' i)
j : ℕ
hj : dissipate s' j = ∅
h₃ : ∀ (v : ℕ) (hv : n ≤ v), dissipate s v = dissipate s' v
⊢ dissipate s' (max j n) = ∅
have rw : ∀ (hj : dissipate s' j ⊆ ∅) (h₃ : ∀ (v : ℕ) (hv : n ≤ v), dissipate s v = dissipate s' v), dissipate s' (max j n) ⊆ ∅
Tactic: rw [← subset_empty_iff] at hj ⊢
Cleared hypotheses: hj, h₃