-- 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 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))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ n, u₀ n
dis : ∀ (n : ℕ), Disjoint (closure (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : x ∈ (fun n => u₀ n) n
⊢ ∃ i, x ∈ u₀ i \ closure (⋃ m, ⋃ (_ : m ≤ i), v₀ m)

Tactic:
refine ⟨n, xinun, ?_⟩

Result:
case 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))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ n, u₀ n
dis : ∀ (n : ℕ), Disjoint (closure (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : x ∈ (fun n => u₀ n) n
⊢ x ∉ closure (⋃ m, ⋃ (_ : m ≤ n), v₀ 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))
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))

Tactic:
rw [Set.disjoint_left]

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)
⊢ ∀ ⦃a : X⦄, a ∈ ⋃ n, u n \ closure (⋃ m, ⋃ (_ : m ≤ n), v m) → a ∉ ⋃ n, v n \ closure (⋃ m, ⋃ (_ : m ≤ n), u m)

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

Tactic:
rintro ⟨⟨u, u_cov, u_props⟩, ⟨v, v_cov, v_props⟩⟩

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
⊢ 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
m_gt_n : ¬n ≤ m
⊢ False

Tactic:
exact xinun.2 (subset_closure (mem_biUnion (le_of_lt (not_le.mp m_gt_n)) xinvm))

Result:
no goals

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 : ℕ
xinvm : x ∈ v m
⊢ x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m')

Tactic:
have n_le_m : n ≤ m := by
  by_contra m_gt_n
  exact xinun.2 (subset_closure (mem_biUnion (le_of_lt (not_le.mp m_gt_n)) 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
n_le_m : n ≤ m
⊢ x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m')

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 : ℕ
xinvm : x ∈ v m
n_le_m : n ≤ m
⊢ x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m')

Tactic:
exact subset_closure (mem_biUnion n_le_m xinun.1)

Result:
no goals

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)
⊢ ∀ ⦃a : X⦄, a ∈ ⋃ n, u n \ closure (⋃ m, ⋃ (_ : m ≤ n), v m) → a ∉ ⋃ n, v n \ closure (⋃ m, ⋃ (_ : m ≤ n), u m)

Tactic:
rintro x ⟨un, ⟨n, rfl⟩, xinun⟩

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
⊢ x ∉ ⋃ n, v n \ closure (⋃ m, ⋃ (_ : m ≤ n), u m)