α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ SeparatedNhds s t
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
⊢ NormalSpace α
refine' ⟨fun s t hs ht hd => _⟩
case intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
⊢ SeparatedNhds s t
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ SeparatedNhds s t
rcases key ht hd with ⟨U, hsU, hUd, hUc⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
⊢ SeparatedNhds s t
case intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
⊢ SeparatedNhds s t
rcases key hs hd.symm with ⟨V, htV, hVd, hVc⟩
case intro.intro.intro.intro.intro.intro.refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
⊢ x ∈
    ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U),
      ↑u \ ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v

case intro.intro.intro.intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
⊢ x ∈
    ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V),
      ↑v \ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ Encodable.encode v), closure ↑u

case intro.intro.intro.intro.intro.intro.refine_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
⊢ Disjoint
    (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U),
      ↑u \ ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v)
    (⋃ (v : ↑(countableBasis α)) (_ : v ∈ V),
      ↑v \ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ Encodable.encode v), closure ↑u)
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
⊢ SeparatedNhds s t
refine ⟨⋃ u ∈ U, ↑u \ ⋃ (v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v,
  ⋃ v ∈ V, ↑v \ ⋃ (u ∈ U) (_ : Encodable.encode u ≤ Encodable.encode v), closure ↑u,
  isOpen_biUnion fun u _ => (isOpen_of_mem_countableBasis u.2).sdiff (hVc _),
  isOpen_biUnion fun v _ => (isOpen_of_mem_countableBasis v.2).sdiff (hUc _),
  fun x hx => ?_, fun x hx => ?_, ?_⟩
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : Disjoint s t
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
⊢ ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
intro s t hc hd
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : Disjoint s t
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
rw [disjoint_left] at hd
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
this : ∀ (x : α), x ∈ s → ∃ U, U ∈ countableBasis α ∧ x ∈ U ∧ Disjoint (closure U) t
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
have : ∀ x ∈ s, ∃ U ∈ countableBasis α, x ∈ U ∧ Disjoint (closure U) t := by
  intro x hx
  rcases (isBasis_countableBasis α).exists_closure_subset (hc.compl_mem_nhds (hd hx))
    with ⟨u, hu, hxu, hut⟩
  exact ⟨u, hu, hxu, disjoint_left.2 hut⟩
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
this : ∀ (x : α), x ∈ s → ∃ U, U ∈ countableBasis α ∧ x ∈ U ∧ Disjoint (closure U) t
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
choose! U hu hxu hd using this
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
set V : s → countableBasis α := MapsTo.restrict _ _ _ hu
case refine'_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
⊢ s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ range V), ↑u

case refine'_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
n : ℕ
⊢ IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ range V) (_ : Encodable.encode u ≤ n), closure ↑u)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
⊢ ∃ U,
    (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
      (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
        ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
refine' ⟨range V, _, forall_range_iff.2 <| Subtype.forall.2 hd, fun n => _⟩
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
x : α
hx : x ∈ s
⊢ ∃ U, U ∈ countableBasis α ∧ x ∈ U ∧ Disjoint (closure U) t
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
⊢ ∀ (x : α), x ∈ s → ∃ U, U ∈ countableBasis α ∧ x ∈ U ∧ Disjoint (closure U) t
intro x hx
case intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
x : α
hx : x ∈ s
u : Set α
hu : u ∈ countableBasis α
hxu : x ∈ u
hut : closure u ⊆ tᶜ
⊢ ∃ U, U ∈ countableBasis α ∧ x ∈ U ∧ Disjoint (closure U) t
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
x : α
hx : x ∈ s
⊢ ∃ U, U ∈ countableBasis α ∧ x ∈ U ∧ Disjoint (closure U) t
rcases (isBasis_countableBasis α).exists_closure_subset (hc.compl_mem_nhds (hd hx))
  with ⟨u, hu, hxu, hut⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
x : α
hx : x ∈ s
u : Set α
hu : u ∈ countableBasis α
hxu : x ∈ u
hut : closure u ⊆ tᶜ
⊢ ∃ U, U ∈ countableBasis α ∧ x ∈ U ∧ Disjoint (closure U) t
exact ⟨u, hu, hxu, disjoint_left.2 hut⟩
case refine'_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
⊢ s ⊆ ⋃ (y : ↑s), ↑(V y)
case refine'_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
⊢ s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ range V), ↑u
rw [biUnion_range]
no goals
case refine'_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
⊢ s ⊆ ⋃ (y : ↑s), ↑(V y)
exact fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, hxu x hx⟩
case refine'_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
n : ℕ
⊢ IsClosed
    (⨆ (u : ↑(countableBasis α)) (_ :
      u ∈ range (MapsTo.restrict (fun x => U x) s (countableBasis α) hu) ∧ Encodable.encode u ≤ n), closure ↑u)
case refine'_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
n : ℕ
⊢ IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ range V) (_ : Encodable.encode u ≤ n), closure ↑u)
simp only [← iSup_eq_iUnion, iSup_and']
no goals
case refine'_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
s t : Set α
hc : IsClosed t
hd✝ : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
U : α → Set α
hu : ∀ (x : α), x ∈ s → U x ∈ countableBasis α
hxu : ∀ (x : α), x ∈ s → x ∈ U x
hd : ∀ (x : α), x ∈ s → Disjoint (closure (U x)) t
V : ↑s → ↑(countableBasis α) := MapsTo.restrict (fun x => U x) s (countableBasis α) hu
n : ℕ
⊢ IsClosed
    (⨆ (u : ↑(countableBasis α)) (_ :
      u ∈ range (MapsTo.restrict (fun x => U x) s (countableBasis α) hu) ∧ Encodable.encode u ≤ n), closure ↑u)
exact isClosed_biUnion (((finite_le_nat n).preimage_embedding (Encodable.encode' _)).subset <|
  inter_subset_right _ _) fun u _ => isClosed_closure
case intro.intro.intro.intro.intro.intro.refine_1.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ ↑u
⊢ x ∈
    ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U),
      ↑u \ ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v
case intro.intro.intro.intro.intro.intro.refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
⊢ x ∈
    ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U),
      ↑u \ ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v
rcases mem_iUnion₂.1 (hsU hx) with ⟨u, huU, hxu⟩
case intro.intro.intro.intro.intro.intro.refine_1.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ ↑u
⊢ ¬x ∈ ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v
case intro.intro.intro.intro.intro.intro.refine_1.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ ↑u
⊢ x ∈
    ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U),
      ↑u \ ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v
