awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
refine_1 :
  ∀ (h : IsCompactSystem (insert ∅ S)) (C : ℕ → Set α) (hdi : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C)
    (hi : ∀ (i : ℕ), C i ∈ S), Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
refine_2 :
  ∀
    (h :
      ∀ (C : ℕ → Set α),
        Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
          (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅)
    (C : ℕ → Set α) (h1 : ∀ (i : ℕ), C i ∈ insert ∅ S) (h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅),
    ∃ (n : ℕ), dissipate C n = ∅
⊢ IsCompactSystem (insert ∅ S) ↔
    ∀ (C : ℕ → Set α),
      Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
        (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅

Tactic:
refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : IsCompactSystem (insert ∅ S)
C : ℕ → Set α
hdi : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C
hi : ∀ (i : ℕ), C i ∈ S
refine_1 : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), dissipate C n = ∅
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅

Tactic:
rw [← exists_dissipate_eq_empty_iff_of_directed hdi]

Premises used: Set.exists_dissipate_eq_empty_iff_of_directed
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : IsCompactSystem (insert ∅ S)
C : ℕ → Set α
hdi : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C
hi : ∀ (i : ℕ), C i ∈ S
⊢ ∀ (i : ℕ), C i ∈ insert ∅ S

Tactic:
simp [hi]
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : IsCompactSystem (insert ∅ S)
C : ℕ → Set α
hdi : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C
hi : ∀ (i : ℕ), C i ∈ S
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), dissipate C n = ∅

Tactic:
exact h C (by simp [hi])
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅

Tactic:
rw [← biInter_le_eq_iInter] at h2

Premises used: Set.biInter_le_eq_iInter
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), dissipate C n) ∅
pos : ∀ (f : ∀ (n : ℕ), dissipate C n ∈ S), ∃ (n : ℕ), dissipate C n = ∅
neg : ∀ (f : ∃ (n : ℕ), dissipate C n ∉ S), ∃ (n : ℕ), dissipate C n = ∅
⊢ ∃ (n : ℕ), dissipate C n = ∅

Tactic:
by_cases! f : ∀ n, dissipate C n ∈ S
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), dissipate C n) ∅
f : ∀ (n : ℕ), dissipate C n ∈ S
⊢ ∃ (n : ℕ), dissipate C n = ∅

Tactic:
h (dissipate C) directed_dissipate f this.2

Premises used: Set.dissipate, And.right, Set.directed_dissipate
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), dissipate C n) ∅
f : ∀ (n : ℕ), dissipate C n ∈ S
⊢ ∃ (n : ℕ), dissipate C n = ∅

Tactic:
exact h (dissipate C) directed_dissipate f this.2

Premises used: Set.dissipate, And.right, Set.directed_dissipate
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), dissipate C n) ∅
f : ∃ (n : ℕ), dissipate C n ∉ S
neg : ∀ (n : ℕ) (hn : dissipate C n ∉ S), ∃ (n : ℕ), dissipate C n = ∅
⊢ ∃ (n : ℕ), dissipate C n = ∅

Tactic:
obtain ⟨n, hn⟩ := f
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), dissipate C n) ∅
n : ℕ
hn : dissipate C n ∉ S
⊢ dissipate C n = ∅

Tactic:
simpa [hn] using this.1 n

Premises used: And.left
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), dissipate C n) ∅
n : ℕ
hn : dissipate C n ∉ S
⊢ ∃ (n : ℕ), dissipate C n = ∅

Tactic:
exact ⟨n, by simpa [hn] using this.1 n⟩
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
refine_2 : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), dissipate C n) ∅
⊢ ∃ (n : ℕ), dissipate C n = ∅

Tactic:
suffices (∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ (⋂ n, dissipate C n = ∅) by
    by_cases! f : ∀ n, dissipate C n ∈ S
    · exact h (dissipate C) directed_dissipate f this.2
    · obtain ⟨n, hn⟩ := f
      exact ⟨n, by simpa [hn] using this.1 n⟩
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
⊢ (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), dissipate C n) ∅

Tactic:
⟨fun n ↦ ?_, h2⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
refine_2 : ∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅
⊢ (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), dissipate C n) ∅

Tactic:
refine ⟨fun n ↦ ?_, h2⟩
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
n : ℕ
pos : ∀ (g : (dissipate C n).Nonempty), dissipate C n ∈ S ∨ dissipate C n = ∅
neg : ∀ (g : ¬(dissipate C n).Nonempty), dissipate C n ∈ S ∨ dissipate C n = ∅
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅

