awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
Tactic: tfae_have 5 ↔ 7 := by
    simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, and_assoc,
      and_left_comm]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
Tactic: tfae_have 5 ↔ 8 := by
    simp only [← principal_singleton, disjoint_principal_right]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
Tactic: tfae_have 8 ↔ 9 := forall_comm.trans (by simp only [disjoint_comm, ne_comm])
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ ∀ (a : T1Space X), Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)
have simp : ∀ (a : T1Space X) (s : Set (CofiniteTopology X)),
  s = ∅ ∨ sᶜ.Finite → IsOpen[inst] ((⇑CofiniteTopology.of : (a : X) → CofiniteTopology X) ⁻¹' s)
Tactic: simp only [continuous_def, CofiniteTopology.isOpen_iff']
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst] ((⇑CofiniteTopology.of : (a : X) → CofiniteTopology X) ⁻¹' s)
have inr : IsOpen[inst] ((⇑CofiniteTopology.of : (a : X) → CofiniteTopology X) ⁻¹' sᶜ)ᶜ
Tactic: rw [← compl_compl s, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_1_to_4 : ∀ (a : T1Space X), Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)
Tactic: tfae_have 1 → 4 := by
    simp only [continuous_def, CofiniteTopology.isOpen_iff']
    rintro H s (rfl | hs)
    · exact isOpen_empty
    · rw [← compl_compl s, preimage_compl]
      exact hs.preimage (Equiv.injective _).injOn |>.isClosed.isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : ∀ (a : T1Space X), Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)
h : Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)
x : X
⊢ IsClosed[inst] {x}
have rw : IsClosed[inst]
  (preimage (β := CofiniteTopology X) (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)
    (image (α := X) (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X) {x}))
Tactic: rw [← CofiniteTopology.of.preimage_image {x}]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : ∀ (a : T1Space X), Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_4_to_2 : ∀ (a : Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)) (x : X), IsClosed[inst] {x}
Tactic: tfae_have 4 → 2 := by
    intro h x
    rw [← CofiniteTopology.of.preimage_image {x}]
    exact (Set.Finite.isClosed <| by simp) |>.preimage h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : ∀ (a : T1Space X), Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)
tfae_4_to_2 :
  ∀ (a : Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)) (x : X), IsClosed[inst] {x}
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_2_iff_10 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y
Tactic: tfae_have 2 ↔ 10 := by
    simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def,
      mem_singleton_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : ∀ (a : T1Space X), Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)
tfae_4_to_2 :
  ∀ (a : Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)) (x : X), IsClosed[inst] {x}
tfae_2_iff_10 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_10_iff_11 : (∀ ⦃x y : X⦄, x ⤳ y → x = y) ↔ T0Space X ∧ R0Space X
Tactic: tfae_have 10 ↔ 11 :=
    ⟨fun h => ⟨⟨fun _ _ h₂ => h h₂.specializes⟩, ⟨fun _ _ h₂ => specializes_of_eq (h h₂).symm⟩⟩,
      fun ⟨_, _⟩ _ _ h => (h.antisymm h.symm).eq⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : DecidableEq X
inst_3 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
⊢ ContinuousOn (update (β := fun (a : X) ↦ Y) f x y) s ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
have rw : (∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s b) ∧
    (x ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s x) ↔
  ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
