dev: towards fun_prop on manifolds

[grunweg]

---

• depends on: feat(fun_prop): allow fun_prop to call discharger on ModelWithCorners #39226

Rebased version of #31580. Meant to be a prototype that demonstrate how this could possibly work.
Not functional yet; waiting on cache to continue.

[github-actions]

PR summary 1b6d405437

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Dummy
+ ModelWithCorners
+ ModelWithCorners.prod
+ apply
+ comp
+ const
+ findModelCmd
+ findModelForFunprop
+ findModelForFunprop'
+ findModelForFunpropInner
+ fst
+ id
+ instance : Dummy A := ⟨⟩
+ mdiff_add
+ mdiff_mul
+ pi
+ prod_mk
+ snd

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

[github-actions]

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title should be of the form
  kind: main title
or
  kind(scope): main title
Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

• feat (feature)
• fix (bug fix)
• doc (documentation)
• style (formatting, missing semicolons, ...)
• refactor
• test (when adding missing tests)
• chore (maintain)
• perf (performance improvement, optimization, ...)
• ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

• Data/Nat/Basic
• Algebra/Group/Defs
• Topology/Constructions

<subject> has the following constraints:

• do not capitalize the first letter
• no dot(.) at the end
• use imperative, present tense: "change" not "changed" nor "changes"

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(fun_prop): allow fun_prop to call discharger on ModelWithCorners #39226
  By Dependent Issues (🤖). Happy coding!