feat: extract_goal preserves explicit foralls #31342

Stream: PR reviews

[Kim Morrison]

Could I please ping on

feat: extract_goal preserves explicit foralls #31342

This was requested by an industrial user of Mathlib. I wrote the PR the same day they asked for it, but now it's been sitting on the queue for two weeks. :-)