Tactic: rw [ContinuousOn, ← and_forall_ne x, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : DecidableEq X
inst_3 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
⊢ (∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s b) ∧
      (x ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s x) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
have refine_1 : ∀ (H : ∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s b) (z : X)
  (hz : z ∈ s \ {x}), ContinuousWithinAt f (s \ {x}) z
Tactic: refine and_congr ⟨fun H z hz => ?_, fun H z hzx hzs => ?_⟩ (forall_congr' fun _ => ?_)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : DecidableEq X
inst_3 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
refine_1 :
  ∀ (H : ∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s b) (z : X)
    (hz : z ∈ s \ {x}), ContinuousWithinAt f (s \ {x}) z
⊢ (∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s b) ∧
      (x ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s x) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
have refine_2 : ∀ (H : ContinuousOn f (s \ {x})) (z : X) (hzx : z ≠ x) (hzs : z ∈ s),
  ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s z
Tactic: refine and_congr ⟨fun H z hz => ?_, fun H z hzx hzs => ?_⟩ (forall_congr' fun _ => ?_)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : DecidableEq X
inst_3 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
refine_1 :
  ∀ (H : ∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s b) (z : X)
    (hz : z ∈ s \ {x}), ContinuousWithinAt f (s \ {x}) z
refine_2 :
  ∀ (H : ContinuousOn f (s \ {x})) (z : X) (hzx : z ≠ x) (hzs : z ∈ s),
    ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s z
⊢ (∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s b) ∧
      (x ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s x) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
have refine_3 : x ∈ s → (ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
Tactic: refine and_congr ⟨fun H z hz => ?_, fun H z hzx hzs => ?_⟩ (forall_congr' fun _ => ?_)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : DecidableEq X
inst_3 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
H : ∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s b
z : X
hz : z ∈ s \ {x}
⊢ ContinuousWithinAt f (s \ {x}) z
have H₁ : ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s z
Tactic: specialize H z hz.2 hz.1
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : DecidableEq X
inst_3 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
z : X
hz : z ∈ s \ {x}
H : ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s z
⊢ ContinuousWithinAt f (s \ {x}) z
have H₁ : ContinuousWithinAt f s z
Tactic: rw [continuousWithinAt_update_of_ne hz.2] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : DecidableEq X
inst_3 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
H : ContinuousOn f (s \ {x})
z : X
hzx : z ≠ x
hzs : z ∈ s
⊢ ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s z
have refine_2 : ContinuousWithinAt f s z
Tactic: rw [continuousWithinAt_update_of_ne hzx]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : DecidableEq X
inst_3 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
H : ContinuousOn f (s \ {x})
z : X
hzx : z ≠ x
hzs : z ∈ s
⊢ ContinuousWithinAt f s z
have refine_2 : (fun (a : X) ↦ Membership.mem (γ := Set X) {x} a → False) ∈ 𝓝 z
Tactic: refine (H z ⟨hzs, hzx⟩).mono_of_mem_nhdsWithin (inter_mem_nhdsWithin _ ?_)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : s.Subsingleton
⊢ IsClosed[inst] s
have inl : ∀ (hs : Set.Subsingleton.{u_1} (α := X) ∅), IsClosed[inst] ∅
Tactic: rcases hs.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : s.Subsingleton
inl : ∀ (hs : Set.Subsingleton.{u_1} (α := X) ∅), IsClosed[inst] ∅
⊢ IsClosed[inst] s
have inr : ∀ (x : X) (hs : Set.Subsingleton (α := X) {x}), IsClosed[inst] {x}
Tactic: rcases hs.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
Cleared hypotheses: s, hs
-- 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 : T1Space Y
y : Y
s : Set X
h : IsClosed[inst] s
h2s : s.Nonempty
⊢ IsClosed[inst_1] (const X y '' s)
have simp_rw : IsClosed[inst_1] ((fun (a : X) ↦ y) '' s)
Tactic: simp_rw [const, h2s.image_const, isClosed_singleton]
-- 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 : T1Space Y
y : Y
s : Set X
h : IsClosed[inst] s
h2s : s.Nonempty
simp_rw : IsClosed[inst_1] ((fun (a : X) ↦ y) '' s)
⊢ IsClosed[inst_1] (const X y '' s)
have simp_rw₁ : IsClosed[inst_1] {y}
Tactic: simp_rw [const, h2s.image_const, isClosed_singleton]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
⊢ 𝓝[insert y s] x = 𝓝[s] x
have refine : ∀ (t : Set X) (ht : t ∈ 𝓝[s] x), t ∈ 𝓝[insert y s] x
Tactic: refine le_antisymm (Filter.le_def.2 fun t ht => ?_) (nhdsWithin_mono x <| subset_insert y s)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
⊢ t ∈ 𝓝[insert y s] x
have obtain : ∀ (o : Set X) (ho : IsOpen[inst] o) (hxo : x ∈ o) (host : o ∩ s ⊆ t), t ∈ 𝓝[insert y s] x
Tactic: obtain ⟨o, ho, hxo, host⟩ := mem_nhdsWithin.mp ht
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen[inst] o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ t ∈ 𝓝[insert y s] x
have refine : o \ {y} ∩ insert y s ⊆ t
Tactic: refine mem_nhdsWithin.mpr ⟨o \ {y}, ho.sdiff isClosed_singleton, ⟨hxo, hxy⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen[inst] o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ o \ {y} ∩ insert y s ⊆ t
have rw : o \ {y} ∩ s ⊆ t
Tactic: rw [inter_insert_of_notMem <| notMem_diff_of_mem (mem_singleton y)]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
⊢ insert x s ∈ 𝓝[t] x
have inl : ∀ (hu : t ⊆ insert x s), insert x s ∈ 𝓝[t] x
Tactic: rcases eq_or_ne x y with (rfl | h)
Cleared hypotheses: y, hu
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
inl : ∀ (hu : t ⊆ insert x s), insert x s ∈ 𝓝[t] x
⊢ insert x s ∈ 𝓝[t] x
have inr : ∀ (h : x ≠ y), insert x s ∈ 𝓝[t] x
Tactic: rcases eq_or_ne x y with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[t] x
have inr : insert x s ∈ 𝓝[insert y s] x
Tactic: refine nhdsWithin_mono x hu ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[insert y s] x
have inr : insert x s ∈ 𝓝[s] x
Tactic: rw [nhdsWithin_insert_of_ne h]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ insert x s =ᶠ[𝓝 x] insert x t
have simp_rw : ∀ (h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t), ∀ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t
Tactic: simp_rw [eventuallyEq_set] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t
have simp_rw : ∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t
Tactic: simp_rw [← union_singleton, ← nhdsWithin_univ, ← compl_union_self {x},
    nhdsWithin_union, eventually_sup, nhdsWithin_singleton,
    eventually_pure, union_singleton, mem_insert_iff, true_or, and_true]