awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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)
tfae_2_to_3 :
  ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x].TFAE
have tfae_3_to_1 : ∀ (a : ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s), RegularSpace X
Tactic: tfae_have 3 → 1 := fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
⊢ RegularSpace X ↔ ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
have refine : ∀ (h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)) {t : Set X} {a : X} (ht : IsClosed[inst] t) (ha : a ∉ t),
  Disjoint (𝓝ˢ t) (𝓝 a)
Tactic: refine ⟨fun _ t ht a ha => RegularSpace.regular
    (h ▸ isOpen_generateFrom_of_mem ht).isClosed_compl
    (Set.notMem_compl_iff.mpr ha), fun h' => ⟨fun {t a} ht ha => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
t : Set X
a : X
ht : IsClosed[inst] t
ha : a ∉ t
⊢ Disjoint (𝓝ˢ t) (𝓝 a)
have obtain : ∀ (t : Set X) (ht : IsClosed[inst] tᶜ) (ha : a ∉ tᶜ), Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Tactic: obtain ⟨t, rfl⟩ := compl_involutive.surjective t
Cleared hypotheses: t, ht, ha
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsClosed[inst] tᶜ
ha : a ∉ tᶜ
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
have ht₁ : IsOpen[generateFrom s] t
Tactic: rw [isClosed_compl_iff, h] at ht
Cleared hypotheses: ht, ha
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[generateFrom s] t
ha : a ∉ tᶜ
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
have ha₁ : a ∈ t
Tactic: rw [Set.notMem_compl_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
S : Set (Set X)
h_1 : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, ∀ (ha : a ∈ s), Disjoint (𝓝ˢ sᶜ) (𝓝 a)
ha : a ∈ ⋃₀ S
⊢ Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)
have sUnion : ∀ (t : Set X) (ht : t ∈ S) (ha : a ∈ t), Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)
Tactic: obtain ⟨t, ht, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t_1 : Set X
S : Set (Set X)
h_1 : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, ∀ (ha : a ∈ s), Disjoint (𝓝ˢ sᶜ) (𝓝 a)
t : Set X
ht : t ∈ S
ha : a ∈ t
⊢ Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)
have sUnion : Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Tactic: grw [compl_sUnion, sInter_image, iInter₂_subset t ht]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[generateFrom s] t
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
have basic : ∀ (t : Set X) (ht : t ∈ s) (ha : a ∈ t), Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Tactic: induction ht with
  | basic t ht => exact h' t ht a ha
  | univ => simp
  | inter t₁ t₂ _ _ ih₁ ih₂ => grind [compl_inter, nhdsSet_union, disjoint_sup_left]
  | sUnion S _ ih =>
    obtain ⟨t, ht, ha⟩ := ha
    grw [compl_sUnion, sInter_image, iInter₂_subset t ht]
    exact ih t ht ha
Cleared hypotheses: ht, ha
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[generateFrom s] t
ha : a ∈ t
basic : ∀ (t : Set X) (ht : t ∈ s) (ha : a ∈ t), Disjoint (𝓝ˢ tᶜ) (𝓝 a)
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
have univ : ∀ (ha : Membership.mem (γ := Set X) univ a), Disjoint (𝓝ˢ univᶜ) (𝓝 a)
Tactic: induction ht with
  | basic t ht => exact h' t ht a ha
  | univ => simp
  | inter t₁ t₂ _ _ ih₁ ih₂ => grind [compl_inter, nhdsSet_union, disjoint_sup_left]
  | sUnion S _ ih =>
    obtain ⟨t, ht, ha⟩ := ha
    grw [compl_sUnion, sInter_image, iInter₂_subset t ht]
    exact ih t ht ha
Cleared hypotheses: ht, ha
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[generateFrom s] t
ha : a ∈ t
basic : ∀ (t : Set X) (ht : t ∈ s) (ha : a ∈ t), Disjoint (𝓝ˢ tᶜ) (𝓝 a)
univ : ∀ (ha : Membership.mem (γ := Set X) Set.univ a), Disjoint (𝓝ˢ Set.univᶜ) (𝓝 a)
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
have inter : ∀ (t₁ t₂ : Set X),
  GenerateOpen s t₁ →
    GenerateOpen s t₂ →
      ∀ (ih₁ : ∀ (ha : a ∈ t₁), Disjoint (𝓝ˢ t₁ᶜ) (𝓝 a)) (ih₂ : ∀ (ha : a ∈ t₂), Disjoint (𝓝ˢ t₂ᶜ) (𝓝 a))
        (ha : a ∈ t₁ ∩ t₂), Disjoint (𝓝ˢ (t₁ ∩ t₂)ᶜ) (𝓝 a)
