[Merged by Bors] - feat: custom elaborators for TangentSpace and tangentMap(Within)

[grunweg]

And use these to golf the differential geometry files a bit further.

---

[github-actions]

PR summary 2c951fc10b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ instance : RiemannianBundle (fun (x : F) ↦ TangentSpace% x)
- instance : RiemannianBundle (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x)

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 2c951fc).

• +3 new declarations
• −0 removed declarations

+Manifold.«termTangentMap%__»
+Manifold.«termTangentMap[_]__»
+Manifold.«termTangentSpace%__»

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 2c951fc10b
Reference commit 6923f2f175

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).

[mathlib-merge-conflicts]

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

[ocfnash]

Modulo ~15 lines of meta code and a question about tests this is all fine.

We'll need to find another reviewer for the meta code though.

[JovanGerb]

I think that a better approach than ensureIsFunction <|← Term.elabTerm _ none would be to propagate the expected type in the elaboration, and use elabTermEnsuringType (which should fill in the function coercion).

But that extra complication need not be part of this PR.

[grunweg]

Let's leave that to a follow-up PR: if so, all other elaborators should be changed similarly.

[JovanGerb]

Is your plan to add corresponding delaborators in the future?

[grunweg]

Is your plan to add corresponding delaborators in the future?

Yes - doing this for all elaborators where this is missing is part of @scholzhannah's master's thesis :-)

[JovanGerb]

Ok, thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by JovanGerb.

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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

[ocfnash]

Thanks, sorry we were so slow here!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

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