[Merged by Bors] - refactor: don't expose definitions of immersions

[grunweg]

Instead of using an irreducible_def, make it an unexposed definition. This has the same effect in other modules,
but leads to much shorter code as we can remove all rw [foo_def] for the immersion definitions.
It also allows removing the @[expose] section from the file (which is nice).

There is a small downside: in downstream projects not using the module system, the definition of immersions
will be unfolded now. At this point, this is a mostly hypothetical risk (and weighs lower than the real benefits of this change). The discussion leading to this change did not have substantial evidence either.

Inspired by the discussion in #35122.

---

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[github-actions]

PR summary dd8018895f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsImmersionAt
+ IsImmersionAtOfComplement
+ instance (h : IsImmersionAt I J n f x) : NormedAddCommGroup h.complement
+ instance (h : IsImmersionAt I J n f x) : NormedSpace 𝕜 h.complement
- instance (h : IsImmersionAt I J n f x) : NormedAddCommGroup h.complement := by
- instance (h : IsImmersionAt I J n f x) : NormedSpace 𝕜 h.complement := by

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.

[chrisflav]

I think this is much better and more user friendly. I don't think the risk "downstream users now get to see the definition" is very big (I personally don't even think that this specific definition is so bad that it needs to be hidden). Long term, I would hope (/ expect) that every Lean project uses the module system by default.

[grunweg]

I agree, and have thus turned this into a proper PR.

[chrisflav]

Thanks!
maintainer merge

[github-actions]

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

[ocfnash]

Thanks, I agree this is much better.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

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