What's the general fix for Lean too eagerly unfolding

Stream: mathlib4

[Arien Malec]

I'm having an issue in mathlib4#1179 where I get a proof to the state where it unfolds too far. The issue strikes mem_fix_iff where a simp isn't hitting places it's supposed to hit because Lean 4 isn't recognizing the current state as pretty printable, and I have the same issue trying to fix prodMap_comp_comp, fixInduction'_stop, ixInduction'_fwd

(I'm also seeing strange errors in generalize_proofs for fixInduction and fix_induction_spec with unknown free variable '_uniq.71572'

Any help for this PR is appreciated -- I've fixed a bunch here, but I'm staring at the rest crosseyed.