Tactic:
by_cases g : (dissipate C n).Nonempty

Premises used: Set.dissipate, Set.Nonempty
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
n : ℕ
g : (dissipate C n).Nonempty
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅

Tactic:
simpa [or_comm] using hpi.insert_empty.dissipate_mem h1 n g

Premises used: IsPiSystem.insert_empty, or_comm, IsPiSystem.dissipate_mem
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
n : ℕ
g : ¬(dissipate C n).Nonempty
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅

Tactic:
.inr (Set.not_nonempty_iff_eq_empty.mp g)

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp, Or.inr
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
n : ℕ
g : ¬(dissipate C n).Nonempty
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅

Tactic:
exact .inr (Set.not_nonempty_iff_eq_empty.mp g)
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
rw :
  (∀ (C : ℕ → Set α),
      Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
        (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅) ↔
    ∀ (C : ℕ → Set α),
      Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
        (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α),
      Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
        (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
rw [isCompactSystem_iff_of_directed hpi]

Premises used: isCompactSystem_iff_of_directed
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
⊢ (∀ (C : ℕ → Set α),
      Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
        (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅) ↔
    ∀ (C : ℕ → Set α),
      Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
        (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
refine_1 :
  ∀
    (h1 :
      ∀ (C : ℕ → Set α),
        Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
          (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅)
    (C : ℕ → Set α) (h3 : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C) (h4 : ∀ (i : ℕ), C i ∈ S),
    (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
refine_2 :
  ∀
    (h1 :
      ∀ (C : ℕ → Set α),
        Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
          (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i))
    (C : ℕ → Set α) (h3 : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C) (s : ∀ (i : ℕ), C i ∈ S),
    Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
⊢ (∀ (C : ℕ → Set α),
      Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
        (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅) ↔
    ∀ (C : ℕ → Set α),
      Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
        (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h3 : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C
h4 : ∀ (i : ℕ), C i ∈ S
refine_1 : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
⊢ (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
contrapose!
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
C : ℕ → Set α
h3 : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C
s : ∀ (i : ℕ), C i ∈ S
refine_2 : (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅

Tactic:
contrapose!
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h3 : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C
h4 : ∀ (i : ℕ), C i ∈ S
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅

Tactic:
h1 C h3 h4
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
C : ℕ → Set α
h3 : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C
h4 : ∀ (i : ℕ), C i ∈ S
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅

Tactic:
exact h1 C h3 h4
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
C : ℕ → Set α
h3 : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C
s : ∀ (i : ℕ), C i ∈ S
⊢ (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
h1 C h3 s
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 :
  ∀ (C : ℕ → Set α),
    Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C →
      (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
C : ℕ → Set α
h3 : Directed (fun (x1 x2 : Set α) ↦ x1 ⊇ x2) C
s : ∀ (i : ℕ), C i ∈ S
⊢ (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
exact h1 C h3 s
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ IsCompactSystem.{u_2} (α := α) {s : Set α | IsCompact s ∧ IsClosed s}

Tactic:
IsCompactSystem.of_nonempty_iInter fun C hC_cc h_nonempty ↦ ?_

Premises used: IsCompactSystem.of_nonempty_iInter
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
refine :
  ∀ (C : ℕ → Set α) (hC_cc : ∀ (i : ℕ), Membership.mem (γ := Set (Set α)) {s : Set α | IsCompact s ∧ IsClosed s} (C i))
    (h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty), Set.Nonempty.{u_2} (α := α) (⋂ (i : ℕ), C i)
⊢ IsCompactSystem.{u_2} (α := α) {s : Set α | IsCompact s ∧ IsClosed s}

Tactic:
refine IsCompactSystem.of_nonempty_iInter fun C hC_cc h_nonempty ↦ ?_

Premises used: IsCompactSystem.of_nonempty_iInter
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), Membership.mem (γ := Set (Set α)) {s : Set α | IsCompact s ∧ IsClosed s} (C i)
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
rw : Set.Nonempty.{u_2} (α := α) (⋂ (x : ℕ), dissipate C x)
⊢ Set.Nonempty.{u_2} (α := α) (⋂ (i : ℕ), C i)

Tactic:
rw [← iInter_dissipate]

Premises used: Set.iInter_dissipate
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), Membership.mem (γ := Set (Set α)) {s : Set α | IsCompact s ∧ IsClosed s} (C i)
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ Set.Nonempty.{u_2} (α := α) (⋂ (x : ℕ), dissipate C x)

Tactic:
IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C)
    (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ isClosed_biInter (fun i _ ↦ (hC_cc i).2))

Premises used: Set.dissipate, isClosed_biInter, IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed, And.right
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), Membership.mem (γ := Set (Set α)) {s : Set α | IsCompact s ∧ IsClosed s} (C i)
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
refine_1 : ∀ (n : ℕ), dissipate C (n + 1) ⊆ dissipate C n
refine_2 : IsCompact (dissipate C 0)
⊢ Set.Nonempty.{u_2} (α := α) (⋂ (x : ℕ), dissipate C x)

Tactic:
refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C)
    (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ isClosed_biInter (fun i _ ↦ (hC_cc i).2))

Premises used: Set.dissipate, isClosed_biInter, IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed, And.right
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), Membership.mem (γ := Set (Set α)) {s : Set α | IsCompact s ∧ IsClosed s} (C i)
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
n : ℕ
⊢ n ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), Membership.mem (γ := Set (Set α)) {s : Set α | IsCompact s ∧ IsClosed s} (C i)
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
n : ℕ
⊢ dissipate C (n + 1) ⊆ dissipate C n

Tactic:
exact Set.antitone_dissipate (by lia)

Premises used: Set.antitone_dissipate
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), Membership.mem (γ := Set (Set α)) {s : Set α | IsCompact s ∧ IsClosed s} (C i)
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ IsCompact (dissipate C 0)

Tactic:
simpa using (hC_cc 0).1

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T2Space α
⊢ IsCompactSystem.{u_2} (α := α) {s : Set α | IsCompact s ∧ IsClosed s}

Tactic:
isCompactSystem_isCompact_isClosed α

Premises used: isCompactSystem_isCompact_isClosed
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T2Space α
h : ∀ (s : Set α), IsCompact s ↔ IsCompact s ∧ IsClosed s
⊢ IsCompactSystem.{u_2} (α := α) {s : Set α | IsCompact s}

Tactic:
convert! isCompactSystem_isCompact_isClosed α with s

Premises used: isCompactSystem_isCompact_isClosed
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T2Space α
s : Set α
⊢ IsCompact s ↔ IsCompact s ∧ IsClosed s

Tactic:
simpa using IsCompact.isClosed

Premises used: IsCompact.isClosed
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ IsCompactSystem (α := α) (insert Set.univ {s : Set α | IsCompact s ∧ IsClosed s})

Tactic:
(isCompactSystem_isCompact_isClosed α).insert_univ

Premises used: isCompactSystem_isCompact_isClosed, IsCompactSystem.insert_univ
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
A : Set X
⊢ IsOpen[inst] A ↔ ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)

Tactic:
IsCoherentWith.isOpen_iff isCoherentWith

Premises used: Set.Mem, CompactlyCoherentSpace.isCoherentWith, IsCompact, Topology.IsCoherentWith.isOpen_iff
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
A : Set X
⊢ IsClosed[inst] A ↔ ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (K ↓∩ A)

Tactic:
IsCoherentWith.isClosed_iff isCoherentWith

Premises used: Set.Mem, CompactlyCoherentSpace.isCoherentWith, Topology.IsCoherentWith.isClosed_iff, IsCompact
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
s : Set X
⊢ IsOpen[inst] s ↔
    ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous[_, inst] f → IsOpen (f ⁻¹' s)

Tactic:
⟨fun hs _ _ _ _ hf ↦ hs.preimage hf, fun hs ↦ isOpen_iff |>.mpr ?_⟩

Premises used: Iff.mpr, CompactlyCoherentSpace.isOpen_iff, Iff.intro, IsOpen.preimage
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
s : Set X
refine :
  ∀
    (hs :
      ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s))
    (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)
⊢ IsOpen[inst] s ↔
    ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous[_, inst] f → IsOpen (f ⁻¹' s)

Tactic:
refine ⟨fun hs _ _ _ _ hf ↦ hs.preimage hf, fun hs ↦ isOpen_iff |>.mpr ?_⟩
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous[_, inst] f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ CompactSpace.{u} (↑K : Type u)

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous[_, inst] f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace.{u} (↑K : Type u)
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)

Tactic:
hs K Subtype.val continuous_subtype_val

Premises used: continuous_subtype_val, Set.Elem, Subtype.val