refine' mem_biUnion huU ⟨hxu, _⟩
case intro.intro.intro.intro.intro.intro.refine_1.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ ↑u
⊢ ¬∃ i h i_1, x ∈ closure ↑i
case intro.intro.intro.intro.intro.intro.refine_1.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ ↑u
⊢ ¬x ∈ ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v
simp only [mem_iUnion]
case intro.intro.intro.intro.intro.intro.refine_1.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ ↑u
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ closure ↑v
⊢ False
case intro.intro.intro.intro.intro.intro.refine_1.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ ↑u
⊢ ¬∃ i h i_1, x ∈ closure ↑i
rintro ⟨v, hvV, -, hxv⟩
no goals
case intro.intro.intro.intro.intro.intro.refine_1.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ s
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ ↑u
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ closure ↑v
⊢ False
exact (hVd v hvV).le_bot ⟨hxv, hx⟩
case intro.intro.intro.intro.intro.intro.refine_2.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ ↑v
⊢ x ∈
    ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V),
      ↑v \ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ Encodable.encode v), closure ↑u
case intro.intro.intro.intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
⊢ x ∈
    ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V),
      ↑v \ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ Encodable.encode v), closure ↑u
rcases mem_iUnion₂.1 (htV hx) with ⟨v, hvV, hxv⟩
case intro.intro.intro.intro.intro.intro.refine_2.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ ↑v
⊢ ¬x ∈ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ Encodable.encode v), closure ↑u
case intro.intro.intro.intro.intro.intro.refine_2.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ ↑v
⊢ x ∈
    ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V),
      ↑v \ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ Encodable.encode v), closure ↑u
refine' mem_biUnion hvV ⟨hxv, _⟩
case intro.intro.intro.intro.intro.intro.refine_2.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ ↑v
⊢ ¬∃ i h i_1, x ∈ closure ↑i
case intro.intro.intro.intro.intro.intro.refine_2.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ ↑v
⊢ ¬x ∈ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ Encodable.encode v), closure ↑u
simp only [mem_iUnion]
case intro.intro.intro.intro.intro.intro.refine_2.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ ↑v
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ closure ↑u
⊢ False
case intro.intro.intro.intro.intro.intro.refine_2.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ ↑v
⊢ ¬∃ i h i_1, x ∈ closure ↑i
rintro ⟨u, huU, -, hxu⟩
no goals
case intro.intro.intro.intro.intro.intro.refine_2.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
x : α
hx : x ∈ t
v : ↑(countableBasis α)
hvV : v ∈ V
hxv : x ∈ ↑v
u : ↑(countableBasis α)
huU : u ∈ U
hxu : x ∈ closure ↑u
⊢ False
exact (hUd u huU).le_bot ⟨hxu, hx⟩
case intro.intro.intro.intro.intro.intro.refine_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
⊢ ∀ ⦃a : α⦄,
    (∃ i h, a ∈ ↑i ∧ ∀ (x : ↑(countableBasis α)), x ∈ V → Encodable.encode x ≤ Encodable.encode i → ¬a ∈ closure ↑x) →
      ∀ (x : ↑(countableBasis α)), x ∈ V → a ∈ ↑x → ∃ x_2 h h, a ∈ closure ↑x_2
case intro.intro.intro.intro.intro.intro.refine_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
⊢ Disjoint
    (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U),
      ↑u \ ⋃ (v : ↑(countableBasis α)) (_ : v ∈ V) (_ : Encodable.encode v ≤ Encodable.encode u), closure ↑v)
    (⋃ (v : ↑(countableBasis α)) (_ : v ∈ V),
      ↑v \ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ Encodable.encode v), closure ↑u)
