PR summary 4e83c73533

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

./scripts/reporting/technical-debt-metrics.sh pr_summary

Looks good to me! I didn't know about the existence of withCanUnfoldPred. Thanks for recognizing this inconsistency and for fixing it.

I appreciate you fixing this! I understand on the first pass just fixing the broken bits by any means necessary, but now that they are isolated, would you mind going back and figuring out what fun_prop tags are missing to fix some of the breakage? That seems like a better solution.

I appreciate you fixing this! I understand on the first pass just fixing the broken bits by any means necessary, but now that they are isolated, would you mind going back and figuring out what fun_prop tags are missing to fix some of the breakage? That seems like a better solution.

Taking a look through these all seem subtler than missing fun_prop lemmas. For example the pattern eta_expand; dsimp; fun_prop appears because you should have to unfold a non irreducible definition manually, and the dsimp lemma that lets you do this is only given in an "apply" form.

Perhaps one solution is to experiment with preprocessing in fun_prop as suggested in this thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Using.20fun_prop.20for.20the.20sum.20of.20two.20continuous.20functions. Note eta_expand; dsimp; fun_prop also proves the second example by Aaron at the top of the thread (on an earlier version of mathlib without the additional fun_prop lemma added).

This pull request has conflicts, please merge master and resolve them.

This pull request has conflicts, please merge master and resolve them.

This pull request has conflicts, please merge master and resolve them.