replace this := congr_arg f (this (f 1))
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : ∀ (n : ℕ), f (n * f 1) = n
⊢ f 1 = 1
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : f (f (f 1 * f 1)) = f (f 1)
⊢ f 1 = 1