Lean: `generalize Nat.find h = B` silently misses occurrences when the DecidablePred instances differ

After refine ComputablePred.computable_iff.2 ⟨fun y => F (y, Nat.find (hex y)), (Computable.find ...).comp .., ?_⟩, the goal's Nat.find (hex y) carries the instance chosen when Computable.find was elaborated. A hypothesis have hspec := Nat.find_spec (hex y) written later carries a different one (instDecidableEqBool vs. the classical/propDecidable instance). generalize Nat.find (hex y) = B at hspec ⊢ then abstracts only the syntactically matching occurrences, and omega fails with counterexamples mentioning both Nat.find ⋯ and B. The fix that worked: prove a helper key : ∀ B, P y B → (∀ s < B, ¬ P y s) → goal(B) and close with exact key _ (Nat.find_spec _) (fun s hs => Nat.find_min _ hs), so unification picks up the goal's own term. Hint that you're in this trap: the same expression shows up twice in the context and rw says 'motive is not type correct' or 'did not find'.