awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_4
I_1 : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I_1
I : Type u_5
inst_5 : Fintype I
IH :
  ∀ {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i))
    (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : I → Set X),
      (∀ (i : I), IsClopen (C i)) ∧
        (∀ (i : I), Z i ⊆ C i) ∧
          (∀ (i : I), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
Z' : I → Set X := fun (i : I) ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst] (Z (some i))
Z'_disj : PairwiseDisjoint univ (Z ∘ some)
U : Set X := D none \ ⋃ (i : I), Z (some i)
U_open : IsOpen[inst] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun (i : I) ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : Subset.{u_4} (α := Set X) (⋃ (i : I), D' i) (⋃ (i : I), C' i)
C'_disj : PairwiseDisjoint univ C'
C0 : Set X := D none \ ⋃ (i : I), C' i
this_1 : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun (i : Option I) ↦ Option.casesOn (motive := fun (x : Option I) ↦ Set X) i C0 C'
i : I
h : Membership.mem (γ := Set (Option I)) univ (some i)
j : I
h_1 : Membership.mem (γ := Set (Option I)) univ (some j)
⊢ (C (some i) ∩ C (some j)).Nonempty → some i = some j

Tactic:
simpa using (Set.pairwiseDisjoint_iff.mp C'_disj) (by trivial) (by trivial)

Premises used: Iff.mp, Set.pairwiseDisjoint_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
⊢ RegularSpace X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
⊢ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
⊢ RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x

Tactic:
1 ↔ 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
rw :
  (∀ (b : X) (a : Set X), IsClosed[inst] aᶜ → b ∉ aᶜ → Disjoint (𝓝ˢ aᶜ) (𝓝 b)) ↔
    ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
⊢ RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x

Tactic:
rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_comm]

Premises used: Function.Surjective.forall, forall_comm, compl_surjective, regularSpace_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
⊢ (∀ (b : X) (a : Set X), IsClosed[inst] aᶜ → b ∉ aᶜ → Disjoint (𝓝ˢ aᶜ) (𝓝 b)) ↔
    ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x

Tactic:
simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _),
      (nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp,
      (nhds_basis_opens _).disjoint_iff_right, ← subset_interior_iff_mem_nhdsSet,
      interior_compl, compl_subset_compl]

Premises used: Classical.not_not, and_imp, Filter.HasBasis.disjoint_iff_right, Filter.HasBasis.le_basis_iff, and_comm, Set.compl_subset_compl, subset_interior_iff_mem_nhdsSet, interior_compl, nhds_basis_opens, Filter.HasBasis.lift'_closure, Set.mem_compl_iff, isClosed_compl_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
⊢ RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x

Tactic:
tfae_have 1 ↔ 5 := by
    rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_comm]
    simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _),
      (nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp,
      (nhds_basis_opens _).disjoint_iff_right, ← subset_interior_iff_mem_nhdsSet,
      interior_compl, compl_subset_compl]
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
⊢ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
⊢ ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
⊢ ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x

Tactic:
5 → 6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
⊢ ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x

Tactic:
tfae_have 5 → 6 := fun h a => (h a).antisymm (𝓝 _).le_lift'_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
⊢ ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
⊢ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
⊢ ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s

Tactic:
6 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
a : X
s : Set X
hs : s ∈ 𝓝 a
⊢ s ∈ (𝓝 a).lift' closure[inst]

Tactic:
rw [← H] at hs
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
a : X
s : Set X
hs : s ∈ (𝓝 a).lift' closure[inst]
rcases : ∀ (U : Set X) (hU : U ∈ 𝓝 a) (hUs : closure[inst] (id U) ⊆ s), ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s

Tactic:
rcases (𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩

Premises used: Filter.HasBasis.mem_iff, nhds, Filter.basis_sets, Iff.mp, Filter.HasBasis.lift'_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
a : X
s : Set X
hs : s ∈ (𝓝 a).lift' closure[inst]
U : Set X
hU : U ∈ 𝓝 a
hUs : closure[inst] (id U) ⊆ s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s

Tactic:
⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩

Premises used: subset_closure, closure, And.intro, Exists.intro, isClosed_closure, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
a : X
s : Set X
hs : s ∈ (𝓝 a).lift' closure[inst]
U : Set X
hU : U ∈ 𝓝 a
hUs : closure[inst] (id U) ⊆ s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s

Tactic:
exact ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
⊢ ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s

Tactic:
tfae_have 6 → 4
  | H, a, s, hs => by
    rw [← H] at hs
    rcases (𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩
    exact ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
⊢ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
⊢ ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
⊢ ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)

Tactic:
4 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
rwa : a ∈ interior sᶜ
rwa₁ rwa₂ rwa₃ rwa₄ : a ∈ (closure[inst] s)ᶜ
⊢ sᶜ ∈ 𝓝 a

Tactic:
rwa [← mem_interior_iff_mem_nhds, interior_compl]

Premises used: mem_interior_iff_mem_nhds, interior_compl
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
⊢ sᶜ ∈ 𝓝 a

Tactic:
have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
ha' : sᶜ ∈ 𝓝 a
rcases : ∀ (U : Set X) (hU : U ∈ 𝓝 a) (hUc : IsClosed[inst] U) (hUs : U ⊆ sᶜ), Disjoint (𝓝ˢ s) (𝓝 a)
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst] U
hUs : U ⊆ sᶜ
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU

Premises used: disjoint_compl_left, Filter.disjoint_of_disjoint_of_mem
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst] U
hUs : U ⊆ sᶜ
refine : Uᶜ ∈ 𝓝ˢ s
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU

Premises used: disjoint_compl_left, Filter.disjoint_of_disjoint_of_mem
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst] U
hUs : U ⊆ sᶜ
rwa : s ⊆ interior Uᶜ
rwa₁ : s ⊆ Uᶜ
rwa₂ rwa₃ rwa₄ rwa₅ : U ⊆ sᶜ
⊢ Uᶜ ∈ 𝓝ˢ s

Tactic:
rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]

Premises used: IsClosed.isOpen_compl, Set.subset_compl_comm, subset_interior_iff_mem_nhdsSet, IsOpen.interior_eq
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
⊢ ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)

Tactic:
tfae_have 4 → 2
  | H, s, a, ha => by
    have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
    rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU
    rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
⊢ ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
⊢ ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
⊢ ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
⊢ ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s

Tactic:
fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩

Premises used: Iff.intro, Iff.mp, mem_closure_iff_nhds_ne_bot
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
refine :
  ∀ (H : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (a : X) (s : Set X) (hd : Disjoint (𝓝ˢ s) (𝓝 a))
    (has : a ∈ closure[inst] s), 𝓝 a ⊓ 𝓟 s = ⊥
⊢ ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s

Tactic:
refine fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
H : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
a : X
s : Set X
hd : Disjoint (𝓝ˢ s) (𝓝 a)
has : a ∈ closure[inst] s
⊢ 𝓝 a ⊓ 𝓟 s = ⊥

Tactic:
(hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot

Premises used: Disjoint.symm, Disjoint.mono_right, Disjoint.eq_bot, principal_le_nhdsSet
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
H : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
a : X
s : Set X
hd : Disjoint (𝓝ˢ s) (𝓝 a)
has : a ∈ closure[inst] s
⊢ 𝓝 a ⊓ 𝓟 s = ⊥

Tactic:
exact (hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot

Premises used: Disjoint.symm, Disjoint.mono_right, Disjoint.eq_bot, principal_le_nhdsSet
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
⊢ ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s

Tactic:
tfae_have 2 → 3 := by
    refine fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩
    exact (hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot