awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
motive : T2Quotient X → T2Quotient Y → Prop
q : T2Quotient X
q' : T2Quotient Y
h : ∀ (x : X) (y : Y), motive (mk x) (mk y)
⊢ motive q q'

Tactic:
Quotient.inductionOn₂ q q' h

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
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
⊢ T2Space.{u_1} (T2Quotient X)

Tactic:
rw [t2Space_iff]

Premises used: t2Space_iff
-- Module: Mathlib.Topology.Separation.Hausdorff
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)
⊢ ∃ (s : Setoid X), T2Space.{u_1} (Quotient s) ∧ ⟦x⟧ ≠ ⟦y⟧

Tactic:
simpa [T2Quotient.mk_eq, Quotient.eq] using h

Premises used: T2Quotient.mk_eq, Quotient.eq
-- Module: Mathlib.Topology.Separation.Hausdorff
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) (T2Quotient.mk x) (T2Quotient.mk y)
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
⊢ ∃ (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
-- Module: Mathlib.Topology.Separation.Hausdorff
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)
s : Setoid X
hs : T2Space.{u_1} (Quotient s)
hsxy : ⟦x⟧ ≠ ⟦y⟧
⊢ Membership.mem (γ := Set (Setoid X)) {s : Setoid X | T2Space.{u_1} (Quotient s)} s

Tactic:
hs

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.Separation.Hausdorff
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)
s : Setoid X
hs : T2Space.{u_1} (Quotient s)
hsxy : ⟦x⟧ ≠ ⟦y⟧
⊢ Membership.mem (γ := Set (Setoid X)) {s : Setoid X | T2Space.{u_1} (Quotient s)} s

Tactic:
exact hs
-- Module: Mathlib.Topology.Separation.Hausdorff
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)
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:
exact separated_by_continuous (continuous_map_sInf (by exact hs)) hsxy
-- Module: Mathlib.Topology.Separation.Hausdorff
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
⊢ t2Setoid X ≤ Setoid.ker f

Tactic:
sInf_le <| .of_injective_continuous
    (Setoid.kerLift_injective _) (hf.quotient_lift fun _ _ ↦ id)

Premises used: T2Space.of_injective_continuous, Setoid.kerLift_injective, sInf_le, Continuous.quotient_lift
-- Module: Mathlib.Topology.Separation.Hausdorff
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
⊢ t2Setoid X ≤ Setoid.ker f

Tactic:
exact sInf_le <| .of_injective_continuous
    (Setoid.kerLift_injective _) (hf.quotient_lift fun _ _ ↦ id)

Premises used: sInf_le
-- Module: Mathlib.Topology.Separation.Hausdorff
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
⊢ Continuous[_, inst_1] (lift hf)

Tactic:
continuous_coinduced_dom.mpr hf

Premises used: Iff.mpr, continuous_coinduced_dom, T2Quotient
-- Module: Mathlib.Topology.Separation.Hausdorff
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
x : X
⊢ lift hf (mk x) = f x

Tactic:
Quotient.lift_mk (s := t2Setoid X) f (T2Quotient.compatible hf) x

Premises used: Quotient.lift_mk, T2Quotient.lift, T2Quotient.compatible
-- Module: Mathlib.Topology.Separation.Hausdorff
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
apply : ∀ (x : X), (g ∘ mk) x = (lift hf ∘ mk) x
⊢ g = lift hf

Tactic:
apply surjective_mk X |>.right_cancellable |>.mp <| funext _

Premises used: funext, Iff.mp, Function.Surjective.right_cancellable, T2Quotient.surjective_mk
-- Module: Mathlib.Topology.Separation.Hausdorff
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
⊢ ∀ (x : X), (g ∘ mk) x = (lift hf ∘ mk) x

Tactic:
simp [← hfg]
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
f g : Y → X
hf : Continuous[inst_1, inst] f
hg : Continuous[inst_1, inst] g
⊢ IsClosed[inst_1] {y : Y | f y = g y}

Tactic:
continuous_iff_isClosed.mp (hf.prodMk hg) _ isClosed_diagonal

Premises used: Set.Mem, setOf, isClosed_diagonal, continuous_iff_isClosed, Set.diagonal, Set.preimage, Iff.mp, Continuous.prodMk
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f g : X → Y
s : Set X
hs : IsClosed[inst] s
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ IsClosed[inst] {x : X | x ∈ s ∧ f x = g x}

Tactic:
(hf.prodMk hg).preimage_isClosed_of_isClosed hs isClosed_diagonal

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, Set.Mem, setOf, Set.inter, isClosed_diagonal, Set.diagonal, Set.preimage, ContinuousOn.prodMk
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
f g : Y → X
hf : Continuous[inst_1, inst] f
hg : Continuous[inst_1, inst] g
⊢ IsOpen[inst_1] {y : Y | f y ≠ g y}

