A `strict_mono` function from `ℕ` is determined by its image

Stream: Is there code for X?

[Shing Tak Lam]

import data.real.basic

lemma exists_of_range_eq_range {α : Type*} {f g : ℕ → α}
  (hfg : set.range f = set.range g) (n : ℕ) :
  ∃ k, f n = g k :=
begin
  have h₁ : f n ∈ set.range g,
  { simp [←hfg] },
  rcases h₁ with ⟨t, ht⟩,
  use t, rw ht
end

-- mainly looking for this one
lemma eq_of_strict_mono_of_range_eq {α : Type*} [linear_order α] {f g : ℕ → α} (hf : strict_mono f)
  (hg : strict_mono g) (hfg : set.range f = set.range g) : f = g :=
begin
  ext i,
  apply nat.strong_induction_on i,
  clear i,
  intros i ih,
  by_contra h,
  cases ne.lt_or_lt h with h₁ h₁,
  { cases exists_of_range_eq_range hfg i with m hm,
    have hmi : m < i,
    { rwa [hm, hg.lt_iff_lt] at h₁ },
    specialize ih m hmi,
    rwa [←hf.lt_iff_lt, hm, ih] at hmi,
    exact lt_irrefl _ hmi },
  { cases exists_of_range_eq_range hfg.symm i with m hm,
    have hmi : m < i,
    { rwa [hm, hf.lt_iff_lt] at h₁ },
    specialize ih m hmi,
    rwa [←hg.lt_iff_lt, hm, ih] at hmi,
    exact lt_irrefl _ hmi }
end

I can't seem to find this in mathlib at the moment.

[Heather Macbeth]

Perhaps
https://leanprover-community.github.io/mathlib_docs/order/order_iso_nat.html
is useful. It contains related results. For example, your result is equivalent to the fact that the embedding constructed in docs#nat.order_embedding_of_set is unique.

[Heather Macbeth]

Another phrasing: there exists a unique strict-mono function (or, a unique order-iso) from ℕ to itself. It seems mathlib has these for fin:
docs#fin.strict_mono_unique
docs#fin.order_embedding_eq
but I don't see the result for ℕ.