[Merged by Bors] - chore: golf proofs of mdifferentiableAt_atlas{_symm}

[grunweg]

• introduce mdifferentiableAt_of_mem_maximalAtlas and mdifferentiableAt_symm_of_mem_maximalAtlas; these generalise the corresponding results to members of the maximal atlas;
• golf the proofs of these lemmas by re-using the corresponding results about maximal atlas members being C^n.

The second bullet slightly strenthens an import dependency (of this file on the corresponding C^n proofs): I consider this unproblematic since

• that dependency was already implicit before,
• there does not seem a pressing need to tease apart imports further; if such need arises, this proof can be reverted,
• for feat: if f is an immersion at x, then x is an immersed point #41796 (the first half of "the composition of immersions is an immersion"), I need versions of these lemmas for extended charts (which are known to be in the maximal atlas). This is a neat way to obtain this.

---

[github-actions]

PR summary 23143ef87d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ mdifferentiableAt_of_mem_maximalAtlas
+ mdifferentiableAt_symm_of_mem_maximalAtlas

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 23143ef).

• +2 new declarations
• −0 removed declarations

+mdifferentiableAt_of_mem_maximalAtlas
+mdifferentiableAt_symm_of_mem_maximalAtlas

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 23143ef87d
Reference commit c026161a58

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[fpvandoorn]

LGTM

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step
• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Build