awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s : Set X
hs : IsCompact s
ι : Type u_3
t : Finset ι
U : ι → Set X
hU : ∀ i ∈ t, IsOpen[inst] (U i)
hsC : s ⊆ ⋃ i ∈ t, U i
empty :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X)
    (hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i))
    (hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i),
    ∃ (K : ι → Set X),
      (∀ (i : ι), IsCompact (K i)) ∧
        (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), K i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
have insert : ∀ (x : ι) (t : Finset ι) (hx : x ∉ t)
  (ih :
    ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
      ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i)
  {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ insert x t, IsOpen[inst] (U i))
  (hsC : s ⊆ ⋃ i ∈ insert x t, U i),
  ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
Tactic: induction t using Finset.induction generalizing U s with
  | empty =>
    refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
    simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC
  | insert x t hx ih =>
    simp only [Finset.set_biUnion_insert] at hsC
    simp only [Finset.forall_mem_insert] at hU
    have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
    rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
    rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
    refine ⟨update K x K₁, ?_, ?_, ?_⟩
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h1K₁]
      · simp only [update_of_ne hi, h1K]
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h2K₁]
      · simp only [update_of_ne hi, h2K]
    · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]
Cleared hypotheses: s, hs, t, U, hU, hsC
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s : Set X
hs : IsCompact s
ι : Type u_3
t : Finset ι
U : ι → Set X
hU : ∀ i ∈ t, IsOpen[inst] (U i)
hsC : s ⊆ ⋃ i ∈ t, U i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
have empty : ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X)
  (hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i))
  (hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i),
  ∃ (K : ι → Set X),
    (∀ (i : ι), IsCompact (K i)) ∧
      (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), K i
Tactic: classical
  induction t using Finset.induction generalizing U s with
  | empty =>
    refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
    simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC
  | insert x t hx ih =>
    simp only [Finset.set_biUnion_insert] at hsC
    simp only [Finset.forall_mem_insert] at hU
    have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
    rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
    rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
    refine ⟨update K x K₁, ?_, ?_, ?_⟩
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h1K₁]
      · simp only [update_of_ne hi, h1K]
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h2K₁]
      · simp only [update_of_ne hi, h2K]
    · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]
Cleared hypotheses: s, hs, t, U, hU, hsC
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s : Set X
hs : IsCompact s
ι : Type u_3
t : Finset ι
U : ι → Set X
hU : ∀ i ∈ t, IsOpen[inst] (U i)
hsC : s ⊆ ⋃ i ∈ t, U i
empty :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X)
    (hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i))
    (hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i),
    ∃ (K : ι → Set X),
      (∀ (i : ι), IsCompact (K i)) ∧
        (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), K i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
have insert : ∀ (x : ι) (t : Finset ι) (hx : x ∉ t)
  (ih :
    ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
      ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i)
  {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ insert x t, IsOpen[inst] (U i))
  (hsC : s ⊆ ⋃ i ∈ insert x t, U i),
  ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
Tactic: classical
  induction t using Finset.induction generalizing U s with
  | empty =>
    refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
    simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC
  | insert x t hx ih =>
    simp only [Finset.set_biUnion_insert] at hsC
    simp only [Finset.forall_mem_insert] at hU
    have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
    rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
    rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
    refine ⟨update K x K₁, ?_, ?_, ?_⟩
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h1K₁]
      · simp only [update_of_ne hi, h1K]
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h2K₁]
      · simp only [update_of_ne hi, h2K]
    · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]
Cleared hypotheses: s, hs, t, U, hU, hsC
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x : TopologicalSpace X := sInf T
⊢ R1Space X
have refine : ∀ (x y : X), x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
⊢ x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)
have simp : LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨ Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
Tactic: simp only [Specializes, nhds_sInf]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
⊢ LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
have pos : ∀ (hTd : ∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)),
  LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
Tactic: by_cases! hTd : ∃ t ∈ T, Disjoint (@nhds X t x) (@nhds X t y)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
pos :
  ∀ (hTd : ∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)),
    LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
      Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
⊢ LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
have neg : ∀ (hTd : ∀ (t : TopologicalSpace X) (_ : t ∈ T), ¬Disjoint (𝓝 x) (𝓝 y)),
  LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
