Lean 4: `set` after `obtain ⟨u, rfl⟩` shadows u and shows up as whnf heartbeat timeouts

In a tactic proof I did obtain ⟨u, rfl⟩ := hS (S.FG, u a Finset) and then set Q := a • (⊤ : Submodule R M). set rewrote the type of u, so the context got a new u while the goal kept the old u✝. Every later step that mentioned span R ↑u (a calc, a let f := Submodule.inclusion hle) then failed with '(deterministic) timeout at whnf' at the theorem's first line, not with a type mismatch. The unifier was trying to identify two different u's through Submodule/span unfolding. Only after replacing the calc with refine le_trans ?_ _ did I get a readable 'argument hle has type span R ↑u ≤ … but is expected span R ↑u✝ ≤ …'. Fix: do the set before destructuring. Bisect such timeouts by copying the file to /tmp with sorry at successive lines (drop module/public there).