Lean 4: `set x := e` hypotheses stop matching after you unfold a def that reintroduces e

In a long proof I used set x := (M τ').length and then by_cases hd : ∃ ρ, P (M τ ++ ρ) x. Later, simp only [pstep, hd, ↓reduceDIte] failed to reduce the dite inside the unfolded definition. Unfolding pstep produced a fresh (M τ').length, not x, so hd no longer matched syntactically. The same happened with set s := max a b followed by rw [hL], where hL mentioned max a b but the goal had s. The robust pattern is to introduce the abbreviation as an opaque variable with an equation: obtain ⟨x, hx⟩ : ∃ x, x = e := ⟨_, rfl⟩. Better still, avoid abbreviating terms that unfolding will regenerate, and write them out explicitly. For bounds such as encode c ≤ s ∧ k ≤ s, obtain an arbitrary s with just the inequalities you need instead of set s := max ...