awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Basic
Goal:
ι : Type u_3
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst_2 : ∀ (i : ι), T1Space.{u_4} (β i)
refine : ∀ (s : Set (β i)) (hs : IsClosed[inst_1 i] s), IsClosed[Pi.topologicalSpace] (update (β := β) x i '' s)
⊢ IsClosedEmbedding (update (β := β) x i)

Tactic:
refine .of_continuous_injective_isClosedMap (continuous_const.update i continuous_id)
    (update_injective x i) fun s hs ↦ ?_
-- Module: Mathlib.Topology.Separation.Basic
Goal:
ι : Type u_3
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst_2 : ∀ (i : ι), T1Space.{u_4} (β i)
s : Set (β i)
hs : IsClosed[inst_1 i] s
rw :
  IsClosed[Pi.topologicalSpace] (Set.pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s))
⊢ IsClosed[Pi.topologicalSpace] (update (β := β) x i '' s)

Tactic:
rw [update_image]

Premises used: Set.update_image
-- Module: Mathlib.Topology.Separation.Basic
Goal:
ι : Type u_3
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst_2 : ∀ (i : ι), T1Space.{u_4} (β i)
s : Set (β i)
hs : IsClosed[inst_1 i] s
hs₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι) univ a →
      IsClosed[inst_1 a] (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s a)
⊢ IsClosed[Pi.topologicalSpace] (Set.pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s))

Tactic:
apply isClosed_set_pi

Premises used: isClosed_set_pi
-- Module: Mathlib.Topology.Separation.Basic
Goal:
ι : Type u_3
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst_2 : ∀ (i : ι), T1Space.{u_4} (β i)
s : Set (β i)
hs : IsClosed[inst_1 i] s
⊢ ∀ (a : ι),
    Membership.mem (γ := Set ι) univ a →
      IsClosed[inst_1 a] (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s a)

Tactic:
simp [forall_update_iff, hs]

Premises used: Function.forall_update_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : T1Space α
a : α
⊢ 𝓝[≠] a ≤ cofinite

Tactic:
le_cofinite_iff_compl_singleton_mem.mpr fun x ↦ ?_

Premises used: Iff.mpr, Filter.le_cofinite_iff_compl_singleton_mem
-- Module: Mathlib.Topology.Separation.Basic
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : T1Space α
a : α
refine : ∀ (x : α), {x}ᶜ ∈ 𝓝[≠] a
⊢ 𝓝[≠] a ≤ cofinite

Tactic:
refine le_cofinite_iff_compl_singleton_mem.mpr fun x ↦ ?_

Premises used: Iff.mpr, Filter.le_cofinite_iff_compl_singleton_mem
-- Module: Mathlib.Topology.Separation.Basic
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : T1Space α
a x : α
inl : {a}ᶜ ∈ 𝓝[≠] a
inr : ∀ (hx : a ≠ x), {x}ᶜ ∈ 𝓝[≠] a
⊢ {x}ᶜ ∈ 𝓝[≠] a

Tactic:
rcases eq_or_ne a x with rfl | hx

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : T1Space α
a : α
⊢ {a}ᶜ ∈ 𝓝[≠] a

Tactic:
self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Topology.Separation.Basic
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : T1Space α
a x : α
hx : a ≠ x
⊢ {x}ᶜ ∈ 𝓝[≠] a

Tactic:
eventually_ne_nhdsWithin hx

Premises used: Set.Mem, Filter.Eventually, setOf, eventually_ne_nhdsWithin, Set.singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : T1Space α
a : α
⊢ {a}ᶜ ∈ 𝓝[≠] a

