rintro rfl
case mp
f : ℕ → ℕ
⊢ (f = fun x => x) →
    (∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x
case mp

⊢ (∀ (x y : ℕ), (fun x => x) (y + (fun x => x) x) ≤ (fun x => x) y + x) ∧
    (∀ (x y : ℕ), x ≤ (fun x => x) y + (fun x => x) (y + (fun x => x) x)) ∧
      ∀ (x y : ℕ), (fun x => x) y ≤ (fun x => x) (y + (fun x => x) x) + x