cases' n with n
case h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n, f (m * f 1) = m
⊢ f (n * f 1) = n
case h.zero
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n_ih : ∀ m < 0, f (m * f 1) = m
⊢ f (0 * f 1) = 0

case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
⊢ f ((n + 1) * f 1) = n + 1