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

Tactic:
simp_all only [closure_iUnion₂_le_nat, disjoint_right, mem_setOf_eq, mem_iUnion,
  exists_false, exists_const, not_false_eq_true]

Result:
no goals

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

Tactic:
simp only [mem_iUnion]

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

Tactic:
suffices ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m') by simpa

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

Proof state:
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

Tactic:
exact
  ⟨⟨fun _ ↦ U,
    h_sub_U.trans (iUnion_const U).symm.subset,
    fun _ ↦
      ⟨U_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) k_sub_V (UV_dis.closure_left V_open)⟩⟩,
   ⟨fun _ ↦ V,
    k_sub_V.trans (iUnion_const V).symm.subset,
    fun _ ↦
      ⟨V_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) h_sub_U (UV_dis.closure_right U_open).symm⟩⟩⟩

Result:
no goals

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

Tactic:
rcases h₀_cov xinh with ⟨un , ⟨n, rfl⟩ , 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 ∈ ⋃ n, u₀ n \ closure (⋃ m, ⋃ (_ : m ≤ n), v₀ m)

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
this : ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m')
⊢ x ∉ ⋃ n, v n \ closure (⋃ m, ⋃ (_ : m ≤ n), u m)

Tactic:
simpa

Result:
no goals