-- Mathlib/Topology/Separation/SeparatedNhds.lean
theorem hasSeparatingCovers_iff_separatedNhds {s t : Set X} :
    HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n → (∀ (n : ℕ), Disjoint (closure (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n => u n \ closure (⋃ m, ⋃ (_ : m ≤ n), v m)) n
⊢ ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m')

Tactic:
intro m xinvm

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n → (∀ (n : ℕ), Disjoint (closure (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n => u n \ closure (⋃ m, ⋃ (_ : m ≤ n), v m)) n
m : ℕ
xinvm : x ∈ v m
⊢ x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m')

Proof state:
case mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
⊢ SeparatedNhds s t

Tactic:
have open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ n, IsOpen (u₀ n)) →
  IsOpen (⋃ n, u₀ n \ closure (a n)) := fun _ _ u₀i_open ↦
    isOpen_iUnion fun i ↦ (u₀i_open i).sdiff isClosed_closure

Result:
case mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n))
⊢ SeparatedNhds s t

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t → HasSeparatingCover s t ∧ HasSeparatingCover t s

Tactic:
rintro ⟨U, V, U_open, V_open, h_sub_U, k_sub_V, UV_dis⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t U V : Set X
U_open : IsOpen U
V_open : IsOpen V
h_sub_U : s ⊆ U
k_sub_V : t ⊆ V
UV_dis : Disjoint U V
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s

Proof state:
case mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n → (∀ (n : ℕ), Disjoint (closure (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
⊢ SeparatedNhds s t

Tactic:
refine
  ⟨⋃ n : ℕ, u n \ (closure (⋃ m ≤ n, v m)),
   ⋃ n : ℕ, v n \ (closure (⋃ m ≤ n, u m)),
   open_lemma u (fun n ↦ ⋃ m ≤ n, v m) (fun n ↦ (u_props n).1),
   open_lemma v (fun n ↦ ⋃ m ≤ n, u m) (fun n ↦ (v_props n).1),
   cover_lemma s u v u_cov (fun n ↦ (v_props n).2),
   cover_lemma t v u v_cov (fun n ↦ (u_props n).2),
   ?_⟩

Result:
case mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n → (∀ (n : ℕ), Disjoint (closure (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
⊢ Disjoint (⋃ n, u n \ closure (⋃ m, ⋃ (_ : m ≤ n), v m)) (⋃ n, v n \ closure (⋃ m, ⋃ (_ : m ≤ n), u m))

Proof state:
case mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n))
⊢ SeparatedNhds s t

Tactic:
have cover_lemma : ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    (h₀ ⊆ ⋃ n, u₀ n) → (∀ n, Disjoint (closure (v₀ n)) h₀) →
    (h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m ≤ n, v₀ m)) :=
    fun h₀ u₀ v₀ h₀_cov dis x xinh ↦ by
  rcases h₀_cov xinh with ⟨un , ⟨n, rfl⟩ , xinun⟩
  simp only [mem_iUnion]
  refine ⟨n, xinun, ?_⟩
  simp_all only [closure_iUnion₂_le_nat, disjoint_right, mem_setOf_eq, mem_iUnion,
    exists_false, exists_const, not_false_eq_true]

Result:
case mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n → (∀ (n : ℕ), Disjoint (closure (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
⊢ SeparatedNhds s t

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n → (∀ (n : ℕ), Disjoint (closure (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n => u n \ closure (⋃ m, ⋃ (_ : m ≤ n), v m)) n
m : ℕ
xinvm : x ∈ v m
⊢ n ≤ m

Tactic:
by_contra m_gt_n

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen (v n) ∧ Disjoint (closure (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n → (∀ (n : ℕ), Disjoint (closure (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n => u n \ closure (⋃ m, ⋃ (_ : m ≤ n), v m)) n
m : ℕ
xinvm : x ∈ v m
m_gt_n : ¬n ≤ m
⊢ False

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t

Tactic:
constructor

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s → SeparatedNhds s t

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t → HasSeparatingCover s t ∧ HasSeparatingCover t s