simp only [disjoint_left, mem_iUnion, mem_diff, not_exists, not_and, not_forall, not_not]
case intro.intro.intro.intro.intro.intro.refine_3.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
a : α
u : ↑(countableBasis α)
huU : u ∈ U
hau : a ∈ ↑u
haV : ∀ (x : ↑(countableBasis α)), x ∈ V → Encodable.encode x ≤ Encodable.encode u → ¬a ∈ closure ↑x
v : ↑(countableBasis α)
hvV : v ∈ V
hav : a ∈ ↑v
⊢ ∃ x h h, a ∈ closure ↑x
case intro.intro.intro.intro.intro.intro.refine_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
⊢ ∀ ⦃a : α⦄,
    (∃ i h, a ∈ ↑i ∧ ∀ (x : ↑(countableBasis α)), x ∈ V → Encodable.encode x ≤ Encodable.encode i → ¬a ∈ closure ↑x) →
      ∀ (x : ↑(countableBasis α)), x ∈ V → a ∈ ↑x → ∃ x_2 h h, a ∈ closure ↑x_2
rintro a ⟨u, huU, hau, haV⟩ v hvV hav
case intro.intro.intro.intro.intro.intro.refine_3.intro.intro.intro.inl
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
a : α
u : ↑(countableBasis α)
huU : u ∈ U
hau : a ∈ ↑u
haV : ∀ (x : ↑(countableBasis α)), x ∈ V → Encodable.encode x ≤ Encodable.encode u → ¬a ∈ closure ↑x
v : ↑(countableBasis α)
hvV : v ∈ V
hav : a ∈ ↑v
hle : Encodable.encode u ≤ Encodable.encode v
⊢ ∃ x h h, a ∈ closure ↑x

case intro.intro.intro.intro.intro.intro.refine_3.intro.intro.intro.inr
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
a : α
u : ↑(countableBasis α)
huU : u ∈ U
hau : a ∈ ↑u
haV : ∀ (x : ↑(countableBasis α)), x ∈ V → Encodable.encode x ≤ Encodable.encode u → ¬a ∈ closure ↑x
v : ↑(countableBasis α)
hvV : v ∈ V
hav : a ∈ ↑v
hle : Encodable.encode v ≤ Encodable.encode u
⊢ ∃ x h h, a ∈ closure ↑x
case intro.intro.intro.intro.intro.intro.refine_3.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
a : α
u : ↑(countableBasis α)
huU : u ∈ U
hau : a ∈ ↑u
haV : ∀ (x : ↑(countableBasis α)), x ∈ V → Encodable.encode x ≤ Encodable.encode u → ¬a ∈ closure ↑x
v : ↑(countableBasis α)
hvV : v ∈ V
hav : a ∈ ↑v
⊢ ∃ x h h, a ∈ closure ↑x
cases' le_total (Encodable.encode u) (Encodable.encode v) with hle hle
no goals
case intro.intro.intro.intro.intro.intro.refine_3.intro.intro.intro.inl
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
a : α
u : ↑(countableBasis α)
huU : u ∈ U
hau : a ∈ ↑u
haV : ∀ (x : ↑(countableBasis α)), x ∈ V → Encodable.encode x ≤ Encodable.encode u → ¬a ∈ closure ↑x
v : ↑(countableBasis α)
hvV : v ∈ V
hav : a ∈ ↑v
hle : Encodable.encode u ≤ Encodable.encode v
⊢ ∃ x h h, a ∈ closure ↑x

case intro.intro.intro.intro.intro.intro.refine_3.intro.intro.intro.inr
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : T3Space α
key :
  ∀ {s t : Set α},
    IsClosed t →
      Disjoint s t →
        ∃ U,
          (s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u) ∧
            (∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t) ∧
              ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
s t : Set α
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
U : Set ↑(countableBasis α)
hsU : s ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ U), ↑u
hUd : ∀ (u : ↑(countableBasis α)), u ∈ U → Disjoint (closure ↑u) t
hUc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ U) (_ : Encodable.encode u ≤ n), closure ↑u)
V : Set ↑(countableBasis α)
htV : t ⊆ ⋃ (u : ↑(countableBasis α)) (_ : u ∈ V), ↑u
hVd : ∀ (u : ↑(countableBasis α)), u ∈ V → Disjoint (closure ↑u) s
hVc : ∀ (n : ℕ), IsClosed (⋃ (u : ↑(countableBasis α)) (_ : u ∈ V) (_ : Encodable.encode u ≤ n), closure ↑u)
a : α
u : ↑(countableBasis α)
huU : u ∈ U
hau : a ∈ ↑u
haV : ∀ (x : ↑(countableBasis α)), x ∈ V → Encodable.encode x ≤ Encodable.encode u → ¬a ∈ closure ↑x
v : ↑(countableBasis α)
hvV : v ∈ V
hav : a ∈ ↑v
hle : Encodable.encode v ≤ Encodable.encode u
⊢ ∃ x h h, a ∈ closure ↑x
exacts [⟨u, huU, hle, subset_closure hau⟩, (haV _ hvV hle <| subset_closure hav).elim]