Tactic:
exacts [self_mem_nhdsWithin, eventually_ne_nhdsWithin hx]

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Topology.Separation.Basic
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : T1Space α
inst_2 : DecidableEq α
f : α → β
a a' : α
b : β
⊢ update (β := fun (a : α) ↦ β) f a b =ᶠ[𝓝[≠] a'] f

Tactic:
(Function.update_eventuallyEq_cofinite f a b).filter_mono (nhdsNE_le_cofinite a')

Premises used: Filter.EventuallyEq.filter_mono, nhdsNE_le_cofinite, Function.update_eventuallyEq_cofinite
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
⊢ Disjoint (𝓝 x) (𝓝 y) ↔ ¬x ⤳ y

Tactic:
⟨fun hd hspec ↦ hspec.not_disjoint hd, (specializes_or_disjoint_nhds _ _).resolve_left⟩

Premises used: Or.resolve_left, R1Space.specializes_or_disjoint_nhds, Iff.intro, Specializes.not_disjoint
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
⊢ x ⤳ y ↔ ¬Disjoint (𝓝 x) (𝓝 y)

Tactic:
disjoint_nhds_nhds_iff_not_specializes.not_left.symm

Premises used: disjoint_nhds_nhds_iff_not_specializes, Iff.not_left, Iff.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
rw : ¬x ⤳ y ↔ ¬Inseparable x y
rw₁ rw₂ : ¬Inseparable x y ↔ ¬Inseparable x y
⊢ Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y

Tactic:
rw [disjoint_nhds_nhds_iff_not_specializes, specializes_iff_inseparable]

Premises used: disjoint_nhds_nhds_iff_not_specializes, specializes_iff_inseparable
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
inst : TopologicalSpace X
⊢ R1Space X ↔ ∀ (x y : X), Inseparable x y ∨ Disjoint (𝓝 x) (𝓝 y)

Tactic:
⟨fun _h x y ↦ (specializes_or_disjoint_nhds x y).imp_left Specializes.inseparable, fun h ↦
    ⟨fun x y ↦ (h x y).imp_left Inseparable.specializes⟩⟩

Premises used: Or.imp_left, R1Space.mk, Specializes.inseparable, R1Space.specializes_or_disjoint_nhds, Inseparable.specializes, Iff.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
h : (𝓝 x ⊓ 𝓝 y).NeBot
⊢ Inseparable x y

Tactic:
(r1Space_iff_inseparable_or_disjoint_nhds.mp ‹_› _ _).resolve_right fun h' => h.ne h'.eq_bot

Premises used: Filter.NeBot.ne, r1Space_iff_inseparable_or_disjoint_nhds, Iff.mp, Or.resolve_right, Disjoint.eq_bot
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
h : ¬Inseparable x y
⊢ ∃ (i : Set X), (x ∈ i ∧ IsOpen[inst] i) ∧ ∃ (i' : Set X), (y ∈ i' ∧ IsOpen[inst] i') ∧ Disjoint i i'

Tactic:
rw [← disjoint_nhds_nhds_iff_not_inseparable,
    (nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)] at h

Premises used: Filter.HasBasis.disjoint_iff, disjoint_nhds_nhds_iff_not_inseparable, nhds_basis_opens
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
h : ∃ (i : Set X), (x ∈ i ∧ IsOpen[inst] i) ∧ ∃ (i' : Set X), (y ∈ i' ∧ IsOpen[inst] i') ∧ Disjoint i i'
obtain :
  ∀ (u : Set X) (hxu : x ∈ u) (hu : IsOpen[inst] u) (v : Set X) (huv : Disjoint u v) (hyv : y ∈ v)
    (hv : IsOpen[inst] v), ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
obtain ⟨u, ⟨hxu, hu⟩, v, ⟨hyv, hv⟩, huv⟩ := h
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
u : Set X
hxu : x ∈ u
hu : IsOpen[inst] u
v : Set X
huv : Disjoint u v
hyv : y ∈ v
hv : IsOpen[inst] v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
⟨u, v, hu, hv, hxu, hyv, huv⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
u : Set X
hxu : x ∈ u
hu : IsOpen[inst] u
v : Set X
huv : Disjoint u v
hyv : y ∈ v
hv : IsOpen[inst] v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
exact ⟨u, v, hu, hv, hxu, hyv, huv⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
f : Y → X
l : Filter Y
a b : X
inst_2 : l.NeBot
ha : Tendsto f l (𝓝 a)
hb : Tendsto f l (𝓝 b)
⊢ Inseparable a b

Tactic:
.of_nhds_neBot <| neBot_of_le <| le_inf ha hb

Premises used: Inseparable.of_nhds_neBot, le_inf, Filter.neBot_of_le
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ IsClosed[instTopologicalSpaceProd] {p : X × X | p.1 ⤳ p.2}

Tactic:
simp only [← isOpen_compl_iff, compl_setOf, ← disjoint_nhds_nhds_iff_not_specializes,
    isOpen_setOf_disjoint_nhds_nhds]

Premises used: isOpen_setOf_disjoint_nhds_nhds, disjoint_nhds_nhds_iff_not_specializes, isOpen_compl_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ IsClosed[instTopologicalSpaceProd] {p : X × X | Inseparable p.1 p.2}

Tactic:
simp only [← specializes_iff_inseparable, isClosed_setOf_specializes]

Premises used: isClosed_setOf_specializes, specializes_iff_inseparable
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
y : X
K : Set X
hK : IsCompact K
⊢ y ∈ closure[inst] K ↔ ∃ x ∈ K, Inseparable x y

Tactic:
⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦
    (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩

Premises used: subset_closure, Membership.mem, Inseparable.mem_closed_iff, _private.0.IsCompact.mem_closure_iff_exists_inseparable.match_1, closure, Iff.intro, Iff.mp, isClosed_closure
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
y : X
K : Set X
hK : IsCompact K
refine : ∀ (hy : y ∈ closure[inst] K), ∃ x ∈ K, Inseparable x y
⊢ y ∈ closure[inst] K ↔ ∃ x ∈ K, Inseparable x y

Tactic:
refine ⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦
    (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : y ∈ closure[inst] K
contrapose! : ∀ (hy : ∀ (x : X) (_ : x ∈ K), ¬Inseparable x y), y ∉ closure[inst] K
⊢ ∃ x ∈ K, Inseparable x y

Tactic:
contrapose! hy
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ (x : X) (_ : x ∈ K), ¬Inseparable x y
⊢ Disjoint (𝓝 y) (𝓝ˢ K)

Tactic:
have : Disjoint (𝓝 y) (𝓝ˢ K) := hK.disjoint_nhdsSet_right.2 fun x hx ↦
    (disjoint_nhds_nhds_iff_not_inseparable.2 (hy x hx)).symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ (x : X) (_ : x ∈ K), ¬Inseparable x y
this : Disjoint (𝓝 y) (𝓝ˢ K)
⊢ y ∉ closure[inst] K

Tactic:
simpa only [disjoint_iff, notMem_closure_iff_nhdsWithin_eq_bot]
    using this.mono_right principal_le_nhdsSet

Premises used: disjoint_iff, notMem_closure_iff_nhdsWithin_eq_bot, Disjoint.mono_right, principal_le_nhdsSet
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
h : ∀ (x : X), x ∈ closure[inst] K ↔ Membership.mem (γ := Set X) (⋃ x ∈ K, {y : X | Inseparable x y}) x
⊢ closure[inst] K = ⋃ x ∈ K, {y : X | Inseparable x y}

Tactic:
ext
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
x : X
⊢ x ∈ closure[inst] K ↔ Membership.mem (γ := Set X) (⋃ x ∈ K, {y : X | Inseparable x y}) x

Tactic:
simp [hK.mem_closure_iff_exists_inseparable]

Premises used: IsCompact.mem_closure_iff_exists_inseparable
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
⊢ closure[inst] K = ⋃ x ∈ K, closure[inst] {x}

Tactic:
simp only [hK.closure_eq_biUnion_inseparable, ← specializes_iff_inseparable,
    specializes_iff_mem_closure, setOf_mem_eq]

Premises used: specializes_iff_mem_closure, IsCompact.closure_eq_biUnion_inseparable, Set.setOf_mem_eq, specializes_iff_inseparable
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
hKU : K ⊆ U
rw : ∀ (i : X) (j : i ∈ K), {y : X | Inseparable i y} ⊆ U
⊢ closure[inst] K ⊆ U

Tactic:
rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]

Premises used: IsCompact.closure_eq_biUnion_inseparable, Set.iUnion₂_subset_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
hKU : K ⊆ U
⊢ ∀ (i : X) (j : i ∈ K), {y : X | Inseparable i y} ⊆ U

Tactic:
fun x hx y hxy ↦ (hxy.mem_open_iff hU).1 (hKU hx)

Premises used: Set.Subset, Iff.mp, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
hKU : K ⊆ U
⊢ ∀ (i : X) (j : i ∈ K), {y : X | Inseparable i y} ⊆ U

Tactic:
exact fun x hx y hxy ↦ (hxy.mem_open_iff hU).1 (hKU hx)
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
⊢ IsCompact (closure[inst] K)

Tactic:
isCompact_of_finite_subcover fun U hUo hKU ↦ ?_

Premises used: isCompact_of_finite_subcover
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
refine :
  ∀ {ι : Type u_1} (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen[inst] (U i)) (hKU : closure[inst] K ⊆ ⋃ (i : ι), U i),
    ∃ (t : Finset ι), closure[inst] K ⊆ ⋃ i ∈ t, U i
⊢ IsCompact (closure[inst] K)

Tactic:
refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_

Premises used: isCompact_of_finite_subcover
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hKU : closure[inst] K ⊆ ⋃ (i : ι), U i
rcases : ∀ (t : Finset ι) (ht : K ⊆ ⋃ i ∈ t, U i), ∃ (t : Finset ι), closure[inst] K ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), closure[inst] K ⊆ ⋃ i ∈ t, U i

Tactic:
rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩

Premises used: subset_closure, HasSubset.Subset.trans, IsCompact.elim_finite_subcover
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hKU : closure[inst] K ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : K ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), closure[inst] K ⊆ ⋃ i ∈ t, U i

Tactic:
⟨t, hK.closure_subset_of_isOpen (isOpen_biUnion fun _ _ ↦ hUo _) ht⟩

Premises used: IsCompact.closure_subset_of_isOpen, Exists.intro, isOpen_biUnion
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hKU : closure[inst] K ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : K ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), closure[inst] K ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨t, hK.closure_subset_of_isOpen (isOpen_biUnion fun _ _ ↦ hUo _) ht⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s K : Set X
hK : IsCompact K
h : s ⊆ K
⊢ IsCompact (closure[inst] s)

Tactic:
hK.closure.of_isClosed_subset isClosed_closure (closure_mono h)

Premises used: IsCompact.closure, closure_mono, IsCompact.of_isClosed_subset, isClosed_closure
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s : Set X
⊢ (∃ (K : Set X), IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure[inst] s)

Tactic:
⟨fun ⟨_K, hK, hsK⟩ => hK.closure_of_subset hsK, fun h => ⟨closure s, h, subset_closure⟩⟩

Premises used: subset_closure, _private.0.exists_isCompact_superset_iff.match_1, closure, And.intro, Iff.intro, Exists.intro, IsCompact.closure_of_subset, IsCompact
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst] L
hd : Disjoint K L
simp_rw : ∀ x ∈ K, ∀ x_1 ∈ L, ¬Inseparable x x_1
⊢ SeparatedNhds K L

Tactic:
simp_rw [separatedNhds_iff_disjoint, hK.disjoint_nhdsSet_left, hL.disjoint_nhdsSet_right,
    disjoint_nhds_nhds_iff_not_inseparable]

Premises used: IsCompact.disjoint_nhdsSet_left, separatedNhds_iff_disjoint, disjoint_nhds_nhds_iff_not_inseparable, IsCompact.disjoint_nhdsSet_right
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst] L
hd : Disjoint K L
x : X
hx : x ∈ K
y : X
hy : y ∈ L
h : Inseparable x y
⊢ False

