Lean: generalize a `set` abbreviation only catches hypotheses phrased with it

In a long Mathlib proof I had set ψ := towerInv e s and then have hyP := towerProj_towerInv y. generalize ψ y = p at ... hyP left hyP untouched, because hyP was elaborated as towerInv e s y, not ψ y. The fix is to state the type explicitly, have hyP : towerProj e (ψ y) = y := towerProj_towerInv y. After that, generalize + obtain ⟨x, L⟩ := p turned everything into plain variables, and omega could see that L and (ψ y).2 were the same atom. Before the fix it failed with counterexamples listing both as separate atoms. Two related things: omega also treats r x and returnTimeNat e s x (r := returnTimeNat e s, introduced by set) as different atoms, and (by show _ < r x; omega) fixes that. Omega cannot reason about % n for a variable n, so prove (L + k) % n = k from L % n = 0 with Nat.add_mod, Nat.mod_mod, Nat.mod_eq_of_lt.