Tactic: by_cases! hTd : ∃ t ∈ T, Disjoint (@nhds X t x) (@nhds X t y)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x_1 : TopologicalSpace X := sInf T
x y : X
hTd : ∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)
⊢ LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
have pos : ∀ (t : TopologicalSpace X) (htT : t ∈ T) (htd : Disjoint (𝓝 x) (𝓝 y)),
  LE.le.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y) ∨
    Disjoint.{u_3} (α := Filter X) (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
Tactic: rcases hTd with ⟨t, htT, htd⟩
Cleared hypotheses: hTd
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ R1Space X
have rw : R1Space X
Tactic: rw [inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ R1Space X
have ht : ∀ (i : Bool), R1Space X
Tactic: apply R1Space.iInf
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s
have hc : IsCompact (f '' K \ interior s)
Tactic: have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ SeparatedNhds {f x} (f '' K \ interior s)
have simp_rw : ∀ x_1 ∈ f '' K \ interior s, ¬Inseparable (f x) x_1
Tactic: simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,
      disjoint_nhds_nhds_iff_not_inseparable]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
⊢ False
have refine : f x ∈ interior s
Tactic: refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s
have obtain : ∀ (U V : Set Y) (Uo : IsOpen[inst_1] U) (Vo : IsOpen[inst_1] V) (hxU : {f x} ⊆ U) (hV : f '' K \ interior s ⊆ V)
  (hd : Disjoint U V), ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s
Tactic: obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' K \ interior s) := by
    simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,
      disjoint_nhds_nhds_iff_not_inseparable]
    rintro y ⟨-, hys⟩ hxy
    refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_
    rwa [mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s
have refine_1 : (f ⁻¹' V)ᶜ ∈ 𝓝 x
Tactic: refine ⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
refine_1 : (f ⁻¹' V)ᶜ ∈ 𝓝 x
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s
have refine_2 : ∀ (y : X) (hy : y ∈ K \ f ⁻¹' V), f y ∈ s
Tactic: refine ⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
⊢ (f ⁻¹' V)ᶜ ∈ 𝓝 x
have h : ∀ (a : X), Membership.mem (γ := Set X) {x : X | x ∈ f ⁻¹' U → x ∈ (f ⁻¹' V)ᶜ} a
Tactic: filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx
      using Set.disjoint_left.1 hd hx
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
h : ∀ (a : X), Membership.mem (γ := Set X) {x : X | x ∈ f ⁻¹' U → x ∈ (f ⁻¹' V)ᶜ} a
⊢ (f ⁻¹' V)ᶜ ∈ 𝓝 x
have h₁ : ∀ a ∈ f ⁻¹' U, a ∈ (f ⁻¹' V)ᶜ
Tactic: filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx
      using Set.disjoint_left.1 hd hx
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
y : X
hy : y ∈ K \ f ⁻¹' V
⊢ f y ∈ s
have refine_2 : ∀ (hys : f y ∉ s), False
Tactic: by_contra hys
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ coclosedCompact X = cocompact X
have refine : coclosedCompact X ≤ cocompact X
Tactic: refine le_antisymm ?_ cocompact_le_coclosedCompact
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ coclosedCompact X ≤ cocompact X
have rw : ∀ (i' : Set X), IsCompact i' → ∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ i'ᶜ
Tactic: rw [hasBasis_coclosedCompact.le_basis_iff hasBasis_cocompact]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ IsCompact (closure[inst] V)
have rcases : ∀ (K' : Set X) (hK' : IsCompact K') (hKK' : K ⊆ interior K'),
  ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ IsCompact (closure[inst] V)
Tactic: rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ CompletelyRegularSpace X =
    ∀ (x : X) (x_1 : Set X),
      IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ
have simp_rw : Eq (α := Prop)
  (∀ (x : X) (x_1 : Set X),
    IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ)
  (∀ (x : X) (x_1 : Set X),
    IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ)
Tactic: simp_rw +singlePass [completelyRegularSpace_iff, compl_surjective.forall, isClosed_compl_iff,
      mem_compl_iff, not_not]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
| CompletelyRegularSpace X
have tactic : ∀ (x : X) (x_1 : Set X),
  IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ
Tactic: tactic =>
    simp_rw +singlePass [completelyRegularSpace_iff, compl_surjective.forall, isClosed_compl_iff,
      mem_compl_iff, not_not]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ CompletelyRegularSpace X ↔
    ∀ (x : X) (K : Set X),
      IsOpen[inst] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
have conv_lhs : CompletelyRegularSpace X ↔
  ∀ (x : X) (K : Set X), IsOpen[inst] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
Tactic: conv_lhs => tactic =>
    simp_rw +singlePass [completelyRegularSpace_iff, compl_surjective.forall, isClosed_compl_iff,
      mem_compl_iff, not_not]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
conv_lhs :
  CompletelyRegularSpace X ↔
    ∀ (x : X) (K : Set X),
      IsOpen[inst] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
⊢ CompletelyRegularSpace X ↔
    ∀ (x : X) (K : Set X),
      IsOpen[inst] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
have conv_lhs₁ : (∀ (x : X) (x_1 : Set X),
    IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ) ↔
  ∀ (x : X) (K : Set X), IsOpen[inst] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
Tactic: conv_lhs => tactic =>
    simp_rw +singlePass [completelyRegularSpace_iff, compl_surjective.forall, isClosed_compl_iff,
      mem_compl_iff, not_not]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
⊢ RegularSpace X
have rw : ∀ {s : Set X} {a : X}, IsClosed[inst] s → a ∉ s → Disjoint (𝓝ˢ s) (𝓝 a)
Tactic: rw [regularSpace_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst] s
ha : a ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
have obtain : ∀ (f : X → (↑I : Type)) (cf : Continuous[inst, _] f) (hf : f a = 0) (hhf : EqOn f 1 s), Disjoint (𝓝ˢ s) (𝓝 a)
Tactic: obtain ⟨f, cf, hf, hhf⟩ := CompletelyRegularSpace.completely_regular a s hs ha
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst] s
ha : a ∉ s
f : X → (↑I : Type)
cf : Continuous[inst, _] f
hf : f a = 0
hhf : EqOn f 1 s
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
have apply : Disjoint (map f (𝓝ˢ s)) (map f (𝓝 a))
Tactic: apply disjoint_of_map (f := f)
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst] s
ha : a ∉ s
f : X → (↑I : Type)
cf : Continuous[inst, _] f
hf : f a = 0
hhf : EqOn f 1 s
⊢ Disjoint (map f (𝓝ˢ s)) (map f (𝓝 a))
have apply : Disjoint (𝓝 (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) 1 sorry)) (𝓝 (f a))
Tactic: apply Disjoint.mono (cf.tendsto_nhdsSet_nhds hhf) cf.continuousAt
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
⊢ CompletelyRegularSpace X
have rw : ∀ (x : X) (K : Set X), IsClosed[inst] K → x ∉ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
Tactic: rw [completelyRegularSpace_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have cx : IsClosed[inst] (closure[inst] {x})
Tactic: have cx : IsClosed (closure {x}) := isClosed_closure
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
⊢ Disjoint (closure[inst] {x}) K
have rw : closure[inst] {x} ∩ K ⊆ ∅
Tactic: rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
a : X
⊢ a ∈ closure[inst] {x} ∩ K → Membership.mem (γ := Set X) ∅ a
have this : ∀ (hax : Membership.mem (γ := Set X) (closure[inst] {x}) a) (haK : a ∈ K), Membership.mem (γ := Set X) ∅ a
Tactic: ⟨hax, haK⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have d : Disjoint (closure[inst] {x}) K
Tactic: have d : Disjoint (closure {x}) K := by
    rw [Set.disjoint_iff]
    intro a ⟨hax, haK⟩
    exact hx ((specializes_iff_mem_closure.mpr hax).symm.mem_closed hK haK)
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
d : Disjoint (closure[inst] {x}) K
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have let : ∀ (f : X → ℝ) (cf : Continuous[inst, _] f)
  (hfx : EqOn (α := X) (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 0 (closure[inst] {x}))
  (hfK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 1 K)
  (hficc :
    ∀ (x : X),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
        (({ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)),
  ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
Tactic: let ⟨⟨f, cf⟩, hfx, hfK, hficc⟩ := exists_continuous_zero_one_of_isClosed cx hK d
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
d : Disjoint (closure[inst] {x}) K
f : X → ℝ
cf : Continuous[inst, _] f
hfx : EqOn (α := X) (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 0 (closure[inst] {x})
hfK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 1 K
hficc :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
g : X → (↑I : Type) := fun (x : X) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (f x) ⋯
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have cg : Continuous[inst, _] g
Tactic: have cg : Continuous g := cf.subtype_mk hficc