awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ (n : ℕ), u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
rcases :
  ∀ (n : ℕ) (xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u₀ n) n) x),
    Membership.mem (γ := Set X) (⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)) x
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)) x

Tactic:
rcases h₀_cov xinh with ⟨un, ⟨n, rfl⟩, xinun⟩

Premises used: rfl
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ (n : ℕ), u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u₀ n) n) x
simp : ∃ (i : ℕ), x ∈ u₀ i \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ i), v₀ m)
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)) x

Tactic:
simp only [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ (n : ℕ), u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u₀ n) n) x
⊢ ∃ (i : ℕ), x ∈ u₀ i \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ i), v₀ m)

Tactic:
⟨n, xinun, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ (n : ℕ), u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u₀ n) n) x
refine : x ∉ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
⊢ ∃ (i : ℕ), x ∈ u₀ i \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ i), v₀ m)

Tactic:
refine ⟨n, xinun, ?_⟩
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ (n : ℕ), u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u₀ n) n) x
⊢ x ∉ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)

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

Premises used: Set.disjoint_right, Set.mem_iUnion, exists_false, not_false_eq_true, closure_iUnion₂_le_nat
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
⊢ ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)

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_iUnion,
        exists_false, not_false_eq_true]
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
⊢ SeparatedNhds s t

Tactic:
⟨⋃ 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),
       ?_⟩

Premises used: SDiff.sdiff, closure, And.right, And.left, And.intro, Exists.intro, SeparatedNhds, Set.iUnion
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
mp :
  Disjoint.{u_1} (α := Set X) (⋃ (n : ℕ), u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m))
    (⋃ (n : ℕ), v n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), u 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),
       ?_⟩
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
mp :
  ∀ ⦃a : X⦄,
    Membership.mem (γ := Set X) (⋃ (n : ℕ), u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) a →
      a ∉ ⋃ (n : ℕ), v n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), u m)
⊢ Disjoint.{u_1} (α := Set X) (⋃ (n : ℕ), u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m))
    (⋃ (n : ℕ), v n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), u m))

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
this :
  ∀ (m : ℕ),
    x ∈ v m →
      Membership.mem (γ := Set X)
        (closure[inst] (⋃ (m' : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {m' : ℕ | m' ≤ m} m'), u m')) x
⊢ x ∉ ⋃ (n : ℕ), v n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), u m)

Tactic:
simpa
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
mp :
  ∀ (m : ℕ),
    x ∈ v m →
      Membership.mem (γ := Set X)
        (closure[inst] (⋃ (m' : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {m' : ℕ | m' ≤ m} m'), u m')) x
⊢ x ∉ ⋃ (n : ℕ), v n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), u m)

Tactic:
suffices ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m') by simpa
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
m : ℕ
xinvm : x ∈ v m
by_contra : ∀ (m_gt_n : ¬n ≤ m), False
⊢ n ≤ m

Tactic:
by_contra m_gt_n
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
m : ℕ
xinvm : x ∈ v m
m_gt_n : ¬n ≤ m
⊢ False

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

Premises used: not_le, subset_closure, le_of_lt, Set.mem_biUnion, And.right, Iff.mp
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
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))

