fix: rename definitions which use underscores in their name (#33103)

Per the naming convention, "all other terms of types" should be named in
lowerCamelCase: this applies to all changes made in this PR.

This PR is far from exhaustive.

Author: grunweg

Mathlib/Geometry/Manifold/IsManifold/Basic.lean

@@ -168,7 +168,7 @@ structure ModelWithCorners (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Ty
   source_eq : source = univ
   /-- To check this condition when the space already has a real normed space structure,
   use `Convex.convex_isRCLikeNormedField` which eliminates the `letI`s below, or the constructor
-  `ModelWithCorners.of_convex_range` -/
+  `ModelWithCorners.ofConvexRange` -/
   convex_range' :
     if h : IsRCLikeNormedField 𝕜 then
       letI := h.rclike 𝕜
@@ -185,7 +185,7 @@ lemma ModelWithCorners.range_eq_target {𝕜 E H : Type*} [NontriviallyNormedFie
   rw [← I.image_source_eq_target, I.source_eq, image_univ.symm]
 
 /-- If a model with corners has full range, the `convex_range'` condition is satisfied. -/
-def ModelWithCorners.of_target_univ (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+def ModelWithCorners.ofTargetUniv (𝕜 : Type*) [NontriviallyNormedField 𝕜]
     {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
     (φ : PartialEquiv H E) (hsource : φ.source = univ) (htarget : φ.target = univ)
     (hcont : Continuous φ) (hcont_inv : Continuous φ.symm) : ModelWithCorners 𝕜 E H where
@@ -202,12 +202,15 @@ def ModelWithCorners.of_target_univ (𝕜 : Type*) [NontriviallyNormedField 𝕜
     have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
     simp [this, htarget]
 
+@[deprecated (since := "2025-12-19")]
+alias ModelWithCorners.of_target_univ := ModelWithCorners.ofTargetUniv
+
 attribute [simp, mfld_simps] ModelWithCorners.source_eq
 
 /-- A vector space is a model with corners, denoted as `𝓘(𝕜, E)` within the `Manifold` namespace. -/
 def modelWithCornersSelf (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*)
     [NormedAddCommGroup E] [NormedSpace 𝕜 E] : ModelWithCorners 𝕜 E E :=
-  ModelWithCorners.of_target_univ 𝕜 (PartialEquiv.refl E) rfl rfl continuous_id continuous_id
+  ModelWithCorners.ofTargetUniv 𝕜 (PartialEquiv.refl E) rfl rfl continuous_id continuous_id
 
 @[inherit_doc] scoped[Manifold] notation "𝓘(" 𝕜 ", " E ")" => modelWithCornersSelf 𝕜 E
 
@@ -316,7 +319,7 @@ lemma _root_.Convex.convex_isRCLikeNormedField [NormedSpace ℝ E] [h : IsRCLike
   · rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @algebraMap_smul (R := ℝ) (A := 𝕜)]
 
 /-- Construct a model with corners over `ℝ` from a continuous partial equiv with convex range. -/
-def of_convex_range
+def ofConvexRange
     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H]
     (φ : PartialEquiv H E) (hsource : φ.source = univ) (htarget : Convex ℝ φ.target)
     (hcont : Continuous φ) (hcont_inv : Continuous φ.symm) (hint : (interior φ.target).Nonempty) :
@@ -331,6 +334,8 @@ def of_convex_range
     have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
     simp [this, hint]
 
+@[deprecated (since := "2025-12-19")] alias of_convex_range := ModelWithCorners.ofConvexRange
+
 theorem convex_range [NormedSpace ℝ E] : Convex ℝ (range I) := by
   by_cases h : IsRCLikeNormedField 𝕜
   · letI : RCLike 𝕜 := h.rclike

Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

@@ -30,7 +30,7 @@ diffeomorphism at every `x ∈ s`, and a **local diffeomorphism** iff it is a lo
 * `IsLocalDiffeomorph.isLocalHomeomorph`: a local diffeomorphism is a local homeomorphism,
   and similarly for a local diffeomorphism on `s`.
 * `IsLocalDiffeomorph.isOpen_range`: the image of a local diffeomorphism is open
-* `IsLocalDiffeomorph.diffeomorph_of_bijective`:
+* `IsLocalDiffeomorph.diffeomorphOfBijective`:
   a bijective local diffeomorphism is a diffeomorphism
 
 * `Diffeomorph.mfderivToContinuousLinearEquiv`: each differential of a `C^n` diffeomorphism
@@ -331,7 +331,7 @@ lemma IsLocalDiffeomorph.image_coe (hf : IsLocalDiffeomorph I J n f) : hf.image.
 -- This argument implies a `LocalDiffeomorphOn f s` for `s` open is a `PartialDiffeomorph`
 
 /-- A bijective local diffeomorphism is a diffeomorphism. -/
-noncomputable def IsLocalDiffeomorph.diffeomorph_of_bijective
+noncomputable def IsLocalDiffeomorph.diffeomorphOfBijective
     (hf : IsLocalDiffeomorph I J n f) (hf' : Function.Bijective f) : Diffeomorph I J M N n := by
   -- Choose a right inverse `g` of `f`.
   choose g hgInverse using (Function.bijective_iff_has_inverse).mp hf'
@@ -359,6 +359,9 @@ noncomputable def IsLocalDiffeomorph.diffeomorph_of_bijective
       have : y = (Φ x) x := ((hgInverse.2 y).congr (hfx hx)).mp rfl
       exact this ▸ (Φ x).map_source hx }
 
+@[deprecated (since := "2025-12-19")]
+alias IsLocalDiffeomorph.diffeomorph_of_bijective := IsLocalDiffeomorph.diffeomorphOfBijective
+
 end Basic
 
 section Differential

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

@@ -164,14 +164,17 @@ lemma toBasisAt_coe (hs : IsLocalFrameOn I F n s u) (hx : x ∈ u) (i : ι) :
 
 /-- If `{sᵢ}` is a local frame on a vector bundle, `F` being finite-dimensional implies the
 indexing set being finite. -/
-def fintype_of_finiteDimensional [VectorBundle 𝕜 F V] [FiniteDimensional 𝕜 F]
+noncomputable def fintypeOfFiniteDimensional [VectorBundle 𝕜 F V] [FiniteDimensional 𝕜 F]
     (hs : IsLocalFrameOn I F n s u) (hx : x ∈ u) : Fintype ι := by
   have : FiniteDimensional 𝕜 (V x) := by
     let phi := (trivializationAt F V x).linearEquivAt 𝕜 x
       (FiberBundle.mem_baseSet_trivializationAt' x)
     exact Finite.equiv phi.symm
   exact FiniteDimensional.fintypeBasisIndex (hs.toBasisAt hx)
 
+@[deprecated (since := "2025-12-19")]
+alias fintype_of_finiteDimensional := fintypeOfFiniteDimensional
+
 open scoped Classical in
 /-- Coefficients of a section `s` of `V` w.r.t. a local frame `{s i}` on `u`.
 Outside of `u`, this returns the junk value 0. -/
@@ -234,7 +237,7 @@ frame at `x` agree. -/
 lemma eq_iff_coeff [VectorBundle 𝕜 F V] [FiniteDimensional 𝕜 F]
     (hs : IsLocalFrameOn I F n s u) (hx : x ∈ u) :
     t x = t' x ↔ ∀ i, hs.coeff i t x = hs.coeff i t' x := by
-  have := fintype_of_finiteDimensional hs hx
+  have := fintypeOfFiniteDimensional hs hx
   exact ⟨fun h i ↦ hs.coeff_congr h i, fun h ↦ by
     simp +contextual [h, hs.coeff_sum_eq t hx, hs.coeff_sum_eq t' hx]⟩
 
@@ -249,7 +252,7 @@ then `t` is `C^n` on `u`. -/
 lemma contMDiffOn_of_coeff [FiniteDimensional 𝕜 F] (h : ∀ i, CMDiff[u] n (hs.coeff i t)) :
     CMDiff[u] n (T% t) := by
   rcases u.eq_empty_or_nonempty with rfl | ⟨x, hx⟩; · simp
-  have := fintype_of_finiteDimensional hs hx
+  have := fintypeOfFiniteDimensional hs hx
   have this (i) : CMDiff[u] n (T% (hs.coeff i t • s i)) :=
     (h i).smul_section (hs.contMDiffOn i)
   have almost : CMDiff[u] n (T% (fun x ↦ ∑ i, (hs.coeff i t) x • s i x)) :=
@@ -262,7 +265,7 @@ lemma contMDiffOn_of_coeff [FiniteDimensional 𝕜 F] (h : ∀ i, CMDiff[u] n (h
 if a section `t` has `C^k` coefficients at `x` w.r.t. `s i`, then `t` is `C^n` at `x`. -/
 lemma contMDiffAt_of_coeff [FiniteDimensional 𝕜 F]
     (h : ∀ i, CMDiffAt n (hs.coeff i t) x) (hu : u ∈ 𝓝 x) : CMDiffAt n (T% t) x := by
-  have := fintype_of_finiteDimensional hs (mem_of_mem_nhds hu)
+  have := fintypeOfFiniteDimensional hs (mem_of_mem_nhds hu)
   have almost : CMDiffAt n (T% (fun x ↦ ∑ i, (hs.coeff i t) x • s i x)) x :=
     .sum_section (fun i _ ↦ (h i).smul_section <| (hs.contMDiffOn i).contMDiffAt hu)
   exact almost.congr_of_eventuallyEq <| (hs.eventually_eq_sum_coeff_smul t hu).mono (by simp)
@@ -271,7 +274,7 @@ lemma contMDiffAt_of_coeff [FiniteDimensional 𝕜 F]
 coefficients at `x ∈ u` w.r.t. `s i`, then `t` is `C^n` at `x`. -/
 lemma contMDiffAt_of_coeff_aux [FiniteDimensional 𝕜 F] (h : ∀ i, CMDiffAt n (hs.coeff i t) x)
     (hu : IsOpen u) (hx : x ∈ u) : CMDiffAt n (T% t) x := by
-  have := fintype_of_finiteDimensional hs hx
+  have := fintypeOfFiniteDimensional hs hx
   exact hs.contMDiffAt_of_coeff h (hu.mem_nhds hx)
 
 section
@@ -283,7 +286,7 @@ w.r.t. `s i`, then `t` is differentiable on `u`. -/
 lemma mdifferentiableOn_of_coeff [FiniteDimensional 𝕜 F] (h : ∀ i, MDiff[u] (hs.coeff i t)) :
     MDiff[u] (T% t) := by
   rcases u.eq_empty_or_nonempty with rfl | ⟨x, hx⟩; · simp
-  have := fintype_of_finiteDimensional hs hx
+  have := fintypeOfFiniteDimensional hs hx
   have this (i) : MDiff[u] (T% (hs.coeff i t • s i)) :=
     (h i).smul_section ((hs.contMDiffOn i).mdifferentiableOn le_rfl)
   have almost : MDiff[u] (T% (fun x ↦ ∑ i, (hs.coeff i t) x • s i x)) :=
@@ -296,7 +299,7 @@ lemma mdifferentiableOn_of_coeff [FiniteDimensional 𝕜 F] (h : ∀ i, MDiff[u]
 coefficients at `x` w.r.t. `s i`, then `t` is differentiable at `x`. -/
 lemma mdifferentiableAt_of_coeff [FiniteDimensional 𝕜 F]
     (h : ∀ i, MDiffAt (hs.coeff i t) x) (hu : u ∈ 𝓝 x) : MDiffAt (T% t) x := by
-  have := fintype_of_finiteDimensional hs (mem_of_mem_nhds hu)
+  have := fintypeOfFiniteDimensional hs (mem_of_mem_nhds hu)
   have almost : MDiffAt (T% (fun x ↦ ∑ i, (hs.coeff i t) x • s i x)) x :=
     .sum_section (fun i ↦ (h i).smul_section <|
       ((hs.contMDiffOn i).mdifferentiableOn le_rfl).mdifferentiableAt hu)

Mathlib/Topology/IsLocalHomeomorph.lean

@@ -250,10 +250,12 @@ theorem isOpenEmbedding_of_injective (hf : IsLocalHomeomorph f) (hi : f.Injectiv
   .of_continuous_injective_isOpenMap hf.continuous hi hf.isOpenMap
 
 /-- A bijective local homeomorphism is a homeomorphism. -/
-noncomputable def toHomeomorph_of_bijective (hf : IsLocalHomeomorph f) (hb : f.Bijective) :
+noncomputable def toHomeomorphOfBijective (hf : IsLocalHomeomorph f) (hb : f.Bijective) :
     X ≃ₜ Y :=
   (Equiv.ofBijective f hb).toHomeomorphOfContinuousOpen hf.continuous hf.isOpenMap
 
+@[deprecated (since := "2025-12-19")] alias toHomeomorph_of_bijective := toHomeomorphOfBijective
+
 /-- Continuous local sections of a local homeomorphism are open embeddings. -/
 theorem isOpenEmbedding_of_comp (hf : IsLocalHomeomorph g) (hgf : IsOpenEmbedding (g ∘ f))
     (cont : Continuous f) : IsOpenEmbedding f :=