diff --git a/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean b/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean
index 48b9999f0..7449bfe81 100644
--- a/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean
+++ b/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean
@@ -171,7 +171,6 @@ lemma schwartzMap_integrable_slice_symm {d : ℕ} (i : Fin d.succ) (η : 𝓢(Sp
   · fun_prop
   · simp
 
-set_option maxSynthPendingDepth 10000 in
 lemma schwartzMap_fderiv_integrable_slice_symm {d : ℕ} (η : 𝓢(Space d.succ, ℝ)) (x : Space d)
     (i : Fin d.succ) :
     Integrable (fun r => fderiv ℝ (fun x => η (((slice i).symm (r, x)))) x) volume := by
diff --git a/Physlib/SpaceAndTime/Space/Module.lean b/Physlib/SpaceAndTime/Space/Module.lean
index 50117b0ac..9d08b88b5 100644
--- a/Physlib/SpaceAndTime/Space/Module.lean
+++ b/Physlib/SpaceAndTime/Space/Module.lean
@@ -253,6 +253,14 @@ instance {d} : InnerProductSpace ℝ (Space d) where
     simpa only [smul_vadd_zero, inner_vadd_zero, conj_trivial]
       using InnerProductSpace.smul_left v1 v2 a
 
+/-- The normed space structure on `Space d`, registered directly. It is definitionally the
+  one underlying the inner product space structure, but registering it as its own instance is
+  needed for typeclass search to find the operator-norm structure on `Space d →L[ℝ] ℝ`
+  (for example `NormSMulClass ℝ (Space d →L[ℝ] ℝ)`), which is not found when
+  `NormedSpace ℝ (Space d)` arises only as a nested subgoal through
+  `InnerProductSpace.toNormedSpace`. -/
+noncomputable instance {d} : NormedSpace ℝ (Space d) := InnerProductSpace.toNormedSpace
+
 lemma norm_smul_sphere {d : ℕ} (n : ↑(Metric.sphere (0 : Space d) 1))
     {r : ℝ} (hr : 0 ≤ r) :
     ‖(r • (n : Space d))‖ = r := by
diff --git a/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean b/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean
index a0e8f1260..e8e2b0994 100644
--- a/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean
+++ b/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean
@@ -292,7 +292,6 @@ lemma time_integral_differentiable {d : ℕ} (η : 𝓢(Time × Space d, ℝ)) :
 
 -/
 
-set_option maxSynthPendingDepth 10000 in
 @[fun_prop]
 lemma integrable_fderiv_space {d : ℕ} (η : 𝓢(Time × Space d, ℝ)) (x : Space d) :
     Integrable (fun t => fderiv ℝ (fun x => η (t, x)) x) volume := by