Tactic: induction ht with
  | basic t ht => exact h' t ht a ha
  | univ => simp
  | inter t₁ t₂ _ _ ih₁ ih₂ => grind [compl_inter, nhdsSet_union, disjoint_sup_left]
  | sUnion S _ ih =>
    obtain ⟨t, ht, ha⟩ := ha
    grw [compl_sUnion, sInter_image, iInter₂_subset t ht]
    exact ih t ht ha
Cleared hypotheses: ht, ha
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[generateFrom s] t
ha : a ∈ t
basic : ∀ (t : Set X) (ht : t ∈ s) (ha : a ∈ t), Disjoint (𝓝ˢ tᶜ) (𝓝 a)
univ : ∀ (ha : Membership.mem (γ := Set X) Set.univ a), Disjoint (𝓝ˢ Set.univᶜ) (𝓝 a)
inter :
  ∀ (t₁ t₂ : Set X),
    GenerateOpen s t₁ →
      GenerateOpen s t₂ →
        ∀ (ih₁ : ∀ (ha : a ∈ t₁), Disjoint (𝓝ˢ t₁ᶜ) (𝓝 a)) (ih₂ : ∀ (ha : a ∈ t₂), Disjoint (𝓝ˢ t₂ᶜ) (𝓝 a))
          (ha : a ∈ t₁ ∩ t₂), Disjoint (𝓝ˢ (t₁ ∩ t₂)ᶜ) (𝓝 a)
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
have sUnion : ∀ (S : Set (Set X)),
  (∀ s_1 ∈ S, GenerateOpen s s_1) →
    ∀ (ih : ∀ s ∈ S, ∀ (ha : a ∈ s), Disjoint (𝓝ˢ sᶜ) (𝓝 a)) (ha : a ∈ ⋃₀ S), Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)
Tactic: induction ht with
  | basic t ht => exact h' t ht a ha
  | univ => simp
  | inter t₁ t₂ _ _ ih₁ ih₂ => grind [compl_inter, nhdsSet_union, disjoint_sup_left]
  | sUnion S _ ih =>
    obtain ⟨t, ht, ha⟩ := ha
    grw [compl_sUnion, sInter_image, iInter₂_subset t ht]
    exact ih t ht ha
Cleared hypotheses: ht, ha
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
⊢ Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
have h : RegularSpace X ↔ ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
Tactic: have h := (regularSpace_TFAE X).out 0 2
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
x_1 x_2 : X
h : ¬x_1 ⤳ x_2
⊢ Disjoint (𝓝 x_1) (𝓝 x_2)
have rwa : Disjoint (𝓝ˢ {x_1}) (𝓝 x_2)
Tactic: rwa [← nhdsSet_singleton, disjoint_nhdsSet_nhds, ← specializes_iff_mem_closure]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
x_1 x_2 : X
h : ¬x_1 ⤳ x_2
rwa : Disjoint (𝓝ˢ {x_1}) (𝓝 x_2)
⊢ Disjoint (𝓝 x_1) (𝓝 x_2)
have rwa₁ : x_2 ∉ closure[inst] {x_1}
Tactic: rwa [← nhdsSet_singleton, disjoint_nhdsSet_nhds, ← specializes_iff_mem_closure]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
have h' : RegularSpace X ↔ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
Tactic: have h' := (regularSpace_TFAE X).out 0 3
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U
have hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
Tactic: have hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ) := by
    simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
      ← subset_interior_iff_mem_nhdsSet] using hU
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U
have rcases : ∀ (V : Set X) (hVo : IsOpen[inst] V) (hKV : K ⊆ V) (W : Set X) (hVW : Disjoint V W) (hW : IsOpen[inst] W)
  (hUW : Uᶜ ⊆ W), ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U
