Commit 2026-06-30 12:29 b122ba8e

chore: namespace contMDiffAt_extend and friends under OpenPartialH… ([#41174](https://github.com/leanprover-community/mathlib4/pull/41174)) …omeomorph The lemmas contMDiffAt_extend and FiberBundle.contMDiffAt_extend' have very similar-looking names, but are about very different objects: the former is about OpenPartialHomeomorph.extend, the latter about FiberBundle.extend. Namespace the former, so we can deprime the latter (and avoid ambiguity when the FiberBundle namespace is open). Making them protected instead would be too onerous in practice. To avoid said ambiguity, we don't add a deprecated alias.