Premises used: not_le, subset_closure, le_of_lt, Set.mem_biUnion, And.right, Iff.mp
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
m : ℕ
xinvm : x ∈ v m
⊢ n ≤ 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))
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
m : ℕ
xinvm : x ∈ v m
n_le_m : n ≤ m
⊢ Membership.mem (γ := Set X)
    (closure[inst] (⋃ (m' : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {m' : ℕ | m' ≤ m} m'), u m')) x

Tactic:
subset_closure (mem_biUnion n_le_m xinun.1)

Premises used: subset_closure, Set.mem_biUnion, And.left
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
m : ℕ
xinvm : x ∈ v m
n_le_m : n ≤ m
⊢ Membership.mem (γ := Set X)
    (closure[inst] (⋃ (m' : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {m' : ℕ | m' ≤ m} m'), u m')) x

Tactic:
exact subset_closure (mem_biUnion n_le_m xinun.1)

Premises used: subset_closure, Set.mem_biUnion
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t U V : Set X
U_open : IsOpen[inst] U
V_open : IsOpen[inst] V
h_sub_U : s ⊆ U
k_sub_V : t ⊆ V
UV_dis : Disjoint U V
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s

Tactic:
⟨⟨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⟩⟩⟩

Premises used: HasSubset.Subset.trans, Set.disjoint_of_subset, Set.iUnion_const, Eq.subset, Disjoint.closure_right, Disjoint.symm, And.intro, Exists.intro, Disjoint.closure_left, Eq.symm
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t U V : Set X
U_open : IsOpen[inst] U
V_open : IsOpen[inst] 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⟩⟩⟩
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
x : ℕ
⊢ Disjoint (closure[inst] ((fun (x : ℕ) ↦ (∅ : Set X)) x)) s

Tactic:
simp only [closure_empty, empty_disjoint]

Premises used: closure_empty, Set.empty_disjoint
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
x : ℕ
⊢ Disjoint.{u_1} (α := Set X) (closure[inst] ((fun (x : ℕ) ↦ (univ : Set X)) x)) ∅

Tactic:
apply disjoint_empty

Premises used: Set.disjoint_empty
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
sc_st : HasSeparatingCover s₂ t₂
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
obtain :
  ∀ (u : ℕ → Set X) (u_cov : s₂ ⊆ ⋃ (n : ℕ), u n)
    (u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t₂), HasSeparatingCover s₁ t₁
⊢ HasSeparatingCover s₁ t₁

Tactic:
obtain ⟨u, u_cov, u_props⟩ := sc_st
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
u : ℕ → Set X
u_cov : s₂ ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t₂
⊢ HasSeparatingCover s₁ t₁

Tactic:
⟨u,
     s_sub.trans u_cov,
     fun n ↦
       ⟨(u_props n).1,
        disjoint_of_subset (fun ⦃_⦄ a ↦ a) t_sub (u_props n).2⟩⟩

Premises used: HasSubset.Subset.trans, HasSeparatingCover, Set.disjoint_of_subset, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
u : ℕ → Set X
u_cov : s₂ ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t₂
⊢ HasSeparatingCover s₁ t₁

Tactic:
exact
    ⟨u,
     s_sub.trans u_cov,
     fun n ↦
       ⟨(u_props n).1,
        disjoint_of_subset (fun ⦃_⦄ a ↦ a) t_sub (u_props n).2⟩⟩
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t → SeparatedNhds t s

Tactic:
fun ⟨U, V, oU, oV, aU, bV, UV⟩ =>
  ⟨V, U, oV, oU, bV, aU, Disjoint.symm UV⟩

Premises used: Disjoint.symm, And.intro, Exists.intro, SeparatedNhds, _private.0.SeparatedNhds.symm.match_1
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t ↔ SeparatedNhds t s

Tactic:
⟨symm, symm⟩

Premises used: SeparatedNhds.symm, Iff.intro
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s t : Set Y
h : SeparatedNhds s t
hf : Continuous[inst, inst_1] f
⊢ SeparatedNhds (f ⁻¹' s) (f ⁻¹' t)

Tactic:
let ⟨U, V, oU, oV, sU, tV, UV⟩ := h
  ⟨f ⁻¹' U, f ⁻¹' V, oU.preimage hf, oV.preimage hf, preimage_mono sU, preimage_mono tV,
    UV.preimage f⟩

Premises used: Set.preimage_mono, Set.preimage, And.intro, Exists.intro, SeparatedNhds, _private.0.SeparatedNhds.symm.match_1, IsOpen.preimage, Disjoint.preimage
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
h : SeparatedNhds s t
⊢ Disjoint s t

Tactic:
let ⟨_, _, _, _, hsU, htV, hd⟩ := h; hd.mono hsU htV

Premises used: Disjoint, Disjoint.mono, _private.0.SeparatedNhds.disjoint.match_1
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
h : SeparatedNhds s t
⊢ Disjoint (closure[inst] s) t

Tactic:
let ⟨_U, _V, _, hV, hsU, htV, hd⟩ := h
  (hd.closure_left hV).mono (closure_mono hsU) htV

Premises used: Disjoint, closure_mono, closure, Disjoint.mono, _private.0.SeparatedNhds.symm.match_1, Disjoint.closure_left
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
h : SeparatedNhds s t
⊢ Disjoint s (closure[inst] t)

Tactic:
h.symm.disjoint_closure_left.symm

Premises used: SeparatedNhds.disjoint_closure_left, SeparatedNhds.symm, Disjoint.symm
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ SeparatedNhds s ∅

Tactic:
⟨_, _, isOpen_univ, isOpen_empty, fun a _ => mem_univ a, Subset.rfl, disjoint_empty _⟩

Premises used: isOpen_univ, Set.Subset.rfl, And.intro, Exists.intro, Set.disjoint_empty, Set.mem_univ, SeparatedNhds, isOpen_empty
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ SeparatedNhds ∅ s

Tactic:
(empty_right _).symm

Premises used: SeparatedNhds.symm, SeparatedNhds.empty_right
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h : SeparatedNhds s₂ t₂
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ SeparatedNhds s₁ t₁

Tactic:
let ⟨U, V, hU, hV, hsU, htV, hd⟩ := h
  ⟨U, V, hU, hV, hs.trans hsU, ht.trans htV, hd⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro, SeparatedNhds, _private.0.SeparatedNhds.symm.match_1
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t u : Set X
⊢ SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u

Tactic:
simpa only [separatedNhds_iff_disjoint, nhdsSet_union, disjoint_sup_left] using And.intro

Premises used: nhdsSet_union, separatedNhds_iff_disjoint, And.intro, disjoint_sup_left