diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean
index bb922383d08d1..c84328c8ea028 100644
--- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean
+++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean
@@ -382,7 +382,7 @@ theorem stereographic'_target {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphe
 
 /-- The unit sphere in an `n + 1`-dimensional inner product space `E` is a charted space
 modelled on the Euclidean space of dimension `n`. -/
-instance chartedSpace {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
+instance EuclideanSpace.instChartedSpaceSphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
     ChartedSpace (EuclideanSpace ℝ (Fin n)) (sphere (0 : E) 1) where
   atlas := {f | ∃ v : sphere (0 : E) 1, f = stereographic' n v}
   chartAt v := stereographic' n (-v)
@@ -411,7 +411,7 @@ theorem stereographic'_symm_apply {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v :
 
 /-- The unit sphere in an `n + 1`-dimensional inner product space `E` is a smooth manifold,
 modelled on the Euclidean space of dimension `n`. -/
-instance smoothMfldWithCorners {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
+instance EuclideanSpace.instSmoothManifoldWithCornersSphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
     SmoothManifoldWithCorners (𝓡 n) (sphere (0 : E) 1) :=
   smoothManifoldWithCorners_of_contDiffOn (𝓡 n) (sphere (0 : E) 1)
     (by
@@ -443,7 +443,7 @@ instance smoothMfldWithCorners {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
 theorem contMDiff_coe_sphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
     ContMDiff (𝓡 n) 𝓘(ℝ, E) ∞ ((↑) : sphere (0 : E) 1 → E) := by
   -- Porting note: trouble with filling these implicit variables in the instance
-  have := smoothMfldWithCorners (E := E) (n := n)
+  have := EuclideanSpace.instSmoothManifoldWithCornersSphere (E := E) (n := n)
   rw [contMDiff_iff]
   constructor
   · exact continuous_subtype_val
@@ -589,10 +589,10 @@ attribute [local instance] finrank_real_complex_fact'
 /-- The unit circle in `ℂ` is a charted space modelled on `EuclideanSpace ℝ (Fin 1)`.  This
 follows by definition from the corresponding result for `Metric.Sphere`. -/
 instance : ChartedSpace (EuclideanSpace ℝ (Fin 1)) circle :=
-  chartedSpace
+  EuclideanSpace.instChartedSpaceSphere
 
 instance : SmoothManifoldWithCorners (𝓡 1) circle :=
-  smoothMfldWithCorners (E := ℂ)
+  EuclideanSpace.instSmoothManifoldWithCornersSphere (E := ℂ)
 
 /-- The unit circle in `ℂ` is a Lie group. -/
 instance : LieGroup (𝓡 1) circle where
diff --git a/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean b/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean
index d9bef5da10fd8..4bc6b10688607 100644
--- a/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean
+++ b/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean
@@ -71,7 +71,7 @@ structure MulChar extends MonoidHom R R' where
   map_nonunit' : ∀ a : R, ¬IsUnit a → toFun a = 0
 #align mul_char MulChar
 
-instance funLike : FunLike (MulChar R R') R (fun _ => R') :=
+instance MulChar.instFunLike : FunLike (MulChar R R') R (fun _ => R') :=
   ⟨fun χ => χ.toFun,
     fun χ₀ χ₁ h => by cases χ₀; cases χ₁; congr; apply MonoidHom.ext (fun _ => congr_fun h _)⟩
 
diff --git a/docs/overview.yaml b/docs/overview.yaml
index d262da1176d36..bf6a5b7332969 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -408,7 +408,7 @@ Geometry:
     tangent bundle: 'TangentBundle'
     tangent map: 'tangentMap'
     Lie group: 'LieGroup'
-    sphere: 'smoothMfldWithCorners'
+    sphere: 'EuclideanSpace.instSmoothManifoldWithCornersSphere'
 
   Algebraic geometry:
     prime spectrum: 'PrimeSpectrum'