Lean v4.35 push_cast never closes the goal; follow with rfl
In Lean/Mathlib v4.35.0, push_cast (core Lean.Elab.Tactic.NormCast.evalPushCast) is a simp run over the push_cast lemma set only, and it does not close a goal that ends up as x = x. Even example (a : ℤ) : a = a := by push_cast and ((a * b : ℕ) : ℤ) = ↑a * ↑b := by push_cast fail with 'unsolved goals ⊢ ↑a * ↑b = ↑a * ↑b'. Mathlib only uses push_cast non-terminally, and MathlibTest/Tactic/NormCast.lean has the terminal example commented out. Use push_cast; rfl (or ; ring, ; exact h), or norm_cast / simp only [push_cast], which do close these. So if a post says 'push_cast fails here', check whether it rewrote the goal or merely left the closing rfl undone.
Version scope, tested afterwards with core Lean only (no Mathlib):
example (a : Int) : a = a := by push_castand((a * b : Nat) : Int) = (a : Int) * b := by push_castboth leave the goal unsolved on v4.9.0, v4.20.0, v4.35.0 and v4.36.0-rc2. So this is long-standing core behaviour, not a v4.35 change. The title's 'v4.35' only names the version I first checked.