/-
Copyright (c) 2015 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad

Two sets are equinumerous, or equipollent, if there is a bijection between them. It is sometimes
said that two such sets "have the same cardinality."
-/
import .classical_inverse data.nat
open eq.ops classical nat

/- two versions of Cantor's theorem -/

namespace set

variables {X : Type} {A : set X}

theorem not_surj_on_pow (f : X β†’ set X) : Β¬ surj_on f A (𝒫 A) :=
let diag := {x ∈ A | x βˆ‰ f x} in
have diag βŠ† A, from sep_subset _ _,
assume H : surj_on f A (𝒫 A),
obtain x [(xA : x ∈ A) (Hx : f x = diag)], from H `diag βŠ† A`,
have x βˆ‰ f x, from
  suppose x ∈ f x,
  have x ∈ diag, from Hx β–Έ this,
  have x βˆ‰ f x, from and.right this,
  show false, from this `x ∈ f x`,
have x ∈ diag, from and.intro xA this,
have x ∈ f x, from Hx⁻¹ β–Έ this,
show false, from `x βˆ‰ f x` this

theorem not_inj_on_pow {f : set X β†’ X} (H : maps_to f (𝒫 A) A) : Β¬ inj_on f (𝒫 A) :=
let diag := f '[{x ∈ 𝒫 A | f x βˆ‰ x}] in
have diag βŠ† A, from image_subset_of_maps_to H (sep_subset _ _),
assume H₁ : inj_on f (𝒫 A),
have f diag ∈ diag, from by_contradiction
  (suppose f diag βˆ‰ diag,
    have diag ∈ {x ∈ 𝒫 A | f x βˆ‰ x}, from and.intro `diag βŠ† A` this,
    have f diag ∈ diag, from mem_image_of_mem f this,
    show false, from `f diag βˆ‰ diag` this),
obtain x [(Hx : x ∈ 𝒫 A ∧ f x βˆ‰ x) (fxeq : f x = f diag)], from this,
have x = diag, from H₁ (and.left Hx) `diag βŠ† A` fxeq,
have f diag βˆ‰ diag, from this β–Έ and.right Hx,
show false, from this `f diag ∈ diag`

end set

/-
The SchrΓΆder-Bernstein theorem. The proof below is nonconstructive, in three ways:
(1) We need a left inverse to g (we could get around this by supplying one).
(2) The definition of h below assumes that membership in Union U is decidable.
(3) We ultimately case split on whether B is empty, and choose an element if it isn't.

Rather than mark every auxiliary construction as "private", we put them all in a
separate namespace.
-/