Tactic:
isOpen_compl_iff.mpr <| isClosed_eq hf hg

Premises used: Iff.mpr, Set.Mem, setOf, isClosed_eq, isOpen_compl_iff
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
s : Set Y
f g : Y → X
h : EqOn f g s
hf : Continuous[inst_1, inst] f
hg : Continuous[inst_1, inst] g
⊢ EqOn f g (closure[inst_1] s)

Tactic:
closure_minimal h (isClosed_eq hf hg)

Premises used: Set.Mem, closure_minimal, Set.EqOn, Set.Subset, isClosed_eq
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
s : Set Y
hs : Dense s
f g : Y → X
hf : Continuous[inst_1, inst] f
hg : Continuous[inst_1, inst] g
h : EqOn f g s
⊢ f = g

Tactic:
funext fun x => h.closure hf hg (hs x)

Premises used: Set.EqOn.closure, funext
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
Z : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : T2Space Z
s : Set X
t : Set Y
f g : X → Y → Z
h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y
hf₁ : ∀ (x : X), Continuous[inst_1, inst_2] (f x)
hf₂ : ∀ (y : Y), Continuous[inst, inst_2] fun (x : X) ↦ f x y
hg₁ : ∀ (x : X), Continuous[inst_1, inst_2] (g x)
hg₂ : ∀ (y : Y), Continuous[inst, inst_2] fun (x : X) ↦ g x y
this : closure[inst] s ⊆ ⋂ y ∈ closure[inst_1] t, {x : X | f x y = g x y}
⊢ ∀ x ∈ closure[inst] s, ∀ y ∈ closure[inst_1] t, f x y = g x y

Tactic:
simpa only [subset_def, mem_iInter]

Premises used: Set.subset_def, Set.mem_iInter
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
Z : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : T2Space Z
s : Set X
t : Set Y
f g : X → Y → Z
h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y
hf : Continuous[instTopologicalSpaceProd, inst_2] (uncurry f)
hg : Continuous[instTopologicalSpaceProd, inst_2] (uncurry g)
⊢ ∀ x ∈ closure[inst] s, ∀ y ∈ closure[inst_1] t, f x y = g x y

Tactic:
eqOn_closure₂' h hf.uncurry_left hf.uncurry_right hg.uncurry_left hg.uncurry_right

Premises used: eqOn_closure₂', Continuous.uncurry_right, Continuous.uncurry_left
-- Module: Mathlib.Topology.Separation.Hausdorff
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
⊢ (𝓝[s] x).NeBot

Tactic:
have : (𝓝[s] x).NeBot := mem_closure_iff_clusterPt.mp (hts hx)
-- Module: Mathlib.Topology.Separation.Hausdorff
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
this : (𝓝[s] x).NeBot
⊢ f x = g x

Tactic:
tendsto_nhds_unique_of_eventuallyEq ((hf x hx).mono_left <| nhdsWithin_mono _ hst)
      ((hg x hx).mono_left <| nhdsWithin_mono _ hst) (h.eventuallyEq_of_mem self_mem_nhdsWithin)

Premises used: Set.EqOn.eventuallyEq_of_mem, tendsto_nhds_unique_of_eventuallyEq, self_mem_nhdsWithin, Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.Topology.Separation.Hausdorff
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
this : (𝓝[s] x).NeBot
⊢ f x = g x

Tactic:
exact
    tendsto_nhds_unique_of_eventuallyEq ((hf x hx).mono_left <| nhdsWithin_mono _ hst)
      ((hg x hx).mono_left <| nhdsWithin_mono _ hst) (h.eventuallyEq_of_mem self_mem_nhdsWithin)

Premises used: Set.EqOn.eventuallyEq_of_mem, tendsto_nhds_unique_of_eventuallyEq, self_mem_nhdsWithin, Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
f : X → Y
g : Y → X
h : LeftInverse f g
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst] g
⊢ IsClosed[inst] (range g)

Tactic:
have : EqOn (g ∘ f) id (closure <| range g) :=
    h.rightInvOn_range.eqOn.closure (hg.comp hf) continuous_id
  isClosed_of_closure_subset fun x hx => ⟨f x, this hx⟩

Premises used: Set.RightInvOn.eqOn, Continuous.comp, Set.EqOn.closure, continuous_id, Exists.intro, Function.LeftInverse.rightInvOn_range, isClosed_of_closure_subset
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
f : X → Y
g : Y → X
h : LeftInverse f g
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst] g
⊢ IsClosedEmbedding g

Tactic:
⟨.of_leftInverse h hf hg, h.isClosed_range hf hg⟩