Tactic: rcases ((hasBasis_nhdsSet _).disjoint_iff (hasBasis_nhdsSet _)).1 hd
    with ⟨V, ⟨hVo, hKV⟩, W, ⟨hW, hUW⟩, hVW⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
V : Set X
hVo : IsOpen[inst] V
hKV : K ⊆ V
W : Set X
hVW : Disjoint V W
hW : IsOpen[inst] W
hUW : Uᶜ ⊆ W
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U
have refine : closure[inst] V ⊆ Wᶜ
Tactic: refine ⟨V, hVo, hKV, Subset.trans ?_ (compl_subset_comm.1 hUW)⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).lift' closure[inst] = 𝓝ˢ K
have refine : ∀ (U : Set X) (hU : U ∈ 𝓝ˢ K), U ∈ (𝓝ˢ K).lift' closure[inst]
Tactic: refine le_antisymm (fun U hU ↦ ?_) (le_lift'_closure _)
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
⊢ U ∈ (𝓝ˢ K).lift' closure[inst]
have rcases : ∀ (V : Set X) (hVo : IsOpen[inst] V) (hKV : K ⊆ V) (hVU : closure[inst] V ⊆ U), U ∈ (𝓝ˢ K).lift' closure[inst]
Tactic: rcases hK.exists_isOpen_closure_subset hU with ⟨V, hVo, hKV, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (𝓝 b).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 (f b) ∧ IsClosed[inst] s) fun (i : Set X) ↦ f ⁻¹' id i
have rw : (comap f (𝓝 (f b))).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 (f b) ∧ IsClosed[inst] s) fun (i : Set X) ↦ f ⁻¹' id i
Tactic: rw [hf.nhds_eq_comap b]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
a : X
⊢ (𝓝 a).HasBasis
    (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
          If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
            IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
              (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
    fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
    ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
      If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i
have rw : HasBasis (α := X) (⨅ (i : (↑T : Type u_3)), 𝓝 a)
  (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
    If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
      ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
        If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
          IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
            (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
  fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
  ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
    If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i
Tactic: rw [nhds_sInf, ← iInf_subtype'']
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
⊢ RegularSpace X
have this : ∀ (a : X),
  (𝓝 a).HasBasis
    (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
          If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
            IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
              (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
    fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
    ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
      If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i
Tactic: have : ∀ a, (𝓝 a).HasBasis
      (fun If : Σ I : Set T, I → Set X =>
        If.1.Finite ∧ ∀ i : If.1, If.2 i ∈ @nhds X i a ∧ @IsClosed X i (If.2 i))
      fun If => ⋂ i : If.1, If.snd i := fun a ↦ by
    rw [nhds_sInf, ← iInf_subtype'']
    exact .iInf fun t : T => @closed_nhds_basis X t (h t t.2) a
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis
      (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
        If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
          ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
            If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
              IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
                (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
      fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
        If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i
⊢ RegularSpace X
have refine : ∀ (a : X) (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X))
  (hIf :
    If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
      ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
        If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
          IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
            (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
  (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
  IsClosed[sInf T] (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i)
Tactic: refine .of_hasBasis this fun a If hIf => isClosed_iInter fun i => ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : RegularSpace X
h₂ : RegularSpace X
⊢ RegularSpace X
have rw : RegularSpace X
Tactic: rw [inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
⊢ _root_.HasSeparatingCover s t
have inl : ∀ (empty_X : IsEmpty X), _root_.HasSeparatingCover s t
Tactic: rcases isEmpty_or_nonempty X with empty_X | nonempty_X
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
inl : ∀ (empty_X : IsEmpty X), _root_.HasSeparatingCover s t
⊢ _root_.HasSeparatingCover s t
have inr : ∀ (nonempty_X : Nonempty X), _root_.HasSeparatingCover s t
Tactic: rcases isEmpty_or_nonempty X with empty_X | nonempty_X
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
empty_X : IsEmpty X
⊢ _root_.HasSeparatingCover s t
have inl : _root_.HasSeparatingCover ∅ t
Tactic: rw [subset_eq_empty (t := s) (fun ⦃_⦄ _ ↦ trivial) (univ_eq_empty_iff.mpr empty_X)]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
⊢ ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)
have inr : ∀
  (this :
    ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s)
      (t_cl : IsClosed t) (st_dis : Disjoint s t) (nonempty_X : Nonempty X) (a : X) (ains : a ∈ s),
      ∃ (n : Set X), IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n))
  (ains : a ∉ s), ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)
Tactic: wlog ains : a ∈ s
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
inr :
  ∀
    (this :
      ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s)
        (t_cl : IsClosed t) (st_dis : Disjoint s t) (nonempty_X : Nonempty X) (a : X) (ains : a ∈ s),
        ∃ (n : Set X), IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n))
    (ains : a ∉ s), ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)
⊢ ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)
have wlog : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s)
  (t_cl : IsClosed t) (st_dis : Disjoint s t) (nonempty_X : Nonempty X) (a : X) (ains : a ∈ s),
  ∃ (n : Set X), IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)
Tactic: wlog ains : a ∈ s
Cleared hypotheses: s, t, inst_1, inst_2, s_cl, t_cl, st_dis, nonempty_X, a
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
s t : Set X
inst_2 : LindelofSpace X
inst_3 : RegularSpace X
s_cl : IsClosed[inst_1] s
t_cl : IsClosed[inst_1] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
⊢ ∃ (n : Set X), IsOpen[inst_1] n ∧ Disjoint (closure[inst_1] n) t ∧ (a ∈ s → a ∈ n)
have obtain : ∀ (n : Set X) (nna : n ∈ 𝓝 a) (ncl : IsClosed[inst_1] n) (nsubkc : n ⊆ tᶜ),
  ∃ (n : Set X), IsOpen[inst_1] n ∧ Disjoint (closure[inst_1] n) t ∧ (a ∈ s → a ∈ n)
Tactic: obtain ⟨n, nna, ncl, nsubkc⟩ := ((regularSpace_TFAE X).out 0 3 :).mp ‹RegularSpace X› a tᶜ <|
      t_cl.compl_mem_nhds (disjoint_left.mp st_dis ains)
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
⊢ _root_.HasSeparatingCover s t
have this : ∀ (a : X), ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)
Tactic: have (a : X) : ∃ n : Set X, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n) := by
    wlog ains : a ∈ s
    · exact ⟨∅, isOpen_empty, SeparatedNhds.empty_left t |>.disjoint_closure_left, fun a ↦ ains a⟩
    obtain ⟨n, nna, ncl, nsubkc⟩ := ((regularSpace_TFAE X).out 0 3 :).mp ‹RegularSpace X› a tᶜ <|
      t_cl.compl_mem_nhds (disjoint_left.mp st_dis ains)
    exact
      ⟨interior n,
       isOpen_interior,
       disjoint_left.mpr fun ⦃_⦄ ain ↦
         nsubkc <| (IsClosed.closure_subset_iff ncl).mpr interior_subset ain,
       fun _ ↦ mem_interior_iff_mem_nhds.mpr nna⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
