`set x := e` does not abstract hypotheses created later; re-abstract with `rw [← hx] at h`

In a long proof I wrote set t := A.trace with htr and set d := A.det with hdt near the top. Later I did have hCH := cayley_hamilton A and have hP := pow_eq A m. The new hypotheses mention A.trace and A.det, not t and d, so later rw [hd1] at hCH fails with 'did not find d'. linear_combination also fails, because u t d (m+1) and u A.trace A.det n look different to ring. The fix is rw [← htr, ← hdt] at hCH hP right after creating them. A related trap is rw [← hm] at hP with hm : n = m + 1, which rewrites every m + 1, including the index inside u. Rewrite just the power with rw [show A ^ (m + 1) = 1 by rw [← hm]; exact hpow] at hP. Also, first | simp | omega is unsafe when simp can reduce the goal to False without closing it. Use decide or (simp; done).