awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
⊢ ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s

Tactic:
tfae_have 2 → 3 := fun h s hso hy => h (hso.mem_nhds hy)
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
⊢ ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
⊢ ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
⊢ ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
⊢ ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s

Tactic:
tfae_have 3 → 4 := fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx

Premises used: of_not_not
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
⊢ ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
⊢ ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
4 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
⊢ ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
tfae_have 4 → 5 := fun h => h _ isClosed_closure (subset_closure <| mem_singleton _)
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x})

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
6 ↔ 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
tfae_have 6 ↔ 5 := isClosed_closure.closure_subset_iff.trans singleton_subset_iff

Premises used: Set.singleton_subset_iff, IsClosed.closure_subset_iff, Iff.trans, isClosed_closure
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ ClusterPt y (pure x)

Tactic:
7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)

Tactic:
5 ↔ 7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
rw : ClusterPt y (𝓟 {x}) ↔ ClusterPt y (pure x)
rw₁ rw₂ : ClusterPt y (pure x) ↔ ClusterPt y (pure x)
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)

Tactic:
rw [mem_closure_iff_clusterPt, principal_singleton]

Premises used: mem_closure_iff_clusterPt, Filter.principal_singleton
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)

Tactic:
tfae_have 5 ↔ 7 := by
    rw [mem_closure_iff_clusterPt, principal_singleton]
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
⊢ x ⤳ y

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
⊢ ∀ (a : Membership.mem (γ := Set X) (closure[inst] {x}) y), x ⤳ y

Tactic:
5 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
⊢ ∀ (a : Membership.mem (γ := Set X) (closure[inst] {x}) y), x ⤳ y

Tactic:
fun h => (nhds_basis_opens _).ge_iff.2 ?_

Premises used: Iff.mpr, Specializes, Filter.HasBasis.ge_iff, nhds_basis_opens
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
refine : ∀ (h : Membership.mem (γ := Set X) (closure[inst] {x}) y) (i' : Set X), y ∈ i' ∧ IsOpen[inst] i' → i' ∈ 𝓝 x
⊢ ∀ (a : Membership.mem (γ := Set X) (closure[inst] {x}) y), x ⤳ y

Tactic:
refine fun h => (nhds_basis_opens _).ge_iff.2 ?_

Premises used: Iff.mpr, Filter.HasBasis.ge_iff, nhds_basis_opens
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
h : Membership.mem (γ := Set X) (closure[inst] {x}) y
s : Set X
hy : y ∈ s
ho : IsOpen[inst] s
rcases :
  ∀ (z : X) (hxs : z ∈ s) (tfae_1_to_2 : ∀ (a : z ⤳ y), pure z ≤ 𝓝 y)
    (tfae_2_to_3 : ∀ (a : pure z ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → z ∈ s)
    (tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → z ∈ s) (s : Set X), IsClosed[inst] s → z ∈ s → y ∈ s)
    (tfae_4_to_5 :
      ∀ (a : ∀ (s : Set X), IsClosed[inst] s → z ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {z}) y)
    (tfae_6_iff_5 :
      Subset (α := Set X) (closure[inst] {y}) (closure[inst] {z}) ↔ Membership.mem (γ := Set X) (closure[inst] {z}) y)
    (tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {z}) y ↔ ClusterPt y (pure z))
    (h : Membership.mem (γ := Set X) (closure[inst] {z}) y), s ∈ 𝓝 z
⊢ s ∈ 𝓝 x

Tactic:
rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩

Premises used: mem_closure_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
y : X
s : Set X
hy : y ∈ s
ho : IsOpen[inst] s
z : X
hxs : z ∈ s
tfae_1_to_2 : ∀ (a : z ⤳ y), pure z ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure z ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → z ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → z ∈ s) (s : Set X), IsClosed[inst] s → z ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → z ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {z}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {z}) ↔ Membership.mem (γ := Set X) (closure[inst] {z}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {z}) y ↔ ClusterPt y (pure z)
h : Membership.mem (γ := Set X) (closure[inst] {z}) y
⊢ s ∈ 𝓝 z

Tactic:
ho.mem_nhds hxs

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
y : X
s : Set X
hy : y ∈ s
ho : IsOpen[inst] s
z : X
hxs : z ∈ s
tfae_1_to_2 : ∀ (a : z ⤳ y), pure z ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure z ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → z ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → z ∈ s) (s : Set X), IsClosed[inst] s → z ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → z ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {z}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {z}) ↔ Membership.mem (γ := Set X) (closure[inst] {z}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {z}) y ↔ ClusterPt y (pure z)
h : Membership.mem (γ := Set X) (closure[inst] {z}) y
⊢ s ∈ 𝓝 z

Tactic:
exact ho.mem_nhds hxs

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
⊢ ∀ (a : Membership.mem (γ := Set X) (closure[inst] {x}) y), x ⤳ y