Premises used: Function.LeftInverse.isClosed_range, Topology.IsEmbedding.of_leftInverse, Topology.IsClosedEmbedding.mk
-- Module: Mathlib.Topology.Separation.Hausdorff
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
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)ᶜ
⊢ SeparatedNhds s t

Tactic:
simp only [SeparatedNhds, prod_subset_compl_diagonal_iff_disjoint.symm] at hst ⊢

Premises used: SeparatedNhds, Set.prod_subset_compl_diagonal_iff_disjoint, Iff.symm
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
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:
generalized_tube_lemma hs ht isClosed_diagonal.isOpen_compl hst

Premises used: IsClosed.isOpen_compl, generalized_tube_lemma
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
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:
exact generalized_tube_lemma hs ht isClosed_diagonal.isOpen_compl hst

Premises used: IsClosed.isOpen_compl, generalized_tube_lemma
-- Module: Mathlib.Topology.Separation.Hausdorff
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
⊢ IsCompact t

Tactic:
have ht : IsCompact t := .of_isClosed_subset H2 H3 <| H4.subset_compl_left.trans subset_closure
-- Module: Mathlib.Topology.Separation.Hausdorff
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
rw : SeparatedNhds (s \ interior s ∪ interior s) t
⊢ SeparatedNhds s t

Tactic:
rw [← diff_union_of_subset (interior_subset (s := s))]

Premises used: interior_subset, Set.diff_union_of_subset
-- Module: Mathlib.Topology.Separation.Hausdorff
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

Tactic:
.union_left ?_ ⟨interior s, sᶜ, isOpen_interior, H1.isOpen_compl, le_rfl,
    H4.subset_compl_left, disjoint_compl_right.mono_left interior_subset⟩

Premises used: le_rfl, interior_subset, IsClosed.isOpen_compl, Compl.compl, isOpen_interior, Disjoint.mono_left, Disjoint.subset_compl_left, And.intro, interior, SeparatedNhds.union_left, Exists.intro, disjoint_compl_right
-- Module: Mathlib.Topology.Separation.Hausdorff
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
refine : SeparatedNhds (s \ interior s) t
⊢ SeparatedNhds (s \ interior 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⟩
-- Module: Mathlib.Topology.Separation.Hausdorff
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
rw : SeparatedNhds (s ∩ closure[inst] sᶜ) t
⊢ SeparatedNhds (s \ interior s) t

Tactic:
rw [← H1.frontier_eq, frontier_eq_closure_inter_closure, H1.closure_eq]

Premises used: IsClosed.closure_eq, IsClosed.frontier_eq, frontier_eq_closure_inter_closure
-- Module: Mathlib.Topology.Separation.Hausdorff
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

Tactic:
.of_isCompact_isCompact_isClosed ?_ ht H3 (disjoint_of_subset_left inter_subset_left H4)

Premises used: Set.disjoint_of_subset_left, Set.inter_subset_left, SeparatedNhds.of_isCompact_isCompact_isClosed
-- Module: Mathlib.Topology.Separation.Hausdorff
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
refine : IsCompact (s ∩ closure[inst] sᶜ)
⊢ SeparatedNhds (s ∩ closure[inst] sᶜ) t

Tactic:
refine .of_isCompact_isCompact_isClosed ?_ ht H3 (disjoint_of_subset_left inter_subset_left H4)
-- Module: Mathlib.Topology.Separation.Hausdorff
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
⊢ IsCompact (s ∩ closure[inst] sᶜ)

Tactic:
H2.of_isClosed_subset (H1.inter isClosed_closure) inter_subset_right

Premises used: IsCompact.of_isClosed_subset, IsClosed.inter, isClosed_closure, Set.inter_subset_right
-- Module: Mathlib.Topology.Separation.Hausdorff
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
⊢ IsCompact (s ∩ closure[inst] sᶜ)

Tactic:
exact H2.of_isClosed_subset (H1.inter isClosed_closure) inter_subset_right

Premises used: IsCompact.of_isClosed_subset, IsClosed.inter, isClosed_closure, Set.inter_subset_right
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Finset X
h : Disjoint s t
⊢ SeparatedNhds (↑s : Set X) (↑t : Set X)

Tactic:
.of_isCompact_isCompact s.finite_toSet.isCompact t.finite_toSet.isCompact <| mod_cast h

Premises used: cast, Set.Finite.isCompact, Finset.disjoint_coe._simp_1, Finset.finite_toSet, SeparatedNhds.of_isCompact_isCompact, Eq.symm
-- Module: Mathlib.Topology.Separation.Hausdorff
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
rw : SeparatedNhds (↑(hs.toFinset (s := s)) : Set X) (↑(ht.toFinset (s := t)) : Set X)
⊢ SeparatedNhds s t

Tactic:
rw [← hs.coe_toFinset, ← ht.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.Topology.Separation.Hausdorff
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 (↑(hs.toFinset (s := s)) : Set X) (↑(ht.toFinset (s := t)) : Set X)

Tactic:
SeparatedNhds.of_finset_finset _ _ (Finite.disjoint_toFinset.2 h)

Premises used: Iff.mpr, SeparatedNhds.of_finset_finset, Set.Finite.disjoint_toFinset
-- Module: Mathlib.Topology.Separation.Hausdorff
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 (↑(hs.toFinset (s := s)) : Set X) (↑(ht.toFinset (s := t)) : Set X)

Tactic:
exact SeparatedNhds.of_finset_finset _ _ (Finite.disjoint_toFinset.2 h)

Premises used: Iff.mpr, SeparatedNhds.of_finset_finset, Set.Finite.disjoint_toFinset
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x : X
s : Finset X
h : x ∉ s
⊢ SeparatedNhds {x} (↑s : Set X)

Tactic:
mod_cast .of_finset_finset {x} s (Finset.disjoint_singleton_left.mpr h)

Premises used: Iff.mpr, Finset.coe_singleton, congrArg, cast, SeparatedNhds.of_finset_finset, SetLike.coe, SeparatedNhds, congrFun', Finset.disjoint_singleton_left, Singleton.singleton
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s : Set X
hs : IsCompact s
⊢ IsClosed[inst] s

Tactic:
isClosed_iff_forall_filter.2 fun _x _f _ hfs hfx =>
    let ⟨_y, hy, hfy⟩ := hs.exists_clusterPt hfs
    mem_of_eq_of_mem (eq_of_nhds_neBot (hfy.mono hfx).neBot).symm hy

Premises used: Iff.mpr, ClusterPt.mono, eq_of_nhds_neBot, ClusterPt.neBot, Membership.mem, IsCompact.exists_clusterPt, Set.mem_of_eq_of_mem, _private.0.IsCompact.isClosed.match_1, isClosed_iff_forall_filter, Eq.symm
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X → Y
s : Set Y
hs : IsCompact s
hf : Continuous[inst, inst_1] f
⊢ IsCompact (f ⁻¹' s)

Tactic:
(hs.isClosed.preimage hf).isCompact

Premises used: IsClosed.isCompact, IsClosed.preimage, IsCompact.isClosed
-- Module: Mathlib.Topology.Separation.Hausdorff
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)
mpr : (IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)) → IsCompact s
⊢ IsCompact s ↔ IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Hausdorff
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)
H : IsCompact s
⊢ IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)

