chase.lean

import topology.subset_properties
import topology.connected
import topology.nhds_set
import topology.inseparable
import topology.separation
import topology.maps

open function set filter topological_space
open_locale topological_space filter classical

universes u v
variables {α : Type u} {β : Type v} [topological_space α]

open separated

def function_diagonal (f: α → β): set (α × α) := prod.map f f ⁻¹' diagonal β



lemma t2_closed_func_diag [t2_space α] [topological_space β] [hb : nonempty β] {f:β → α} (hf : continuous f): is_closed (prod.map f f ⁻¹' diagonal α) :=
begin
  refine is_closed_iff_cluster_pt.mpr _,
  rintro ⟨ a₁, a₂ ⟩ h,
  refine eq_of_nhds_ne_bot ⟨ λ this : 𝓝 (f a₁) ⊓ 𝓝 (f a₂) = ⊥, h.ne _⟩,
  obtain ⟨ t₁, (ht₁ : t₁ ∈ 𝓝 (f a₁)), t₂, (ht₂ : t₂ ∈ 𝓝 (f a₂)), (h' : t₁ ∩ t₂ = ∅)⟩ :=
    inf_eq_bot_iff.mp this,
  obtain ha₁ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₁) ht₁,
  obtain ha₂ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₂) ht₂,
  rw [inf_principal_eq_bot, nhds_prod_eq],
  apply mem_of_superset (prod_mem_prod ha₁ ha₂),
  rintro ⟨x, y⟩ ⟨x_in, y_in⟩ (heq : f x = f y),
  apply set.not_mem_empty x,
  rw ← @set.preimage_empty _ _ f,
  rw ← h',
  rw set.preimage_inter,
  split,
  { exact x_in },
  { rw mem_preimage,
    rw heq,
    exact y_in }
end


lemma my_lemma [topological_space β] (hb : nonempty β) (f : β → α)
  (h : is_closed (function_diagonal f))
  (hf₁ : is_open_map f) (hf₂ : surjective f) : t2_space α :=
begin
  rw t2_space_iff_nhds,
  intros x y hneq₁,
  obtain ⟨p₁, hp₁⟩ := hf₂ x, subst hp₁,
  obtain ⟨p₂, hp₂⟩ := hf₂ y, subst hp₂,
  change (p₁, p₂) ∉ function_diagonal f at hneq₁,
  rw is_closed_iff_nhds at h,
  obtain ⟨N, hN⟩ := not_forall.mp (mt (h (p₁, p₂)) hneq₁),
  rw [not_forall, exists_prop, mem_nhds_prod_iff] at hN,
  obtain ⟨u, hu, v, hv, huv⟩ := hN.left,
  existsi f '' u, existsi is_open_map.image_mem_nhds hf₁ hu,
  existsi f '' v, existsi is_open_map.image_mem_nhds hf₁ hv,
  rw [disjoint_iff_inter_eq_empty, eq_empty_iff_forall_not_mem],
  intros s hs,
  apply hN.right,
  rw [mem_inter_iff, mem_image, mem_image] at hs,
  obtain ⟨z₁, hz₁, hz₁'⟩ := hs.left,
  obtain ⟨z₂, hz₂, hz₂'⟩ := hs.right, subst hz₂',
  existsi (z₁, z₂),
  split,
  { refine huv _, exact ⟨hz₁, hz₂⟩ },
  { exact hz₁' }
end