awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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 : ℕ), C n = ∅
have refine_1 : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), dissipate C n = ∅
Tactic: rw [← exists_dissipate_eq_empty_iff_of_directed hdi]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (hypothesis)
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) ∅
⊢ ∃ (n : ℕ), dissipate C n = ∅
have h2₁ : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (m : ℕ), ⋂ (_ : m ≤ n), C m) ∅
Tactic: rw [← biInter_le_eq_iInter] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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 : ℕ), dissipate C n = ∅
have pos : ∀ (f : ∀ (n : ℕ), dissipate C n ∈ S), ∃ (n : ℕ), dissipate C n = ∅
Tactic: by_cases! f : ∀ n, dissipate C n ∈ S
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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 = ∅
⊢ ∃ (n : ℕ), dissipate C n = ∅
have neg : ∀ (f : ∃ (n : ℕ), dissipate C n ∉ S), ∃ (n : ℕ), dissipate C n = ∅
Tactic: by_cases! f : ∀ n, dissipate C n ∈ S
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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 = ∅
have neg : ∀ (n : ℕ) (hn : dissipate C n ∉ S), ∃ (n : ℕ), dissipate C n = ∅
Tactic: obtain ⟨n, hn⟩ := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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 = ∅
have refine_2 : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ Eq.{u_1 + 1} (α := Set α) (⋂ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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) ∅
have refine_2 : ∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅
Tactic: refine ⟨fun n ↦ ?_, h2⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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 = ∅
have pos : ∀ (g : (dissipate C n).Nonempty), dissipate C n ∈ S ∨ dissipate C n = ∅
Tactic: by_cases g : (dissipate C n).Nonempty
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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 = ∅
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅
have neg : ∀ (g : ¬(dissipate C n).Nonempty), dissipate C n ∈ S ∨ dissipate C n = ∅
Tactic: by_cases g : (dissipate C n).Nonempty
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
⊢ 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)
have 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)
Tactic: rw [isCompactSystem_iff_of_directed hpi]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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)
have 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)
Tactic: refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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)
⊢ (∀ (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)
have 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 = ∅
Tactic: refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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
⊢ (∀ (n : ℕ), (C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
have refine_1 : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), C n = ∅
have refine_2 : (∀ (n : ℕ), (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_2
inst : TopologicalSpace α
⊢ IsCompactSystem.{u_2} (α := α) {s : Set α | IsCompact s ∧ IsClosed s}
have 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)
Tactic: refine IsCompactSystem.of_nonempty_iInter fun C hC_cc h_nonempty ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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} (α := α) (⋂ (i : ℕ), C i)
have rw : Set.Nonempty.{u_2} (α := α) (⋂ (x : ℕ), dissipate C x)
Tactic: rw [← iInter_dissipate]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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)
have refine_1 : ∀ (n : ℕ), dissipate C (n + 1) ⊆ dissipate C n
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))
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
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
⊢ Set.Nonempty.{u_2} (α := α) (⋂ (x : ℕ), dissipate C x)
have refine_2 : IsCompact (dissipate C 0)
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))
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactSystem (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T2Space α
⊢ IsCompactSystem.{u_2} (α := α) {s : Set α | IsCompact s}
have h : ∀ (s : Set α), IsCompact s ↔ IsCompact s ∧ IsClosed s
Tactic: convert! isCompactSystem_isCompact_isClosed α with s
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
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)
have 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)
Tactic: refine ⟨fun hs _ _ _ _ hf ↦ hs.preimage hf, fun hs ↦ isOpen_iff |>.mpr ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (hypothesis)
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
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)
have this : CompactSpace.{u} (↑K : Type u)
Tactic: have : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
⊢ CompactlyCoherentSpace X
have refine : ∀ (A : Set X) (hA : ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)) (K : Type u)
  (x : TopologicalSpace K), CompactSpace K → ∀ (f : K → X) (hf : Continuous[_, inst] f), IsOpen (f ⁻¹' A)
Tactic: refine of_isOpen fun A hA ↦ h A fun K _ _ f hf ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
A : Set X
hA : ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)
K : Type u
x : TopologicalSpace K
h_1 : CompactSpace K
f : K → X
hf : Continuous[x, inst] f
⊢ IsOpen[x] (f ⁻¹' A)
have hA₁ : IsOpen[instTopologicalSpaceSubtype] (range f ↓∩ A)
Tactic: specialize hA (range f) (isCompact_range hf)
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
A : Set X
K : Type u
x : TopologicalSpace K
h_1 : CompactSpace K
f : K → X
hf : Continuous[x, inst] f
hA : IsOpen[instTopologicalSpaceSubtype] (range f ↓∩ A)
⊢ IsOpen[x] (f ⁻¹' A)
have this : IsOpen[x] (codRestrict f (range f) sorry ⁻¹' range f ↓∩ A)
Tactic: have := hA.preimage (hf.codRestrict mem_range_self)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
A : Set X
K : Type u
x : TopologicalSpace K
h_1 : CompactSpace K
f : K → X
hf : Continuous[x, inst] f
hA : IsOpen[instTopologicalSpaceSubtype] (range f ↓∩ A)
this : IsOpen[x] (codRestrict f (range f) ⋯ ⁻¹' range f ↓∩ A)
⊢ IsOpen[x] (f ⁻¹' A)
have rwa : ∀ (this : IsOpen[x] (Subtype.val (p := fun (x : X) ↦ x ∈ range f) ∘ codRestrict f (range f) sorry ⁻¹' A)),
  IsOpen[x] (f ⁻¹' A)
Tactic: rwa [← preimage_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set (𝐤X)
⊢ IsOpen[instTopologicalSpace] A ↔
    ∀ (K : Set X),
      IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)
have simp_rw : (∀ (i : Set X) (i_1 : IsCompact i),
    IsOpen[TopologicalSpace.coinduced Subtype.val
          { IsOpen := instTopologicalSpace._aux_1 i, isOpen_univ := sorry, isOpen_inter := sorry, isOpen_sUnion := sorry }]
      ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)) ↔
  ∀ (K : Set X),
    IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)
Tactic: simp_rw [isOpen_coinduced, isOpen_iSup_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set (𝐤X)
⊢ IsClosed[instTopologicalSpace] A ↔
    ∀ (K : Set X),
      IsCompact K → IsClosed[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)
have simp_rw : (∀ (i : Set X) (i_1 : IsCompact i),
    IsClosed[TopologicalSpace.coinduced (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)
          (TopologicalSpace.coinduced Subtype.val
            { IsOpen := instTopologicalSpace._aux_1 i, isOpen_univ := sorry, isOpen_inter := sorry, isOpen_sUnion := sorry })]
      A) ↔
  ∀ (K : Set X),
    IsCompact K →
      IsClosed[TopologicalSpace.coinduced (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)
            (TopologicalSpace.coinduced Subtype.val instTopologicalSpaceSubtype)]
        A
Tactic: simp_rw [isClosed_coinduced, isClosed_iSup_iff, ← isClosed_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : 𝐤X → Y
⊢ Continuous[instTopologicalSpace, inst_1] f ↔
    ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)) K
have simp_rw : (∀ (i : Set X) (i_1 : IsCompact i),
    Continuous[{ IsOpen := instTopologicalSpace._aux_1 i, isOpen_univ := sorry, isOpen_inter := sorry, isOpen_sUnion := sorry },
        inst_1]
      ((f ∘ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)) ∘ Subtype.val (p := i))) ↔
  ∀ (K : Set X),
    IsCompact K →
      Continuous[instTopologicalSpaceSubtype, inst_1]
        (K.restrict (π := fun (a : X) ↦ Y) (f ∘ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)))
Tactic: simp_rw [continuous_coinduced_dom, continuous_iSup_dom, continuous_coinduced_dom,
    continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Continuous[instTopologicalSpace, inst] (⇑(CompactCoherentification.mk X).symm : (a : 𝐤X) → X)
have rw : ∀ (K : Set X),
  IsCompact K →
    ContinuousOn (Y := X)
      (Function.comp (β := 𝐤X) (⇑(CompactCoherentification.mk X).symm : (a : 𝐤X) → X)
        (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X))
      K
Tactic: rw [continuous_dom_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
hA : IsOpen[inst] A
⊢ IsOpen[instTopologicalSpace] ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) '' A)
have rw : ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)
Tactic: rw [isOpen_iff, Equiv.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
⊢ ContinuousOn (Y := 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) K
have rw : Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
  (K.restrict (π := fun (a : X) ↦ 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X))
Tactic: rw [continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → 𝐤Y
K : Set X
hK : IsCompact K
⊢ ContinuousOn f K ↔ ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) K
have refine : ∀ (H : ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) K), ContinuousOn f K
Tactic: refine ⟨fun H ↦ continuous_mk_symm.comp_continuousOn H, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
⊢ Continuous[inst, instTopologicalSpace] (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)
have rw : ∀ (s : Set X),
  Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} s →
    ContinuousOn (Y := 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) s
Tactic: rw [CompactlyCoherentSpace.isCoherentWith.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → 𝐤Y
inst_2 : CompactSpace X
⊢ Continuous[inst, instTopologicalSpace] f ↔
    Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
have rw : ContinuousOn f univ ↔ Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
Tactic: rw [← continuousOn_univ, continuousOn_rng_of_isCompact isCompact_univ, continuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → 𝐤Y
inst_2 : CompactSpace X
rw : ContinuousOn f univ ↔ Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
⊢ Continuous[inst, instTopologicalSpace] f ↔
    Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
have rw₁ : ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) univ ↔
  Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
Tactic: rw [← continuousOn_univ, continuousOn_rng_of_isCompact isCompact_univ, continuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → 𝐤Y
inst_2 : CompactSpace X
rw : ContinuousOn f univ ↔ Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
rw₁ :
  ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) univ ↔
    Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
⊢ Continuous[inst, instTopologicalSpace] f ↔
    Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
have rw₂ : Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) ↔
  Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
Tactic: rw [← continuousOn_univ, continuousOn_rng_of_isCompact isCompact_univ, continuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (CompactCoherentification.map f)
have simp_rw : ∀ (K : Set X), IsCompact K → ContinuousOn (Y := 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) K
Tactic: simp_rw [continuous_dom_iff, CompactCoherentification.map_comp_mk]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (CompactCoherentification.map f)
have hf₁ : ∀ (K : Set X), IsCompact K → ContinuousOn f K
Tactic: apply continuous_map_of_continuousOn