PR summary ba1699697a

Import changes for modified files

No significant changes to the import graph

Declarations diff

+ ContMDiff.congr
+ contMDiff_congr

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

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

You could golf this by one line by proving ContMDiff.congr using contMDiff_congr - but either way, looks good to me. I'm a bit surprised that we're phrasing equality of functions as ∀ y, f₁ y = f y instead of f₁ = f here, but Continuous.congr also does it, so it makes sense to stay consistent.

You're right about the golf, good catch!
About the function equality: in general, there is a difference for dependent functions (e.g., sections of a vector bundle): saying f = g makes it not apply to dependent functions. In this case, that's probably no problem (as ContMDiff requires non-dependent functions anyway, and e.g. using TotalSpace.mk(') to turn a section into a function into the total space).

At the same time, staying consistent is good: if we wanted to change this, that should be a separate PR changing all such lemmas.

Let's hope rebasing fixes the CI error!

bors r+

Pull request successfully merged into master.

Build succeeded:

• CI Success