Commit 2024-04-30 16:16 a41b81fd

perf: make LocalInvariantProp a structure (#12552)

• Also redefine MDifferentiableWithinAt and MDifferentiableAt so that they are using LiftProp[Within]At.
• This causes a speedup in the old proof of ContMDiffWithinAt.cle_arrowCongr by 25%.
• Also give some extra information in the proof of ContMDiffWithinAt.cle_arrowCongr to speed it up by another factor of 4.
• A bit of the fallout (e.g. in hasSmoothAddSelf) is from Lean unfolding way too many definitions to make things definitionally equal. Since LiftPropWithinAt is now a structure, the old proofs now break, unless you rewrite with chartedSpaceSelf_prod), causing much less defeq-abuse.
• The new lemmas MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt and MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt have a bit long names. This is to avoid naming clash with the existing MDifferentiableWithinAt.differentiableWithinAt. I'm open for other suggestions.