-- Mathlib/Topology/Separation/Basic.lean
theorem IsCompact.binary_compact_cover {K U V : Set X}
    (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) :
    ∃ K₁ K₂ : Set X, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
⊢ Disjoint (closure K \ U) (closure K \ V)

Tactic:
rw [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
⊢ closure K ⊆ U ∪ V

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
⊢ closure K ⊆ U ∪ V

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

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
this : SeparatedNhds (closure K \ U) (closure K \ V)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
have : SeparatedNhds (K \ U) (K \ V) :=
  this.mono (diff_subset_diff_left (subset_closure)) (diff_subset_diff_left (subset_closure))

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
this✝ : SeparatedNhds (closure K \ U) (closure K \ V)
this : SeparatedNhds (K \ U) (K \ V)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
⊢ SeparatedNhds (closure K \ U) (closure K \ V)

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

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
⊢ Disjoint (closure K \ U) (closure K \ V)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
this✝ : SeparatedNhds (closure K \ U) (closure K \ V)
this : SeparatedNhds (K \ U) (K \ V)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
rcases this with ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
this : SeparatedNhds (closure K \ U) (closure K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen O₁
h1O₂ : IsOpen O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
this : SeparatedNhds (closure K \ U) (closure K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen O₁
h1O₂ : IsOpen O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ K = K \ O₁ ∪ K \ O₂

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

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

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

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
this : SeparatedNhds (closure K \ U) (closure K \ V)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
this : SeparatedNhds (closure K \ U) (closure K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen O₁
h1O₂ : IsOpen O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ ∃ K₁ K₂, 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]⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
have hK' : IsCompact (closure K) := hK.closure

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure K)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