awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Basic
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}
⊢ (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y

Tactic:
2 ↔ 10

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
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}
⊢ (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y

Tactic:
simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def,
      mem_singleton_iff, eq_comm]

Premises used: Set.subset_def, closure_subset_iff_isClosed, specializes_iff_mem_closure, eq_comm, Set.mem_singleton_iff
-- Module: Mathlib.Topology.Separation.Basic
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}
⊢ (∀ (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]
-- Module: Mathlib.Topology.Separation.Basic
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
⊢ ∀ ⦃x y : X⦄, x ⤳ y → x = y

Tactic:
10

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
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
⊢ T0Space X ∧ R0Space X

Tactic:
11

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
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
⊢ (∀ ⦃x y : X⦄, x ⤳ y → x = y) ↔ T0Space X ∧ R0Space X

Tactic:
10 ↔ 11

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
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
⊢ (∀ ⦃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⟩
-- Module: Mathlib.Topology.Separation.Basic
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
tfae_10_iff_11 : (∀ ⦃x y : X⦄, x ⤳ y → x = y) ↔ T0Space X ∧ R0Space 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

Tactic:
tfae_finish
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T1Space X ↔ Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X)

Tactic:
(t1Space_TFAE X).out 0 3

Premises used: t1Space_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
⊢ Continuous[inst, _] (⇑of : (a : X) → CofiniteTopology X)

Tactic:
t1Space_iff_continuous_cofinite_of.mp ‹_›

Premises used: t1Space_iff_continuous_cofinite_of, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T1Space X ↔ Pairwise fun (x y : X) ↦ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U

Tactic:
(t1Space_TFAE X).out 0 6

Premises used: t1Space_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)

Tactic:
(t1Space_TFAE X).out 0 8

Premises used: t1Space_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)

Tactic:
(t1Space_TFAE X).out 0 7

Premises used: t1Space_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y

Tactic:
(t1Space_TFAE X).out 0 9

Premises used: t1Space_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T1Space X ↔ T0Space X ∧ R0Space X

Tactic:
(t1Space_TFAE X).out 0 10

Premises used: t1Space_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
h : x ≠ y
⊢ Disjoint (pure x) (𝓝 y)

Tactic:
t1Space_iff_disjoint_pure_nhds.mp ‹_› h

Premises used: t1Space_iff_disjoint_pure_nhds, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
h : x ≠ y
⊢ Disjoint (𝓝 x) (pure y)

Tactic:
t1Space_iff_disjoint_nhds_pure.mp ‹_› h

Premises used: t1Space_iff_disjoint_nhds_pure, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
h : x ⤳ y
⊢ x = y

Tactic:
t1Space_iff_specializes_imp_eq.1 ‹_› h

Premises used: t1Space_iff_specializes_imp_eq, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
⊢ x ⤳ y ↔ x = y

Tactic:
⟨Specializes.eq, fun h => h ▸ specializes_rfl⟩

Premises used: Eq.rec, Specializes.eq, specializes_rfl, Iff.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
⊢ Eq.{u_1 + 1} (α := X → X → Prop) (fun (x1 x2 : X) ↦ x1 ⤳ x2) Eq

Tactic:
funext₂ fun _ _ => propext specializes_iff_eq

Premises used: specializes_iff_eq, funext₂, propext
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
a b : X
⊢ pure a ≤ 𝓝 b ↔ a = b

Tactic:
specializes_iff_pure.symm.trans specializes_iff_eq

Premises used: specializes_iff_eq, Iff.trans, specializes_iff_pure, Iff.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
a b : X
⊢ 𝓝 a ≤ 𝓝 b ↔ a = b

Tactic:
specializes_iff_eq

Premises used: Specializes, specializes_iff_eq
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
⊢ R0Space X

Tactic:
(t1Space_iff_t0Space_and_r0Space.mp ‹T1Space X›).right

Premises used: And.right, Iff.mp, t1Space_iff_t0Space_and_r0Space
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T0Space X
inst_2 : R0Space X
⊢ T1Space X

Tactic:
t1Space_iff_t0Space_and_r0Space.mpr ⟨‹T0Space X›, ‹R0Space X›⟩

Premises used: Iff.mpr, And.intro, t1Space_iff_t0Space_and_r0Space
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
⊢ Antitone (@T1Space X)

Tactic:
fun a _ h _ =>
  @T1Space.mk _ a fun x => (T1Space.t1 x).mono h

Premises used: T1Space.t1, IsClosed.mono, T1Space.mk, Antitone
-- Module: Mathlib.Topology.Separation.Basic
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' : X
y : Y
hne : x' ≠ x
⊢ ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s x' ↔ ContinuousWithinAt f s x'

Tactic:
EventuallyEq.congr_continuousWithinAt
    (mem_nhdsWithin_of_mem_nhds <| mem_of_superset (isOpen_ne.mem_nhds hne) fun _y' hy' =>
      Function.update_of_ne hy' _ _)
    (Function.update_of_ne hne ..)

Premises used: mem_nhdsWithin_of_mem_nhds, Filter.EventuallyEq.congr_continuousWithinAt, isOpen_ne, IsOpen.mem_nhds, Filter.mem_of_superset, Function.update_of_ne
-- Module: Mathlib.Topology.Separation.Basic
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
x x' : X
y : Y
hne : x' ≠ x
⊢ ContinuousAt (update (β := fun (a : X) ↦ Y) f x y) x' ↔ ContinuousAt f x'

Tactic:
simp only [← continuousWithinAt_univ, continuousWithinAt_update_of_ne hne]

Premises used: continuousWithinAt_univ, continuousWithinAt_update_of_ne
-- Module: Mathlib.Topology.Separation.Basic
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
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))
⊢ ContinuousOn (update (β := fun (a : X) ↦ Y) f x y) s ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))