this : ∀ (a : X), ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)
⊢ _root_.HasSeparatingCover s t
have inr : ∀ (u : (a : X) → Set X) (u_open : ∀ (a : X), IsOpen[inst] (u a)) (u_dis : ∀ (a : X), Disjoint (closure[inst] (u a)) t)
  (u_nhds : ∀ a ∈ s, a ∈ u a), _root_.HasSeparatingCover s t
Tactic: choose u u_open u_dis u_nhds using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
u : (a : X) → Set X
u_open : ∀ (a : X), IsOpen[inst] (u a)
u_dis : ∀ (a : X), Disjoint (closure[inst] (u a)) t
u_nhds : ∀ a ∈ s, a ∈ u a
⊢ _root_.HasSeparatingCover s t
have inr : ∀ (f : ℕ → X) (f_cov : s ⊆ ⋃ (n : ℕ), u (f n)), _root_.HasSeparatingCover s t
Tactic: obtain ⟨f, f_cov⟩ := s_cl.isLindelof.indexed_countable_subcover
    u u_open (fun a ainh ↦ mem_iUnion.mpr ⟨a, u_nhds a ainh⟩)
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x y : X
h : ¬Inseparable x y
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
have rcases : ∀ (U₁ U₂ : Set X) (U₁_op : IsOpen[inst] U₁) (U₂_op : IsOpen[inst] U₂) (x_in : x ∈ U₁) (y_in : y ∈ U₂)
  (H : Disjoint U₁ U₂),
  ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
Tactic: rcases r1_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