[Merged by Bors] - chore: tidy various files

Mathlib/Algebra/Category/AlgebraCat/Limits.lean

@@ -44,7 +44,7 @@ instance algebraObj (F : J ⥤ AlgebraCatMax.{v, w} R) (j) :
   inferInstanceAs <| Algebra R (F.obj j)
 #align Algebra.algebra_obj AlgebraCat.algebraObj
 
-/-- The flat sections of a functor into `Algebra R` form a submodule of all sections.
+/-- The flat sections of a functor into `AlgebraCat R` form a submodule of all sections.
 -/
 def sectionsSubalgebra (F : J ⥤ AlgebraCatMax.{v, w} R) : Subalgebra R (∀ j, F.obj j) :=
   { SemiRingCat.sectionsSubsemiring
@@ -62,7 +62,7 @@ instance limitAlgebra (F : J ⥤ AlgebraCatMax.{v, w} R) :
   inferInstanceAs <| Algebra R (sectionsSubalgebra F)
 #align Algebra.limit_algebra AlgebraCat.limitAlgebra
 
-/-- `limit.π (F ⋙ forget (Algebra R)) j` as a `alg_hom`. -/
+/-- `limit.π (F ⋙ forget (AlgebraCat R)) j` as a `AlgHom`. -/
 def limitπAlgHom (F : J ⥤ AlgebraCatMax.{v, w} R) (j) :
     (Types.limitCone (F ⋙ forget (AlgebraCat R))).pt →ₐ[R]
       (F ⋙ forget (AlgebraCatMax.{v, w} R)).obj j :=
@@ -73,10 +73,10 @@ def limitπAlgHom (F : J ⥤ AlgebraCatMax.{v, w} R) (j) :
 
 namespace HasLimits
 
--- The next two definitions are used in the construction of `has_limits (Algebra R)`.
+-- The next two definitions are used in the construction of `HasLimits (AlgebraCat R)`.
 -- After that, the limits should be constructed using the generic limits API,
--- e.g. `limit F`, `limit.cone F`, and `limit.is_limit F`.
-/-- Construction of a limit cone in `Algebra R`.
+-- e.g. `limit F`, `limit.cone F`, and `limit.isLimit F`.
+/-- Construction of a limit cone in `AlgebraCat R`.
 (Internal use only; use the limits API.)
 -/
 def limitCone (F : J ⥤ AlgebraCatMax.{v, w} R) : Cone F where
@@ -87,7 +87,7 @@ def limitCone (F : J ⥤ AlgebraCatMax.{v, w} R) : Cone F where
         AlgHom.coe_fn_injective ((Types.limitCone (F ⋙ forget _)).π.naturality f) }
 #align Algebra.has_limits.limit_cone AlgebraCat.HasLimits.limitCone
 