Tactic:
tfae_have 5 → 1 := by
    refine fun h => (nhds_basis_opens _).ge_iff.2 ?_
    rintro s ⟨hy, ho⟩
    rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩
    exact ho.mem_nhds hxs
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
tfae_5_to_1 : ∀ (a : Membership.mem (γ := Set X) (closure[inst] {x}) y), x ⤳ y
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s,
      Membership.mem (γ := Set X) (closure[inst] {x}) y, Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}),
      ClusterPt y (pure x)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ 𝓝 x ≤ 𝓝 y

Tactic:
Iff.rfl

Premises used: Specializes, Iff.rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ⤳ y
hd : Disjoint (𝓝 x) (𝓝 y)
⊢ ¬Disjoint (𝓝 x) (𝓝 x)

Tactic:
simp [NeBot.ne']

Premises used: Filter.NeBot.ne'
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ pure x ≤ 𝓝 y

Tactic:
(specializes_TFAE x y).out 0 1

Premises used: List.TFAE.out, OfNat.ofNat, specializes_TFAE
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
h : ∀ (x_1 : X), x_1 ∈ (𝓝 x).ker ↔ Membership.mem (γ := Set X) {y : X | y ⤳ x} x_1
⊢ (𝓝 x).ker = {y : X | y ⤳ x}

Tactic:
ext
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x x_1 : X
⊢ x_1 ∈ (𝓝 x).ker ↔ Membership.mem (γ := Set X) {y : X | y ⤳ x} x_1

Tactic:
simp [specializes_iff_pure, le_def]

Premises used: specializes_iff_pure, Filter.le_def
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s

Tactic:
(specializes_TFAE x y).out 0 2

Premises used: List.TFAE.out, OfNat.ofNat, specializes_TFAE
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : Tendsto g l (𝓝 y)
hl : ∀ (x : X), f x ⤳ g x
simp_all :
  ∀ (h : ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → g ⁻¹' s ∈ l)
    (hl : ∀ (x : X) (s : Set Y), IsOpen[inst] s → g x ∈ s → f x ∈ s) (s : Set Y), IsOpen[inst] s → y ∈ s → f ⁻¹' s ∈ l
⊢ Tendsto f l (𝓝 y)

Tactic:
simp_all only [specializes_iff_forall_open, tendsto_nhds]

Premises used: tendsto_nhds, specializes_iff_forall_open
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → g ⁻¹' s ∈ l
hl : ∀ (x : X) (s : Set Y), IsOpen[inst] s → g x ∈ s → f x ∈ s
⊢ ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → f ⁻¹' s ∈ l

Tactic:
fun s ho hy => mem_of_superset (h s ho hy) fun x hx => ?_

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → g ⁻¹' s ∈ l
hl : ∀ (x : X) (s : Set Y), IsOpen[inst] s → g x ∈ s → f x ∈ s
refine : ∀ (s : Set Y) (ho : IsOpen[inst] s) (hy : y ∈ s) (x : X) (hx : x ∈ g ⁻¹' s), x ∈ f ⁻¹' s
⊢ ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → f ⁻¹' s ∈ l

Tactic:
refine fun s ho hy => mem_of_superset (h s ho hy) fun x hx => ?_

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → g ⁻¹' s ∈ l
hl : ∀ (x : X) (s : Set Y), IsOpen[inst] s → g x ∈ s → f x ∈ s
s : Set Y
ho : IsOpen[inst] s
hy : y ∈ s
x : X
hx : x ∈ g ⁻¹' s
⊢ x ∈ f ⁻¹' s

Tactic:
mem_preimage.2 (hl x s ho (mem_preimage.1 hx))

Premises used: Iff.mpr, Iff.mp, Set.mem_preimage
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → g ⁻¹' s ∈ l
hl : ∀ (x : X) (s : Set Y), IsOpen[inst] s → g x ∈ s → f x ∈ s
s : Set Y
ho : IsOpen[inst] s
hy : y ∈ s
x : X
hx : x ∈ g ⁻¹' s
⊢ x ∈ f ⁻¹' s

Tactic:
exact mem_preimage.2 (hl x s ho (mem_preimage.1 hx))

Premises used: Iff.mpr, Iff.mp, Set.mem_preimage
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
s : Set X
h : x ⤳ y
hs : IsOpen[inst] s
hy : y ∈ s
⊢ x ∈ s

Tactic:
specializes_iff_forall_open.1 h s hs hy

Premises used: Iff.mp, specializes_iff_forall_open
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
s : Set X
hs : IsOpen[inst] s
hx : x ∉ s
hy : y ∈ s
⊢ ¬x ⤳ y

Tactic:
fun h =>
  hx <| h.mem_open hs hy

Premises used: Specializes.mem_open, Not
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s

Tactic:
(specializes_TFAE x y).out 0 3

Premises used: List.TFAE.out, OfNat.ofNat, specializes_TFAE