Tactic:
⟨H.isClosed, fun i ↦ H.image <| continuous_apply i⟩

Premises used: And.intro, continuous_apply, IsCompact.image, IsCompact.isClosed
-- Module: Mathlib.Topology.Separation.Hausdorff
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)
H : IsCompact s
⊢ IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)

Tactic:
exact ⟨H.isClosed, fun i ↦ H.image <| continuous_apply i⟩
-- Module: Mathlib.Topology.Separation.Hausdorff
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)
H : IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)
⊢ IsCompact s

Tactic:
IsCompact.of_isClosed_subset (isCompact_univ_pi H.2) H.1 (subset_pi_eval_image univ s)

Premises used: Set.univ, isCompact_univ_pi, IsCompact.of_isClosed_subset, And.right, And.left, Set.subset_pi_eval_image
-- Module: Mathlib.Topology.Separation.Hausdorff
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)
H : IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval (β := X) i '' s)
⊢ IsCompact s

Tactic:
exact IsCompact.of_isClosed_subset (isCompact_univ_pi H.2) H.1 (subset_pi_eval_image univ s)

Premises used: Set.univ, isCompact_univ_pi, IsCompact.of_isClosed_subset, And.right, And.left, Set.subset_pi_eval_image
-- Module: Mathlib.Topology.Separation.Hausdorff
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
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
⊢ IsCompact (closure[topologicalSpace] s) ↔ ∀ (i : ι), IsCompact (closure[inst i] (eval (β := X) i '' s))

Tactic:
simp_rw [← exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, image_subset_iff]

Premises used: exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, Set.image_subset_iff
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
inst_2 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
⊢ ∃ (i : ι), V i ⊆ U

Tactic:
exists_subset_nhds_of_isCompact' hV hV_cpct (fun i => (hV_cpct i).isClosed) hU

Premises used: exists_subset_nhds_of_isCompact', IsCompact.isClosed
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
K : CompactExhaustion X
n : ℕ
⊢ IsClosed[inst] ((K : (a : ℕ) → Set X) n)

Tactic:
(K.isCompact n).isClosed

Premises used: CompactExhaustion.isCompact, IsCompact.isClosed