-/-- Witness that the limit cone in `Algebra R` is a limit cone.
+/-- Witness that the limit cone in `AlgebraCat R` is a limit cone.
 (Internal use only; use the limits API.)
 -/
 def limitConeIsLimit (F : J ⥤ AlgebraCatMax.{v, w} R) : IsLimit (limitCone.{v, w} F) := by

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -412,21 +412,23 @@ theorem carrier.add_mem (q : Spec.T A⁰_ f) {a b : A} (ha : a ∈ carrier f_deg
   let g : ℕ → A⁰_ f := fun j => (m + m).choose j •
       if h2 : m + m < j then (0 : A⁰_ f)
       else
+        -- Porting note: inlining `l`, `r` causes a "can't synth HMul A⁰_ f A⁰_ f ?" error
         if h1 : j ≤ m then
-          -- Porting note : cannot use * notation since can't synth HMul A⁰_ f A⁰_ f ?
-          Mul.mul (Quotient.mk''
-              ⟨m * i, ⟨proj 𝒜 i a ^ j * proj 𝒜 i b ^ (m - j), ?_⟩,
-                ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
-            (Quotient.mk''
-              ⟨m * i, ⟨proj 𝒜 i b ^ m, by mem_tac⟩,
-                ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
+          letI l : A⁰_ f := Quotient.mk''
+            ⟨m * i, ⟨proj 𝒜 i a ^ j * proj 𝒜 i b ^ (m - j), ?_⟩,
+              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩
+          letI r : A⁰_ f := Quotient.mk''
+            ⟨m * i, ⟨proj 𝒜 i b ^ m, by mem_tac⟩,
+              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩
+          l * r
         else
-          Mul.mul (Quotient.mk''
-              ⟨m * i, ⟨proj 𝒜 i a ^ m, by mem_tac⟩,
-                ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
-            (Quotient.mk''
-              ⟨m * i, ⟨proj 𝒜 i a ^ (j - m) * proj 𝒜 i b ^ (m + m - j), ?_⟩,
-                ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
+          letI l : A⁰_ f := Quotient.mk''
+            ⟨m * i, ⟨proj 𝒜 i a ^ m, by mem_tac⟩,
+              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩
+          letI r : A⁰_ f := Quotient.mk''
+            ⟨m * i, ⟨proj 𝒜 i a ^ (j - m) * proj 𝒜 i b ^ (m + m - j), ?_⟩,
+              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩
+          l * r
   rotate_left
   · rw [(_ : m * i = _)]
     -- Porting note: it seems unification with mul_mem is more fiddly reducing value of mem_tac

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -40,7 +40,6 @@ attribute [-instance] Matrix.SpecialLinearGroup.instCoeFun
 attribute [-instance] Matrix.GeneralLinearGroup.instCoeFun
 
 local notation "GL(" n ", " R ")" "⁺" => Matrix.GLPos (Fin n) R
--- TODO: these don't seem to work yet
 local notation:1024 "↑ₘ" A:1024 =>
   (((A : GL(2, ℝ)⁺) : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) _)
 local notation:1024 "↑ₘ[" R "]" A:1024 =>
@@ -88,7 +87,7 @@ def re (z : ℍ) :=
 theorem ext' {a b : ℍ} (hre : a.re = b.re) (him : a.im = b.im) : a = b :=
   ext <| Complex.ext hre him
 
-/-- Constructor for `upper_half_plane`. It is useful if `⟨z, h⟩` makes Lean use a wrong
+/-- Constructor for `UpperHalfPlane`. It is useful if `⟨z, h⟩` makes Lean use a wrong
 typeclass instance. -/
 def mk (z : ℂ) (h : 0 < z.im) : ℍ :=
   ⟨z, h⟩
@@ -293,12 +292,12 @@ theorem subgroup_on_glpos_smul_apply (s : Γ) (g : GL(2, ℝ)⁺) (z : ℍ) :
   rfl
 #align upper_half_plane.subgroup_on_GL_pos_smul_apply UpperHalfPlane.subgroup_on_glpos_smul_apply
 
-instance subgroup_on_gLPos : IsScalarTower Γ GL(2, ℝ)⁺ ℍ where
+instance subgroup_on_glpos : IsScalarTower Γ GL(2, ℝ)⁺ ℍ where
   smul_assoc := by
     intro s g z
     simp only [subgroup_on_glpos_smul_apply]
     apply mul_smul'
-#align upper_half_plane.subgroup_on_GL_pos UpperHalfPlane.subgroup_on_gLPos
+#align upper_half_plane.subgroup_on_GL_pos UpperHalfPlane.subgroup_on_glpos
 
 instance subgroupSL : SMul Γ SL(2, ℤ) :=
   ⟨fun s g => s * g⟩

Mathlib/Analysis/Convex/Combination.lean

@@ -431,7 +431,7 @@ theorem convexHull_add (s t : Set E) : convexHull R (s + t) = convexHull R s + c
 variable (R E)
 
 -- porting note: needs `noncomputable` due to `OrderHom.toFun`!?
-/-- `convex_hull` is an additive monoid morphism under pointwise addition. -/
+/-- `convexHull` is an additive monoid morphism under pointwise addition. -/
 @[simps]
 noncomputable def convexHullAddMonoidHom : Set E →+ Set E where
   toFun := convexHull R

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -40,6 +40,7 @@ adjoint
 
 -/
 
+local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
 
 noncomputable section
 
@@ -142,9 +143,8 @@ theorem adjoint_comp (A : F →L[𝕜] G) (B : E →L[𝕜] F) : (A ∘L B)† =
   simp only [adjoint_inner_right, ContinuousLinearMap.coe_comp', Function.comp_apply]
 #align continuous_linear_map.adjoint_comp ContinuousLinearMap.adjoint_comp
 
--- Porting note: Originally `‖A x‖ ^ 2`. But this didn't work because the exponent was `2 : ℝ`.
 theorem apply_norm_sq_eq_inner_adjoint_left (A : E →L[𝕜] E) (x : E) :
-    HPow.hPow ‖A x‖ 2 = re ⟪(A† * A) x, x⟫ := by
+    ‖A x‖ ^ 2 = re ⟪(A† * A) x, x⟫ := by
   have h : ⟪(A† * A) x, x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_left]; rfl
   rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
 #align continuous_linear_map.apply_norm_sq_eq_inner_adjoint_left ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left
@@ -154,9 +154,8 @@ theorem apply_norm_eq_sqrt_inner_adjoint_left (A : E →L[𝕜] E) (x : E) :
   rw [← apply_norm_sq_eq_inner_adjoint_left, Real.sqrt_sq (norm_nonneg _)]
 #align continuous_linear_map.apply_norm_eq_sqrt_inner_adjoint_left ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left
 
--- Porting note: Originally `‖A x‖ ^ 2`. But this didn't work because the exponent was `2 : ℝ`.
 theorem apply_norm_sq_eq_inner_adjoint_right (A : E →L[𝕜] E) (x : E) :
-    HPow.hPow ‖A x‖ 2 = re ⟪x, (A† * A) x⟫ := by
+    ‖A x‖ ^ 2 = re ⟪x, (A† * A) x⟫ := by
   have h : ⟪x, (A† * A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]; rfl
   rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
 #align continuous_linear_map.apply_norm_sq_eq_inner_adjoint_right ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right

Mathlib/Analysis/InnerProductSpace/OfNorm.lean

@@ -30,7 +30,7 @@ and use the parallelogram identity
 
 $$‖x + y‖^2 + ‖x - y‖^2 = 2 (‖x‖^2 + ‖y‖^2)$$
 
-to prove it is an inner product, i.e., that it is conjugate-symmetric (`Inner_.conj_symm`) and
+to prove it is an inner product, i.e., that it is conjugate-symmetric (`inner_.conj_symm`) and
 linear in the first argument. `add_left` is proved by judicious application of the parallelogram
 identity followed by tedious arithmetic. `smul_left` is proved step by step, first noting that
 $\langle λ x, y \rangle = λ \langle x, y \rangle$ for $λ ∈ ℕ$, $λ = -1$, hence $λ ∈ ℤ$ and $λ ∈ ℚ$
@@ -124,7 +124,7 @@ theorem _root_.Continuous.inner_ {f g : ℝ → E} (hf : Continuous f) (hg : Con
   continuity
 #align inner_product_spaceable.continuous.inner_ Continuous.inner_
 
-theorem Inner_.norm_sq (x : E) : ‖x‖ ^ 2 = re (inner_ 𝕜 x x) := by
+theorem inner_.norm_sq (x : E) : ‖x‖ ^ 2 = re (inner_ 𝕜 x x) := by
   simp only [inner_]
   have h₁ : IsROrC.normSq (4 : 𝕜) = 16 := by
     have : ((4 : ℝ) : 𝕜) = (4 : 𝕜) := by norm_cast
@@ -134,9 +134,9 @@ theorem Inner_.norm_sq (x : E) : ‖x‖ ^ 2 = re (inner_ 𝕜 x x) := by
   simp only [h₁, h₂, algebraMap_eq_ofReal, sub_self, norm_zero, mul_re, inv_re, ofNat_re, map_sub,
     map_add, ofReal_re, ofNat_im, ofReal_im, mul_im, I_re, inv_im]
   ring
-#align inner_product_spaceable.inner_.norm_sq InnerProductSpaceable.Inner_.norm_sq
+#align inner_product_spaceable.inner_.norm_sq InnerProductSpaceable.inner_.norm_sq
 
-theorem Inner_.conj_symm (x y : E) : conj (inner_ 𝕜 y x) = inner_ 𝕜 x y := by
+theorem inner_.conj_symm (x y : E) : conj (inner_ 𝕜 y x) = inner_ 𝕜 x y := by
   simp only [inner_]
   have h4 : conj (4⁻¹ : 𝕜) = 4⁻¹ := by norm_num
   rw [map_mul, h4]
@@ -159,7 +159,7 @@ theorem Inner_.conj_symm (x y : E) : conj (inner_ 𝕜 y x) = inner_ 𝕜 x y :=
     · rw [smul_add, smul_smul, I_mul_I_of_nonzero hI, neg_one_smul, ← neg_add_eq_sub]
   rw [h₁, h₂, ← sub_add_eq_add_sub]
   simp only [neg_mul, sub_eq_add_neg, neg_neg]
-#align inner_product_spaceable.inner_.conj_symm InnerProductSpaceable.Inner_.conj_symm
+#align inner_product_spaceable.inner_.conj_symm InnerProductSpaceable.inner_.conj_symm
 
 variable [InnerProductSpaceable E]
 
@@ -320,8 +320,8 @@ noncomputable def InnerProductSpace.ofNorm
     InnerProductSpace 𝕜 E :=
   haveI : InnerProductSpaceable E := ⟨h⟩
   { inner := inner_ 𝕜
-    norm_sq_eq_inner := Inner_.norm_sq
-    conj_symm := Inner_.conj_symm
+    norm_sq_eq_inner := inner_.norm_sq
+    conj_symm := inner_.conj_symm
     add_left := InnerProductSpaceable.add_left
     smul_left := fun _ _ _ => innerProp _ _ _ }
 #align inner_product_space.of_norm InnerProductSpace.ofNorm
@@ -336,8 +336,8 @@ parallelogram identity can be given a compatible inner product. Do
 `InnerProductSpace 𝕜 E`. -/
 theorem nonempty_innerProductSpace : Nonempty (InnerProductSpace 𝕜 E) :=
   ⟨{  inner := inner_ 𝕜
-      norm_sq_eq_inner := Inner_.norm_sq
-      conj_symm := Inner_.conj_symm
+      norm_sq_eq_inner := inner_.norm_sq
+      conj_symm := inner_.conj_symm
       add_left := add_left
       smul_left := fun _ _ _ => innerProp _ _ _ }⟩
 #align nonempty_inner_product_space nonempty_innerProductSpace

Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean

@@ -13,6 +13,7 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Log
 We construct the power functions `x ^ y`, where `x` and `y` are complex numbers.
 -/
 
+local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y) -- Porting note: See issue #2220
 
 open Classical Real Topology Filter ComplexConjugate Finset Set
 
@@ -55,7 +56,7 @@ theorem cpow_eq_zero_iff (x y : ℂ) : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0 := by
 theorem zero_cpow {x : ℂ} (h : x ≠ 0) : (0 : ℂ) ^ x = 0 := by simp [cpow_def, *]
 #align complex.zero_cpow Complex.zero_cpow
 
-theorem zero_cpow_eq_iff {x : ℂ} {a : ℂ} : 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 := by
+theorem zero_cpow_eq_iff {x : ℂ} {a : ℂ} : (0 : ℂ) ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 := by
   constructor
   · intro hyp
     simp only [cpow_def, eq_self_iff_true, if_true] at hyp
@@ -72,7 +73,7 @@ theorem zero_cpow_eq_iff {x : ℂ} {a : ℂ} : 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 
     · exact cpow_zero _
 #align complex.zero_cpow_eq_iff Complex.zero_cpow_eq_iff
 
-theorem eq_zero_cpow_iff {x : ℂ} {a : ℂ} : a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 := by
+theorem eq_zero_cpow_iff {x : ℂ} {a : ℂ} : a = (0 : ℂ) ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 := by
   rw [← zero_cpow_eq_iff, eq_comm]
 #align complex.eq_zero_cpow_iff Complex.eq_zero_cpow_iff
 
@@ -111,9 +112,8 @@ theorem cpow_sub {x : ℂ} (y z : ℂ) (hx : x ≠ 0) : x ^ (y - z) = x ^ y / x
 theorem cpow_neg_one (x : ℂ) : x ^ (-1 : ℂ) = x⁻¹ := by simpa using cpow_neg x 1
 #align complex.cpow_neg_one Complex.cpow_neg_one
 
--- Porting note: couldn't find a way to use `^` for the RHS
 @[simp, norm_cast]
-theorem cpow_nat_cast (x : ℂ) : ∀ n : ℕ, x ^ (n : ℂ) = HPow.hPow x (n : ℕ)
+theorem cpow_nat_cast (x : ℂ) : ∀ n : ℕ, x ^ (n : ℂ) = x ^ n
   | 0 => by simp
   | n + 1 =>
     if hx : x = 0 then by
@@ -123,22 +123,22 @@ theorem cpow_nat_cast (x : ℂ) : ∀ n : ℕ, x ^ (n : ℂ) = HPow.hPow x (n :
 #align complex.cpow_nat_cast Complex.cpow_nat_cast
 
 @[simp]
-theorem cpow_two (x : ℂ) : x ^ (2 : ℂ) = HPow.hPow x (2 : ℕ) := by
+theorem cpow_two (x : ℂ) : x ^ (2 : ℂ) = x ^ (2 : ℕ) := by
   rw [← cpow_nat_cast]
   simp only [Nat.cast_ofNat]
 #align complex.cpow_two Complex.cpow_two
 
 open Int in
 @[simp, norm_cast]
-theorem cpow_int_cast (x : ℂ) : ∀ n : ℤ, x ^ (n : ℂ) = HPow.hPow x n
+theorem cpow_int_cast (x : ℂ) : ∀ n : ℤ, x ^ (n : ℂ) = x ^ n
   | (n : ℕ) => by simp
   | -[n+1] => by
     rw [zpow_negSucc]
     simp only [Int.negSucc_coe, Int.cast_neg, Complex.cpow_neg, inv_eq_one_div, Int.cast_ofNat,
       cpow_nat_cast]
 #align complex.cpow_int_cast Complex.cpow_int_cast
 
-theorem cpow_nat_inv_pow (x : ℂ) {n : ℕ} (hn : n ≠ 0) : HPow.hPow (x ^ (n⁻¹ : ℂ)) n = x := by
+theorem cpow_nat_inv_pow (x : ℂ) {n : ℕ} (hn : n ≠ 0) : (x ^ (n⁻¹ : ℂ)) ^ n = x := by
   suffices im (log x * (n⁻¹ : ℂ)) ∈ Ioc (-π) π by
     rw [← cpow_nat_cast, ← cpow_mul _ this.1 this.2, inv_mul_cancel, cpow_one]
     exact_mod_cast hn

Mathlib/Data/ZMod/Defs.lean

@@ -70,7 +70,7 @@ instance instDistrib (n : ℕ) : Distrib (Fin n) :=
       rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm] }
 #align fin.distrib Fin.instDistrib
 
-/-- Commutative ring structure on `fin n`. -/
+/-- Commutative ring structure on `Fin n`. -/
 instance instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n) :=
   { Fin.instAddMonoidWithOne n, Fin.addCommGroup n, Fin.instCommSemigroup n, Fin.instDistrib n with
     one_mul := Fin.one_mul'
@@ -81,7 +81,7 @@ instance instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n) :=
     mul_zero := Fin.mul_zero' }
 #align fin.comm_ring Fin.instCommRing
 
-/-- Note this is more general than `fin.comm_ring` as it applies (vacuously) to `fin 0` too. -/
+/-- Note this is more general than `Fin.instCommRing` as it applies (vacuously) to `Fin 0` too. -/
 instance instHasDistribNeg (n : ℕ) : HasDistribNeg (Fin n) :=
   { toInvolutiveNeg := Fin.instInvolutiveNeg n
     mul_neg := Nat.casesOn n finZeroElim fun _i => mul_neg

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

@@ -241,7 +241,7 @@ end SmoothPartitionOfUnity
 
 namespace BumpCovering
 
--- Repeat variables to drop [finite_dimensional ℝ E] and [smooth_manifold_with_corners I M]
+-- Repeat variables to drop `[FiniteDimensional ℝ E]` and `[SmoothManifoldWithCorners I M]`
 theorem smooth_toPartitionOfUnity {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
     {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM}
     [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : BumpCovering ι M s)
@@ -503,7 +503,8 @@ theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (h
   haveI : LocallyCompactSpace H := I.locally_compact
   haveI : LocallyCompactSpace M := ChartedSpace.locallyCompact H M
   haveI : NormalSpace M := normal_of_paracompact_t2
-  -- porting note: split `rcases` into `have` + `rcases`
+  -- porting note(https://github.com/leanprover/std4/issues/116):
+  -- split `rcases` into `have` + `rcases`
   have := BumpCovering.exists_isSubordinate_of_prop (Smooth I 𝓘(ℝ)) ?_ hs U ho hU
   · rcases this with ⟨f, hf, hfU⟩
     exact ⟨f.toSmoothPartitionOfUnity hf, hfU.toSmoothPartitionOfUnity hf⟩
@@ -522,7 +523,7 @@ be a family of convex sets. Suppose that for each point `x : M` there exists a n
 `y ∈ U`. Then there exists a $C^n$ smooth function `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x`
 for all `x`. See also `exists_smooth_forall_mem_convex_of_local` and
 `exists_smooth_forall_mem_convex_of_local_const`. -/
-theorem exists_cont_mdiff_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x))
+theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x))
     (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) :
     ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := by
   choose U hU g hgs hgt using Hloc
@@ -533,25 +534,25 @@ theorem exists_cont_mdiff_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t
       hf.contMDiff_finsum_smul (fun i => isOpen_interior) fun i => (hgs i).mono interior_subset⟩,
     fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ _) (ht _)⟩
   exact interior_subset (hf _ <| subset_closure hi)
-#align exists_cont_mdiff_forall_mem_convex_of_local exists_cont_mdiff_forall_mem_convex_of_local
+#align exists_cont_mdiff_forall_mem_convex_of_local exists_contMDiffOn_forall_mem_convex_of_local
 
 /-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F`
 be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood
 `U ∈ 𝓝 x` and a function `g : M → F` such that `g` is smooth on `U` and `g y ∈ t y` for all `y ∈ U`.
 Then there exists a smooth function `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`.
-See also `exists_cont_mdiff_forall_mem_convex_of_local` and
+See also `exists_contMDiffOn_forall_mem_convex_of_local` and
 `exists_smooth_forall_mem_convex_of_local_const`. -/
 theorem exists_smooth_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x))
     (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, SmoothOn I 𝓘(ℝ, F) g U ∧ ∀ y ∈ U, g y ∈ t y) :
     ∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=
-  exists_cont_mdiff_forall_mem_convex_of_local I ht Hloc
+  exists_contMDiffOn_forall_mem_convex_of_local I ht Hloc
 #align exists_smooth_forall_mem_convex_of_local exists_smooth_forall_mem_convex_of_local
 
 /-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` be
 a family of convex sets. Suppose that for each point `x : M` there exists a vector `c : F` such that
 for all `y` in a neighborhood of `x` we have `c ∈ t y`. Then there exists a smooth function
 `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`.  See also
-`exists_cont_mdiff_forall_mem_convex_of_local` and `exists_smooth_forall_mem_convex_of_local`. -/
+`exists_contMDiffOn_forall_mem_convex_of_local` and `exists_smooth_forall_mem_convex_of_local`. -/
 theorem exists_smooth_forall_mem_convex_of_local_const (ht : ∀ x, Convex ℝ (t x))
     (Hloc : ∀ x : M, ∃ c : F, ∀ᶠ y in 𝓝 x, c ∈ t y) : ∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=
   exists_smooth_forall_mem_convex_of_local I ht fun x =>