Tactic:
absurd ((h.mem_closed_iff h'L).2 hy) <| disjoint_left.1 hd hx

Premises used: Iff.mpr, Set.disjoint_left, Inseparable.mem_closed_iff, absurd, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst] L
hd : Disjoint K L
x : X
hx : x ∈ K
y : X
hy : y ∈ L
h : Inseparable x y
⊢ False

Tactic:
exact absurd ((h.mem_closed_iff h'L).2 hy) <| disjoint_left.1 hd hx

Premises used: Iff.mpr, Set.disjoint_left, Inseparable.mem_closed_iff, absurd, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
⊢ IsCompact (closure[inst] K)

Tactic:
have hK' : IsCompact (closure K) := hK.closure
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
apply : Disjoint (closure[inst] K \ U) (closure[inst] K \ V)
⊢ SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)

Tactic:
apply SeparatedNhds.of_isCompact_isCompact_isClosed (hK'.diff hU) (hK'.diff hV)
      (isClosed_closure.sdiff hV)

Premises used: IsClosed.sdiff, SeparatedNhds.of_isCompact_isCompact_isClosed, IsCompact.diff, isClosed_closure
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
rw : closure[inst] K ⊆ U ∪ V
⊢ Disjoint (closure[inst] K \ U) (closure[inst] K \ V)

Tactic:
rw [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty]

Premises used: Set.disjoint_iff_inter_eq_empty, Set.diff_inter_diff, Set.diff_eq_empty
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
⊢ closure[inst] K ⊆ U ∪ V

Tactic:
hK.closure_subset_of_isOpen (hU.union hV) h2K

Premises used: IsOpen.union, IsCompact.closure_subset_of_isOpen
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
⊢ closure[inst] K ⊆ U ∪ V

Tactic:
exact hK.closure_subset_of_isOpen (hU.union hV) h2K

Premises used: IsOpen.union, IsCompact.closure_subset_of_isOpen
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
⊢ SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)

Tactic:
have : SeparatedNhds (closure K \ U) (closure K \ V) := by
    apply SeparatedNhds.of_isCompact_isCompact_isClosed (hK'.diff hU) (hK'.diff hV)
      (isClosed_closure.sdiff hV)
    rw [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty]
    exact hK.closure_subset_of_isOpen (hU.union hV) h2K
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
this : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
⊢ SeparatedNhds (K \ U) (K \ V)

Tactic:
have : SeparatedNhds (K \ U) (K \ V) :=
    this.mono (diff_subset_diff_left (subset_closure)) (diff_subset_diff_left (subset_closure))
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
this_1 : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
this : SeparatedNhds (K \ U) (K \ V)
rcases :
  ∀ (O₁ O₂ : Set X) (h1O₁ : IsOpen[inst] O₁) (h1O₂ : IsOpen[inst] O₂) (h2O₁ : K \ U ⊆ O₁) (h2O₂ : K \ V ⊆ O₂)
    (hO : Disjoint O₁ O₂), ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
⊢ ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
rcases this with ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
this : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst] O₁
h1O₂ : IsOpen[inst] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
rw : K = K \ (O₁ ∩ O₂)
rw₁ : K = K \ ∅
rw₂ rw₃ : K = K
⊢ K = K \ O₁ ∪ K \ O₂

