import data.set


namespace kuratowski

constant τ : Type

def pair (a b : set τ) : set (set (set τ)) := {{a}, {a, b}}

-- Wikipedia version
def π₂ (p : set (set (set τ))) := ⋃₀ { x | x ∈ ⋃₀ p ∧ (⋃₀ p ≠ ⋂₀ p → x
∉ ⋂₀ p) }
-- Slightly different implementation
def π₂' (p : set (set (set τ))) := ⋃ (x ∈ ⋃₀ p) (_ : ⋃₀ p ≠ ⋂₀ p → x ∉
⋂₀ p), x

-- The projections really are the same.
example : π₂ = π₂' :=
begin
  funext p,
  unfold π₂ π₂',
  ext e,
  split,
  { rintro ⟨t, ⟨ht₁, ht₂⟩, he⟩,
    simp_rw set.mem_Union,
    use [t, ht₁, ht₂, he], },
  { simp_rw set.mem_Union,
    rintro ⟨t, ht₁, ht₂, he⟩,
    use [t, ht₁, ht₂, he], },
end


-- Wikipedia version
theorem it_works {a b : set τ} : π₂ (pair a b) = b :=
begin
  ext e,
  rw [π₂, pair],
  split,
  { have : {a} ∩ {a, b} = ({a} : set (set τ)) := by simp,
    simp [this, imp_false],
    rw set.ext_iff, simp,
    rintro rfl he,
    exact he, },
  { intro he,
    use b,
    simp,
    exact ⟨by rintro h rfl; apply h; simp, he⟩, },
end


-- the other version
theorem it_works' {a b : set τ} : π₂' (pair a b) = b :=
begin
  ext e,
  rw [π₂', pair],
  simp [imp_false],
  split,
  { rintro (⟨eq, he⟩ | ⟨_, he⟩),
    { rw set.ext_iff at eq,
      simp at eq,
      rwa eq, },
    { exact he, }, },
  { intro he,
    right,
    exact ⟨by apply mt; rintro rfl; simp, he⟩, },
end

end kuratowski