Tactic:
rw [ContinuousOn, ← and_forall_ne x, and_comm]

Premises used: and_forall_ne, and_comm, ContinuousOn
-- Module: Mathlib.Topology.Separation.Basic
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))

Tactic:
and_congr ⟨fun H z hz => ?_, fun H z hzx hzs => ?_⟩ (forall_congr' fun _ => ?_)

Premises used: Iff.intro, forall_congr', and_congr
-- Module: Mathlib.Topology.Separation.Basic
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
refine_3 : x ∈ s → (ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 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))

Tactic:
refine and_congr ⟨fun H z hz => ?_, fun H z hzx hzs => ?_⟩ (forall_congr' fun _ => ?_)

Premises used: Iff.intro, forall_congr', and_congr
-- Module: Mathlib.Topology.Separation.Basic
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 (update (β := fun (a : X) ↦ Y) f x y) s z

Tactic:
specialize H z hz.2 hz.1

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Separation.Basic
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 z

Tactic:
rw [continuousWithinAt_update_of_ne hz.2] at H

Premises used: And.right, continuousWithinAt_update_of_ne
-- Module: Mathlib.Topology.Separation.Basic
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 f s z
⊢ ContinuousWithinAt f (s \ {x}) z

Tactic:
H.mono diff_subset

Premises used: Set.diff_subset, ContinuousWithinAt.mono
-- Module: Mathlib.Topology.Separation.Basic
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 f s z
⊢ ContinuousWithinAt f (s \ {x}) z

Tactic:
exact H.mono diff_subset

Premises used: Set.diff_subset, ContinuousWithinAt.mono
-- Module: Mathlib.Topology.Separation.Basic
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
refine_2 : ContinuousWithinAt f s z
⊢ ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s z

Tactic:
rw [continuousWithinAt_update_of_ne hzx]

Premises used: continuousWithinAt_update_of_ne
-- Module: Mathlib.Topology.Separation.Basic
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

Tactic:
(H z ⟨hzs, hzx⟩).mono_of_mem_nhdsWithin (inter_mem_nhdsWithin _ ?_)

Premises used: inter_mem_nhdsWithin, ContinuousWithinAt.mono_of_mem_nhdsWithin, And.intro
-- Module: Mathlib.Topology.Separation.Basic
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
refine_2 : (fun (a : X) ↦ Membership.mem (γ := Set X) {x} a → False) ∈ 𝓝 z
⊢ ContinuousWithinAt f s z

Tactic:
refine (H z ⟨hzs, hzx⟩).mono_of_mem_nhdsWithin (inter_mem_nhdsWithin _ ?_)

Premises used: inter_mem_nhdsWithin, ContinuousWithinAt.mono_of_mem_nhdsWithin, And.intro
-- Module: Mathlib.Topology.Separation.Basic
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
⊢ (fun (a : X) ↦ Membership.mem (γ := Set X) {x} a → False) ∈ 𝓝 z

Tactic:
isOpen_ne.mem_nhds hzx

Premises used: Set.Mem, setOf, isOpen_ne, IsOpen.mem_nhds, Set.singleton, Not
-- Module: Mathlib.Topology.Separation.Basic
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
⊢ (fun (a : X) ↦ Membership.mem (γ := Set X) {x} a → False) ∈ 𝓝 z

Tactic:
exact isOpen_ne.mem_nhds hzx

Premises used: isOpen_ne, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
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 : x ∈ s
⊢ ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y)

Tactic:
continuousWithinAt_update_same

Premises used: continuousWithinAt_update_same
-- Module: Mathlib.Topology.Separation.Basic
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 : x ∈ s
⊢ ContinuousWithinAt (update (β := fun (a : X) ↦ Y) f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y)

Tactic:
exact continuousWithinAt_update_same

Premises used: continuousWithinAt_update_same
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Injective f
hf' : Continuous[inst, inst_1] f
inst_2 : T1Space Y
⊢ T1Space X

Tactic:
t1Space_iff_specializes_imp_eq.2 fun _ _ h => hf (h.map hf').eq

Premises used: t1Space_iff_specializes_imp_eq, Iff.mpr, Specializes.eq, Specializes.map
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
f : X → Y
hf : IsEmbedding f
⊢ T1Space X

Tactic:
t1Space_of_injective_of_continuous hf.injective hf.continuous

Premises used: Topology.IsEmbedding.injective, t1Space_of_injective_of_continuous, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
h : X ≃ₜ Y
⊢ T1Space Y

Tactic:
h.symm.isEmbedding.t1Space

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.t1Space, Homeomorph.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
X : Type u
inst_1 : TopologicalSpace X
inst_2 : T1Space X
p : X → Prop
⊢ T1Space.{u} (Subtype p)

Tactic:
IsEmbedding.subtypeVal.t1Space

Premises used: Topology.IsEmbedding.t1Space, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
inst_3 : T1Space Y
⊢ T1Space (X × Y)

Tactic:
⟨fun ⟨a, b⟩ => @singleton_prod_singleton _ _ a b ▸ isClosed_singleton.prod isClosed_singleton⟩

Premises used: Eq.rec, Set.singleton_prod_singleton, T1Space.mk, IsClosed, IsClosed.prod, _private.0.instT1SpaceProd.match_1, Singleton.singleton, isClosed_singleton