awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
K : Set X
hK : IsClosed[inst] K
hyK : y ∈ K
⊢ x ∈ K
have hK₁ : IsGδ K
Tactic: apply IsClosed.isGδ at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
K : Set X
hyK : y ∈ K
hK : IsGδ K
⊢ x ∈ K
have obtain : ∀ (Ts : Set (Set X)) (hoTs : ∀ t ∈ Ts, IsOpen[inst] t) (hyK : y ∈ ⋂₀ Ts), x ∈ ⋂₀ Ts
Tactic: obtain ⟨Ts, hoTs, -, rfl⟩ := hK
Cleared hypotheses: K, hyK, hK
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
Ts : Set (Set X)
hoTs : ∀ t ∈ Ts, IsOpen[inst] t
hyK : y ∈ ⋂₀ Ts
⊢ x ∈ ⋂₀ Ts
have hyK₁ : ∀ t ∈ Ts, y ∈ t
Tactic: rw [mem_sInter] at hyK ⊢
Cleared hypotheses: hyK
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T2Space X ↔ Pairwise fun (x y : X) ↦ Disjoint (𝓝 x) (𝓝 y)
have refine : ∀ (x y : X),
  x ≠ y →
    ((fun (x y : X) ↦ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) x y ↔
      (fun (x y : X) ↦ Disjoint (𝓝 x) (𝓝 y)) x y)
Tactic: refine (t2Space_iff X).trans (forall₃_congr fun x y _ => ?_)
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ T2Space X ↔ T0Space X
have mp : T2Space X → T0Space X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
mp : T2Space X → T0Space X
⊢ T2Space X ↔ T0Space X
have mpr : T0Space X → T2Space X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap π
⊢ T2Space Y ↔ IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}
have rw : IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}
Tactic: rw [t2_iff_isClosed_diagonal]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap π
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}
have h₁ : IsOpenQuotientMap (Prod.map π π)
Tactic: replace h := IsOpenQuotientMap.prodMap h h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}
have refine : ∀ (H : IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}), IsClosed[instTopologicalSpaceProd] (diagonal Y)
Tactic: refine ⟨fun H ↦ H.preimage h.continuous, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y)
have simp_rw : ∀ (H : IsOpen[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}ᶜ), IsOpen[instTopologicalSpaceProd] (diagonal Y)ᶜ
Tactic: simp_rw [← isOpen_compl_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsOpen[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}ᶜ
⊢ IsOpen[instTopologicalSpaceProd] (diagonal Y)ᶜ
have h₁ : (diagonal Y)ᶜ = Prod.map π π '' {q : X × X | π q.1 = π q.2}ᶜ
Tactic: convert! h.isOpenMap _ H
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t
have refine : 𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)
Tactic: refine le_antisymm (nhdsSet_inter_le _ _) ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)
have simp_rw : LE.le.{u_1} (α := Filter X) (⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2) (⨆ a ∈ s ∩ t, 𝓝 a)
Tactic: simp_rw [hs.nhdsSet_inf_eq_biSup, ht.inf_nhdsSet_eq_biSup, nhdsSet, sSup_image]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ LE.le.{u_1} (α := Filter X) (⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2) (⨆ a ∈ s ∩ t, 𝓝 a)
have refine : ∀ (x : X) (hxs : x ∈ s) (y : X) (hyt : y ∈ t), 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a
Tactic: refine iSup₂_le fun x hxs ↦ iSup₂_le fun y hyt ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a
have inl : ∀ (hyt : x ∈ t), 𝓝 x ⊓ 𝓝 x ≤ ⨆ a ∈ s ∩ t, 𝓝 a
Tactic: rcases eq_or_ne x y with (rfl | hne)
Cleared hypotheses: y, hyt
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
inl : ∀ (hyt : x ∈ t), 𝓝 x ⊓ 𝓝 x ≤ ⨆ a ∈ s ∩ t, 𝓝 a
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a
have inr : ∀ (hne : x ≠ y), 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a
Tactic: rcases eq_or_ne x y with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2
have inl : (x, x) ∈ s ×ˢ s → ∀ (hx : (x, x).1 ∈ s) (hy : (x, x).2 ∈ s), ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2
Tactic: rcases eq_or_ne x y with rfl | hne
Cleared hypotheses: y, h, hx, hy
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
inl : (x, x) ∈ s ×ˢ s → ∀ (hx : (x, x).1 ∈ s) (hy : (x, x).2 ∈ s), ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2
have inr : ∀ (hne : x ≠ y), ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2
Tactic: rcases eq_or_ne x y with rfl | hne
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x : X
h : (x, x) ∈ s ×ˢ s
hx : (x, x).1 ∈ s
hy : (x, x).2 ∈ s
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2
have inl : ∀ (u : Set X) (hu : u ∈ 𝓝 x) (hf : InjOn f u), ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2
Tactic: rcases loc x hx with ⟨u, hu, hf⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2
have inr : ∀ᶠ (z : X × X) in 𝓝 (x, y), f z.1 ≠ f z.2
Tactic: suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ ∀ᶠ (z : X × X) in 𝓝 (x, y), f z.1 ≠ f z.2
have inr : Prod.map f f (x, y) ∈ (diagonal Y)ᶜ
Tactic: refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t
have this : ∀ x ∈ s ×ˢ s, ∀ᶠ (y : X × X) in 𝓝 x, f y.1 = f y.2 → y.1 = y.2
Tactic: have : ∀ x ∈ s ×ˢ s, ∀ᶠ y in 𝓝 x, f y.1 = f y.2 → y.1 = y.2 := fun (x, y) ⟨hx, hy⟩ ↦ by
    rcases eq_or_ne x y with rfl | hne
    · rcases loc x hx with ⟨u, hu, hf⟩
      exact Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf
    · suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne
      refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_
      exact inj.ne hx hy hne
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
this : ∀ x ∈ s ×ˢ s, ∀ᶠ (y : X × X) in 𝓝 x, f y.1 = f y.2 → y.1 = y.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t
have this₁ : ∀ᶠ (x : X × X) in 𝓝ˢ s ×ˢ 𝓝ˢ s, f x.1 = f x.2 → x.1 = x.2
Tactic: rw [← eventually_nhdsSet_iff_forall, sc.nhdsSet_prod_eq sc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
⊢ IsOpen[inst] U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)
have rw : (∀ x ∈ U, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → U ∈ l) ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)
Tactic: rw [isOpen_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
⊢ (∀ x ∈ U, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → U ∈ l) ↔
    ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)
have refine : (∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)) → ∀ x ∈ U, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → U ∈ l
Tactic: refine ⟨fun h F hF => h F.lim hF F F.le_nhds_lim, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)
x : X
hx : x ∈ U
f : Ultrafilter X
h : (↑f : Filter X) ≤ 𝓝 x
⊢ U ∈ f
have hx₁ : f.lim ∈ U
Tactic: rw [← Ultrafilter.lim_eq_iff_le_nhds.2 h] at hx
Cleared hypotheses: hx, h
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
⊢ T2Space (X ⊕ Y)
have t2 : Pairwise fun (x y : X ⊕ Y) ↦
  ∃ (u : Set (X ⊕ Y)) (v : Set (X ⊕ Y)),
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
⊢ T2Space ((i : ι) × X i)
have t2 : Pairwise fun (x y : (i : ι) × X i) ↦
  ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x : X i
j : ι
y : X j
ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) j y
⊢ ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) j y ∈ v ∧ Disjoint u v
have t2 : ∀ (y : X i) (ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) i y),
  ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) i y ∈ v ∧ Disjoint u v
Tactic: rcases eq_or_ne i j with (rfl | h)
Cleared hypotheses: j, y, ne
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x : X i
j : ι
y : X j
ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) j y
t2 :
  ∀ (y : X i) (ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) i y),
    ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
      IsOpen[instTopologicalSpaceSigma] u ∧
        IsOpen[instTopologicalSpaceSigma] v ∧
          mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) i y ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) j y ∈ v ∧ Disjoint u v
have t2₁ : ∀ (h : i ≠ j),
  ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) j y ∈ v ∧ Disjoint u v
Tactic: rcases eq_or_ne i j with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x y : X i
ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) i y
⊢ ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) i y ∈ v ∧ Disjoint u v
have ne₁ : x ≠ y
Tactic: replace ne : x ≠ y := ne_of_apply_ne _ ne
Cleared hypotheses: ne
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x : X i
j : ι
y : X j
ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) j y
h : i ≠ j
x_1 : TopologicalSpace ι := ⊥
⊢ ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) j y ∈ v ∧ Disjoint u v
have this : DiscreteTopology ι
Tactic: have : DiscreteTopology ι := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
⊢ T2Space.{u_1} (T2Quotient X)
have rw : Pairwise fun (x y : T2Quotient X) ↦
  ∃ (u : Set (T2Quotient X)) (v : Set (T2Quotient X)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Tactic: rw [t2Space_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
i : T2Quotient X
x : X
j : T2Quotient X
y : X
h : ¬Eq (α := T2Quotient X) (mk x) (mk y)
⊢ ∃ (u : Set (T2Quotient X)) (v : Set (T2Quotient X)),
    IsOpen u ∧
      IsOpen v ∧
        Quot.mk (⇑(t2Setoid X) : X → X → Prop) x ∈ u ∧ Quot.mk (⇑(t2Setoid X) : X → X → Prop) y ∈ v ∧ Disjoint u v
have mk : ∀ (s : Setoid X) (hs : T2Space.{u_1} (Quotient s)) (hsxy : ⟦x⟧ ≠ ⟦y⟧),
  ∃ (u : Set (T2Quotient X)) (v : Set (T2Quotient X)),
    IsOpen u ∧
      IsOpen v ∧
        Quot.mk (⇑(t2Setoid X) : X → X → Prop) x ∈ u ∧ Quot.mk (⇑(t2Setoid X) : X → X → Prop) y ∈ v ∧ Disjoint u v
Tactic: obtain ⟨s, hs, hsxy⟩ : ∃ s, T2Space (Quotient s) ∧ Quotient.mk s x ≠ Quotient.mk s y := by
    simpa [T2Quotient.mk_eq, Quotient.eq] using h
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
g : T2Quotient X → Y
hfg : g ∘ mk = f
⊢ g = lift hf
have apply : ∀ (x : X), (g ∘ mk) x = (lift hf ∘ mk) x
Tactic: apply surjective_mk X |>.right_cancellable |>.mp <| funext _
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure[inst] s
x : X
hx : x ∈ t
⊢ f x = g x
have this : (𝓝[s] x).NeBot
Tactic: have : (𝓝[s] x).NeBot := mem_closure_iff_clusterPt.mp (hts hx)
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
hst : Disjoint s t
⊢ SeparatedNhds s t
have simp : ∀ (hst : s ×ˢ t ⊆ (diagonal X)ᶜ),
  ∃ (U : Set X) (V : Set X), IsOpen[inst] U ∧ IsOpen[inst] V ∧ s ⊆ U ∧ t ⊆ V ∧ U ×ˢ V ⊆ (diagonal X)ᶜ
Tactic: simp only [SeparatedNhds, prod_subset_compl_diagonal_iff_disjoint.symm] at hst ⊢
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s t : Set X
H1 : IsClosed[inst] s
H2 : IsCompact (closure[inst] sᶜ)
H3 : IsClosed[inst] t
H4 : Disjoint s t
⊢ SeparatedNhds s t
have ht : IsCompact t
Tactic: have ht : IsCompact t := .of_isClosed_subset H2 H3 <| H4.subset_compl_left.trans subset_closure
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s t : Set X
H1 : IsClosed[inst] s
H2 : IsCompact (closure[inst] sᶜ)
H3 : IsClosed[inst] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds s t
have rw : SeparatedNhds (s \ interior s ∪ interior s) t
Tactic: rw [← diff_union_of_subset (interior_subset (s := s))]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s t : Set X
H1 : IsClosed[inst] s
H2 : IsCompact (closure[inst] sᶜ)
H3 : IsClosed[inst] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s \ interior s ∪ interior s) t
have refine : SeparatedNhds (s \ interior s) t
Tactic: refine .union_left ?_ ⟨interior s, sᶜ, isOpen_interior, H1.isOpen_compl, le_rfl,
    H4.subset_compl_left, disjoint_compl_right.mono_left interior_subset⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s t : Set X
H1 : IsClosed[inst] s
H2 : IsCompact (closure[inst] sᶜ)
H3 : IsClosed[inst] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s \ interior s) t
have rw : SeparatedNhds (s ∩ closure[inst] sᶜ) t
Tactic: rw [← H1.frontier_eq, frontier_eq_closure_inter_closure, H1.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s t : Set X
H1 : IsClosed[inst] s
H2 : IsCompact (closure[inst] sᶜ)
H3 : IsClosed[inst] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s ∩ closure[inst] sᶜ) t
have refine : IsCompact (s ∩ closure[inst] sᶜ)
Tactic: refine .of_isCompact_isCompact_isClosed ?_ ht H3 (disjoint_of_subset_left inter_subset_left H4)
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : s.Finite
ht : t.Finite
h : Disjoint s t
⊢ SeparatedNhds s t
have rw : SeparatedNhds (↑(hs.toFinset (s := s)) : Set X) (↑(ht.toFinset (s := t)) : Set X)
Tactic: rw [← hs.coe_toFinset, ← ht.coe_toFinset]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), T2Space.{u_5} (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact s ↔ IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)
have mp : IsCompact s → IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), T2Space.{u_5} (X i)
s : Set ((i : ι) → X i)
mp : IsCompact s → IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)
⊢ IsCompact s ↔ IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)
have mpr : (IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)) → IsCompact s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), R1Space.{u_5} (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact (closure[topologicalSpace] s) ↔ ∀ (i : ι), IsCompact (closure[inst i] (eval (β := X) i '' s))
have simp_rw : (∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K) ↔
  ∀ (i : ι), ∃ (K : Set (X i)), IsCompact K ∧ eval (β := X) i '' s ⊆ K
Tactic: simp_rw [← exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), R1Space.{u_5} (X i)
s : Set ((i : ι) → X i)
simp_rw :
  (∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K) ↔
    ∀ (i : ι), ∃ (K : Set (X i)), IsCompact K ∧ eval (β := X) i '' s ⊆ K
⊢ IsCompact (closure[topologicalSpace] s) ↔ ∀ (i : ι), IsCompact (closure[inst i] (eval (β := X) i '' s))
have simp_rw₁ : (∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki) ↔
  ∀ (i : ι), ∃ (K : Set (X i)), IsCompact K ∧ eval (β := X) i '' s ⊆ K
Tactic: simp_rw [← exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ f x ≠ g x ↔ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
have mp : f x ≠ g x → ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
mp : f x ≠ g x → ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
⊢ f x ≠ g x ↔ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
have mpr : (∀ᶠ (x : X) in 𝓝 x, f x ≠ g x) → f x ≠ g x
Tactic: constructor