induction' n using Nat.strong_induction_on with n n_ih
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
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