intro
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
⊢ ∀ (n : ℕ), f n = n
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
n✝ : ℕ
⊢ f n✝ = n✝