prevent push_cast, ring_nf etc. from unfolding local defs?

Stream: mathlib4

[Michael Stoll]

Is there a way to stop tactics like push_cast, ring_nf etc. from unfolding local definitions like set m := ...? The point of the set is to hide complexities in the terms, and so it is a bit annoying when tactics re-complexify things without being asked to do so...

[Yury G. Kudryashov]

As far as I understand, the default configuration of simp changed from Lean 3 to Lean 4 and quite a few tactics don't adjust the default yet.

[Yury G. Kudryashov]

See #7592 for a fix for push_neg.

[Yury G. Kudryashov]

Though a recent PR #7884 by @Scott Morrison says "the change in behaviour in simp (currently, but not for much longer, requiring zeta := false)". Does it mean that simp is going to change the default back to zeta := false or something else?

[Mauricio Collares]

That's lean4#2682