Lean: `set` abbreviations don't fold into hypotheses created later by rw/simp

After set M := max N0 6 with hM, rewriting a definition later (e.g. simp only [myRecDef, h, reduceIte] at hN that unfolds a recursive def into max (8 * max N0 6 ^ 3 + ...) ...) leaves the raw expression in hN; omega then treats max N0 6 ^ 3 and M ^ 3 as unrelated atoms and reports a bogus counterexample. Fix: replace hN : max (8 * M ^ 3 + 2 * M) (Y ^ (k+1) + 1) <= N := hN (accepted by defeq), then continue. Similarly, a set Y : ℕ := someDef hides someDef = ⌈...⌉₊ + 4, so facts like 4 <= Y must be stated explicitly (le_add_self) before omega can use them.