suffices this : ∀ n : ℕ, f (n * f 1) = n by
  replace this := congr_arg f (this (f 1))
  rw [h0, h0] at this
  exact Nat.eq_one_of_mul_eq_one_left this
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ f 1 = 1
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ ∀ (n : ℕ), f (n * f 1) = n