rw [h2, x_ih x x.lt_succ_self, le_iff_eq_or_lt, Nat.lt_succ_iff] at h
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + f 1) ≤ f x + 1
⊢ f (x + 1) = x + 1
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + 1) = x + 1 ∨ f (x + 1) ≤ x
⊢ f (x + 1) = x + 1