Tactic:
rw [← diff_inter, hO.inter_eq, diff_empty]

Premises used: Set.diff_empty, Disjoint.inter_eq, Set.diff_inter
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
this : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst] O₁
h1O₂ : IsOpen[inst] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
exact ⟨K \ O₁, K \ O₂, hK.diff h1O₁, hK.diff h1O₂, diff_subset_comm.mp h2O₁,
    diff_subset_comm.mp h2O₂, by rw [← diff_inter, hO.inter_eq, diff_empty]⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i)
hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i
⊢ ∃ (K : ι → Set X),
    (∀ (i : ι), IsCompact (K i)) ∧
      (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), K i

Tactic:
⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩

Premises used: And.intro, Set.empty_subset, Exists.intro, EmptyCollection.emptyCollection, isCompact_empty
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i)
hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i
empty : s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (fun (x : ι) ↦ (∅ : Set X)) i
⊢ ∃ (K : ι → Set X),
    (∀ (i : ι), IsCompact (K i)) ∧
      (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), K i

Tactic:
refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i)
hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i
⊢ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (fun (x : ι) ↦ (∅ : Set X)) i

Tactic:
simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC

Premises used: Finset.notMem_empty, Set.iUnion_false, Set.subset_empty_iff, Set.iUnion_empty