Cantorの定理の難易度調整

[Seasawher]

単射バージョンが難しすぎるかも？（閃きがいる…かも）

よりステップごとに追っていけるようにヒントを追加したい

[Seasawher]

案:

1. 選択公理を使って逆写像を作り、全射バージョンに帰着させる方針で一度示す

2. 実は選択公理を使わずに示せる！と言って示させる

要するに全射と単射には双対性があるので、それを自力で閃いてほしい

[Seasawher]

選択公理を使って逆写像を作って全射バージョンに帰着させるコード

/- # 単射 A → B があれば、全射 B → A が作れる -/
import Mathlib.Logic.Function.Defs

open Function

variable {A B : Type}

-- 選択原理を使用する
open Classical in

/-- 単射 `f : A → B` があれば、選択原理を使用することにより
全射 `g : B → A` を作ることができる。 -/
theorem inj_to_surj [Inhabited A] (f : A → B) (hinj : Injective f) : ∃ g : B → A, Surjective g := by
  -- まず `g` を構成する。
  -- `g b` の値を構成するために、`g : B` が `f` の像に入っているかで場合分けをし、
  -- 入っていなければ適当な値、入っていれば `b = f a` となる `a` を返すようにする。
  let g := fun b =>
    if h : ∃ a, f a = b then Classical.choose h
    else default

  -- `g` の定義と `f` の単射性から、`g (f a) = a` が成り立つ。
  have gdef : ∀ a, g (f a) = a := by
    -- `a : A` が与えられたとする。
    intro a

    -- g の定義を展開する
    dsimp only [g]

    -- `f a` は明らかに `f` の像に入っているということを利用して、
    -- `g` の定義の中の `if` 式を簡約する。
    split
    case isFalse h =>
      have : ∃ a₁, f a₁ = f a := ⟨a, rfl⟩
      simp_all [this]

    -- 後は `f` の単射性から従う。
    case isTrue h =>
      have := Classical.choose_spec h
      apply hinj
      assumption

  -- `g` が全射であることを示したい。
  -- それには、`g ∘ f = id` を示せば十分。
  suffices ∀ a, g (f a) = a from by
    exists g
    intro a
    exists f a
    apply this

  -- `g ∘ f = id` を示す。
  exact show ∀ a, g (f a) = a from by
    -- `a : A` が与えられたとする。
    intro a

    -- `f` の単射性により、`f (g (f a)) = f a` を示せばよい。
    apply hinj

    -- それは先に示した `g (f a) = a` から従う。
    simp [gdef]