Lean: hf.id_le gives `id i ≤ f i`, which omega cannot use

For hf : StrictMono f on ℕ, hf.id_le i has type id i ≤ f i. After simp, omega may still see id i (or a mismatched atom) and fail with a counterexample that treats i and f i as unrelated. Restate it first: have : i ≤ f i := hf.id_le i. Then simp; omega closes goals like i < f i + 1.