chore: convenience constructor for IsImmersionAtOfComplement

[grunweg]

Add a version of mk_of_continuousAt specialized to the preferred chart at each point.

---

• depends on: feat: post-composing an immersion with a diffeomorphism yields an immersion #41203

Open questions:

• should we get also a version with e.g. just the domain/or codomain chart being specified?
• Should we have the same for IsImmersionAt? This is not used in practice --- so would make for more predictable API, but not for shorter mathlib proofs.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: post-composing an immersion with a diffeomorphism yields an immersion #41203
  By Dependent Issues (🤖). Happy coding!