countable_of_surjective

proof body

Tactic-mode proof.

  27  -- Build an injection α → ℕ from the surjection
  28  classical
  29  let g : α → ℕ := fun a => Nat.find (hf a)
  30  have hg : ∀ a, f (g a) = a := fun a => Nat.find_spec (hf a)
  31  -- g is a left inverse, hence injective
  32  have hinj : Injective g := by
  33    intro a₁ a₂ heq
  34    calc a₁ = f (g a₁) := (hg a₁).symm
  35      _ = f (g a₂) := by rw [heq]
  36      _ = a₂ := hg a₂
  37  -- Use mathlib's Countable constructor (exists in Lean 4)
  38  exact ⟨g, hinj⟩
  39
  40/-! ### Enumeration from countability -/
  41
  42/-- From `Countable α` and inhabitedness, produce a surjection `ℕ → α`.
  43
  44**Proof strategy**: Use `Nonempty.some` to extract the injection witness from `Countable`,
  45then invert it classically to build a surjection.
  46
  47The challenge is that `Countable α := ∃ f, Injective f` is in `Prop`, but we need
  48to use the witness `f` in a `Type`-producing definition. We use `Nonempty` coercion. -/