English
ofNat(s): ℕ → s is surjective onto s.
Русский
ofNat(s): ℕ → s сюръективно на s.
LaTeX
$$$\operatorname{Surjective}(\operatorname{Nat.Subtype.ofNat}(s))$$$
Lean4
theorem ofNat_surjective : Surjective (ofNat s)
| ⟨x, hx⟩ =>
by
set t : List s :=
((List.range x).filter fun y => y ∈ s).pmap (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
(by intro a ha; simpa using (List.mem_filter.mp ha).2) with
ht
have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩ := by simp [List.mem_filter, Subtype.ext_iff, ht]
cases hmax : List.maximum t with
| bot =>
refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (a := (⊥ : s)) ?_)⟩
rwa [← List.maximum_eq_bot.1 hmax, hmt]
| coe m =>
have wf : ↑m < x := by simpa using hmt.mp (List.maximum_mem hmax)
rcases ofNat_surjective m with ⟨a, rfl⟩
refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩
exact le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax
termination_by n => n.val