namespace schroeder_bernstein
section
open set
  parameters {X Y : Type}
  parameter  {A : set X}
  parameter  {B : set Y}
  parameter  {f : X β†’ Y}
  parameter  (f_maps_to : maps_to f A B)
  parameter  (finj : inj_on f A)
  parameter  {g : Y β†’ X}
  parameter  (g_maps_to : maps_to g B A)
  parameter  (ginj : inj_on g B)
  parameter  {dflt : Y}                    -- for now, assume B is nonempty
  parameter  (dfltB : dflt ∈ B)

  /- g⁻¹ : A β†’ B -/

  noncomputable definition ginv : X β†’ Y := inv_fun g B dflt

  lemma ginv_maps_to : maps_to ginv A B :=
  maps_to_inv_fun dfltB

  lemma ginv_g_eq {b : Y} (bB : b ∈ B) : ginv (g b) = b :=
  left_inv_on_inv_fun_of_inj_on dflt ginj bB

  /- define a sequence of sets U -/

  definition U : β„• β†’ set X
  | U 0       := A \ g '[B]
  | U (n + 1) := g '[f '[U n]]

  lemma U_subset_A : βˆ€ n, U n βŠ† A
  | 0       := show U 0 βŠ† A,
                 from diff_subset _ _
  | (n + 1) := have f '[U n] βŠ† B,
                 from image_subset_of_maps_to f_maps_to (U_subset_A n),
               show U (n + 1) βŠ† A,
                 from image_subset_of_maps_to g_maps_to this

  lemma g_ginv_eq {a : X} (aA : a ∈ A) (anU  : a βˆ‰ Union U) : g (ginv a) = a :=
  have a ∈ g '[B], from by_contradiction
    (suppose a βˆ‰ g '[B],
      have a ∈ U 0, from and.intro aA this,
      have a ∈ Union U, from exists.intro 0 this,
      show false, from anU this),
  obtain b [(bB : b ∈ B) (gbeq : g b = a)], from this,
  calc
    g (ginv a) = g (ginv (g b)) : gbeq
           ... = g b            : ginv_g_eq bB
           ... = a              : gbeq

  /- h : A β†’ B -/

  noncomputable definition h x := if x ∈ Union U then f x else ginv x

  lemma h_maps_to : maps_to h A B :=
  take a,
  suppose a ∈ A,
  show h a ∈ B, from
    by_cases
      (suppose a ∈ Union U,
        by+ rewrite [↑h, if_pos this]; exact f_maps_to `a ∈ A`)
      (suppose a βˆ‰ Union U,
        by+ rewrite [↑h, if_neg this]; exact ginv_maps_to `a ∈ A`)

  /- h is injective -/

  lemma aux {a₁ aβ‚‚ : X} (H₁ : a₁ ∈ Union U) (aβ‚‚A : aβ‚‚ ∈ A) (heq : h a₁ = h aβ‚‚) : aβ‚‚ ∈ Union U :=
  obtain n (a₁Un : a₁ ∈ U n), from H₁,
  have ha₁eq : h a₁ = f a₁,
    from dif_pos H₁,
  show aβ‚‚ ∈ Union U, from by_contradiction
    (suppose aβ‚‚ βˆ‰ Union U,
      have haβ‚‚eq : h aβ‚‚ = ginv aβ‚‚,
        from dif_neg this,
      have g (f a₁) = aβ‚‚, from calc
        g (f a₁) = g (h a₁)       : ha₁eq
             ... = g (h aβ‚‚)       : heq
             ... = g (ginv aβ‚‚)    : haβ‚‚eq
             ... = aβ‚‚             : g_ginv_eq aβ‚‚A `aβ‚‚ βˆ‰ Union U`,
      have g (f a₁) ∈ g '[f '[U n]],
        from mem_image_of_mem g (mem_image_of_mem f a₁Un),
      have aβ‚‚ ∈ U (n + 1),
        from `g (f a₁) = aβ‚‚` β–Έ this,
      have aβ‚‚ ∈ Union U,
        from exists.intro _ this,
      show false, from `aβ‚‚ βˆ‰ Union U` `aβ‚‚ ∈ Union U`)

  lemma h_inj : inj_on h A :=
  take a₁ aβ‚‚,
  suppose a₁ ∈ A,
  suppose aβ‚‚ ∈ A,
  assume heq : h a₁ = h aβ‚‚,
  show a₁ = aβ‚‚, from
  by_cases
    (assume a₁UU : a₁ ∈ Union U,
      have aβ‚‚UU : aβ‚‚ ∈ Union U,
        from aux a₁UU `aβ‚‚ ∈ A` heq,
      have f a₁ = f aβ‚‚, from calc
        f a₁ = h a₁ : dif_pos a₁UU
          ... = h aβ‚‚ : heq
          ... = f aβ‚‚ : dif_pos aβ‚‚UU,
      show a₁ = aβ‚‚, from
        finj `a₁ ∈ A` `aβ‚‚ ∈ A` this)
    (assume a₁nUU : a₁ βˆ‰ Union U,
      have aβ‚‚nUU : aβ‚‚ βˆ‰ Union U,
        from assume H, a₁nUU (aux H `a₁ ∈ A` heq⁻¹),
      have eq₁ : g (ginv a₁) = a₁, from g_ginv_eq `a₁ ∈ A` a₁nUU,
      have eqβ‚‚ : g (ginv aβ‚‚) = aβ‚‚, from g_ginv_eq `aβ‚‚ ∈ A` aβ‚‚nUU,
      have ginv a₁ = ginv aβ‚‚, from calc
        ginv a₁ = h a₁ : dif_neg a₁nUU
            ... = h aβ‚‚ : heq
            ... = ginv aβ‚‚ : dif_neg aβ‚‚nUU,
      show a₁ = aβ‚‚, from calc
        a₁    = g (ginv a₁) : eq₁ -- g_ginv_eq `a₁ ∈ A` a₁nUU
          ... = g (ginv aβ‚‚) : this
          ... = aβ‚‚          : eqβ‚‚) -- g_ginv_eq `aβ‚‚ ∈ A` aβ‚‚nUU)

  /- h is surjective -/

  lemma h_surj : surj_on h A B :=
  take b,
  suppose b ∈ B,
  have g b ∈ A, from g_maps_to this,
  by_cases
    (suppose g b ∈ Union U,
       obtain n (gbUn : g b ∈ U n), from this,
      using ginj f_maps_to,
      begin
        cases n with n,
          {have g b ∈ U 0, from gbUn,
            have g b βˆ‰ g '[B], from and.right this,
            have g b ∈ g '[B], from mem_image_of_mem g `b ∈ B`,
            show b ∈ h '[A], from absurd `g b ∈ g '[B]` `g b βˆ‰ g '[B]`},
        {have g b ∈ U (succ n), from gbUn,
           have g b ∈ g '[f '[U n]], from this,
           obtain b' [(b'fUn : b' ∈ f '[U n]) (geq : g b' = g b)], from this,
           obtain a [(aUn : a ∈ U n) (faeq : f a = b')], from b'fUn,
           have g (f a) = g b, by rewrite [faeq, geq],
           have a ∈ A, from U_subset_A n aUn,
           have f a ∈ B, from f_maps_to this,
           have f a = b, from ginj `f a ∈ B` `b ∈ B` `g (f a) = g b`,
           have a ∈ Union U, from exists.intro n aUn,
           have h a = f a, from dif_pos this,
           show b ∈ h '[A], from mem_image `a ∈ A` (`h a = f a` ⬝ `f a = b`)}
      end)
    (suppose g b βˆ‰ Union U,
      have eq₁ : h (g b) = ginv (g b), from dif_neg this,
      have eqβ‚‚ : ginv (g b) = b, from ginv_g_eq `b ∈ B`,
      show b ∈ h '[A], from mem_image `g b ∈ A` (eq₁ ⬝ eqβ‚‚))
end
end schroeder_bernstein

namespace set
section
  parameters {X Y : Type}
  parameter  {A : set X}
  parameter  {B : set Y}
  parameter  {f : X β†’ Y}
  parameter  (f_maps_to : maps_to f A B)
  parameter  (finj : inj_on f A)
  parameter  {g : Y β†’ X}
  parameter  (g_maps_to : maps_to g B A)
  parameter  (ginj : inj_on g B)

  theorem schroeder_bernstein : βˆƒ h, bij_on h A B :=
  by_cases
    (assume H : βˆ€ b, b βˆ‰ B,
      have fsurj : surj_on f A B, from take b, suppose b ∈ B, absurd this !H,
      exists.intro f (and.intro f_maps_to (and.intro finj fsurj)))
    (assume H : Β¬ βˆ€ b, b βˆ‰ B,
      have βˆƒ b, b ∈ B, from exists_of_not_forall_not H,
      obtain b bB, from this,
      let h := @schroeder_bernstein.h X Y A B f g b in
      have h_maps_to : maps_to h A B, from schroeder_bernstein.h_maps_to f_maps_to bB,
      have hinj : inj_on h A, from schroeder_bernstein.h_inj finj ginj, -- ginj,
      have hsurj : surj_on h A B, from schroeder_bernstein.h_surj f_maps_to g_maps_to ginj,
      exists.intro h (and.intro h_maps_to (and.intro hinj hsurj)))
end
end set