diff --git a/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean b/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean
index c9f1cf7..5a3977f 100644
--- a/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean
+++ b/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean
@@ -20,69 +20,3 @@ variable [FiniteDimensional ℝ V]
 open scoped BoundedContinuousFunction FourierTransform
 
 open MeasureTheory
-
-section CompContinuousCLM
-
-namespace BoundedContinuousFunction
-
-variable {𝕜 α β γ : Type*} [TopologicalSpace α] [SeminormedAddCommGroup β] [TopologicalSpace γ]
-  [NormedField 𝕜] [NormedSpace 𝕜 β]
-
-variable (𝕜) in
-def compContinuousCLM (g : C(γ, α)) : (α →ᵇ β) →L[𝕜] γ →ᵇ β :=
-  LinearMap.mkContinuous
-    { toFun f := f.compContinuous g,
-      map_add' := by intros; ext; simp,
-      map_smul' := by intros; ext; simp }
-    1 (by simpa using norm_compContinuous_le · g)
-
-@[simp]
-theorem compContinuousCLM_apply (f : α →ᵇ β) (g : C(γ, α)) :
-  compContinuousCLM 𝕜 g f = f.compContinuous g := rfl
-
-end BoundedContinuousFunction
-
-end CompContinuousCLM
-
-namespace Real
-
-/-- The Fourier transform from `L1` functions to bounded continuous functions. -/
-def Lp.fourierTransformInv (f : Lp (α := V) E 1) : V →ᵇ E :=
-  (Lp.fourierTransform f).compContinuous (-ContinuousMap.id V)
-
-theorem fourierInv_congr_ae {f₁ f₂ : V → E} (hf : f₁ =ᵐ[volume] f₂) (x : V) :
-    𝓕⁻ f₁ x = 𝓕⁻ f₂ x := by
-  apply integral_congr_ae
-  filter_upwards [hf] with _ hf'
-  rw [hf']
-
-@[simp]
-theorem Lp.fourierTransformInv_apply (f : Lp (α := V) E 1) (x : V) :
-    Lp.fourierTransformInv f x = 𝓕⁻ (f : V → E) x := by
-  simp [Lp.fourierTransformInv, fourierInv_eq_fourier_neg]
-
-@[norm_cast]
-theorem Lp.coe_fourierTransformInv (f : Lp (α := V) E 1) :
-    (Lp.fourierTransformInv f : V → E) = 𝓕⁻ (f : V → E) := by
-  ext x
-  simp
-
-@[simp]
-theorem Lp.fourierTransformInv_toLp {f : V → E} (hf : MemLp f 1) :
-    (Lp.fourierTransformInv hf.toLp : V → E) = 𝓕⁻ f := by
-  simp only [Lp.coe_fourierTransformInv]
-  ext x
-  exact (Real.fourierInv_congr_ae hf.coeFn_toLp) x
-
-variable (V E) in
-/-- The Fourier transform from `L1` functions to bounded continuous functions as a continuous linear
-map. -/
-def Lp.fourierTransformInvCLM : Lp (α := V) E 1 →L[ℂ] V →ᵇ E :=
-  BoundedContinuousFunction.compContinuousCLM ℂ (-ContinuousMap.id V) ∘L Lp.fourierTransformCLM V E
-
-@[simp]
-theorem Lp.fourierTransformInvCLM_apply (f : Lp (α := V) E 1) :
-    Lp.fourierTransformInvCLM V E f = Lp.fourierTransformInv f := by
-  simp [Lp.fourierTransformInvCLM, Lp.fourierTransformInv]
-
-end Real
diff --git a/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean b/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean
index 9477fa6..f07bedd 100644
--- a/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean
+++ b/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean
@@ -42,8 +42,10 @@ theorem Lp.fourierTransformZeroAtInftyCLM_toLp_apply (f : 𝓢(V, E)) (x : V) :
       apply LinearMap.extendOfNorm_eq
       · apply SchwartzMap.denseRange_toLpCLM
         norm_num
-      use 1
-      simpa using norm_fourier_toBoundedContinuousFunction_le_toLp_one
+      refine ⟨1, fun f ↦ ?_⟩
+      show ‖(𝓕 f).toZeroAtInfty‖ ≤ 1 * ‖f.toLp 1 volume‖
+      rw [SchwartzMap.norm_toZeroAtInfty, one_mul]
+      exact norm_fourier_toBoundedContinuousFunction_le_toLp_one f
     _ = 𝓕 f x := by simp
 
 @[simp]
@@ -54,7 +56,7 @@ theorem Lp.fourierTransformZeroAtInftyCLM_toBCF (f : Lp (α := V) E 1) :
     (isClosed_eq (by fun_prop) (Real.Lp.fourierTransformCLM V E).cont)
   intro f
   ext x
-  simpa using Real.fourier_congr_ae (coeFn_toLp f 1 volume).symm x
+  simpa [SchwartzMap.fourier_coe] using Real.fourier_congr_ae (coeFn_toLp f 1 volume).symm x
 
 theorem Lp.fourierTransformZeroAtInftyCLM_apply_apply (f : Lp (α := V) E 1) (x : V) :
     Lp.fourierTransformZeroAtInftyCLM V E f x = 𝓕 (f : V → E) x := by
@@ -82,8 +84,10 @@ theorem Lp.fourierTransformInvZeroAtInftyCLM_toLp_apply (f : 𝓢(V, E)) (x : V)
       apply LinearMap.extendOfNorm_eq
       · apply SchwartzMap.denseRange_toLpCLM
         norm_num
-      use 1
-      simpa using norm_fourierInv_toBoundedContinuousFunction_le_toLp_one
+      refine ⟨1, fun f ↦ ?_⟩
+      show ‖(𝓕⁻ f).toZeroAtInfty‖ ≤ 1 * ‖f.toLp 1 volume‖
+      rw [SchwartzMap.norm_toZeroAtInfty, one_mul]
+      exact norm_fourierInv_toBoundedContinuousFunction_le_toLp_one f
     _ = 𝓕⁻ f x := by simp
 
 @[simp]
diff --git a/DirichletProblem/Sobolev/Basic.lean b/DirichletProblem/Sobolev/Basic.lean
index 2386c61..4ab2663 100644
--- a/DirichletProblem/Sobolev/Basic.lean
+++ b/DirichletProblem/Sobolev/Basic.lean
@@ -300,7 +300,7 @@ def laplacianₗ {s : ℝ} : Sobolev E F s 2 →ₗ[ℂ] Sobolev E F (s - 2) 2 w
     simpa using (LineDeriv.laplacianCLM ℂ E 𝓢'(E, F)).map_add f.toDistr g.toDistr
   map_smul' c f := by
     ext1
-    simpa only [laplacian_toDistr, laplacianCLM_apply] using
+    simpa only [laplacian_toDistr, laplacianCLM_apply, toDistr_smul, RingHom.id_apply] using
       (LineDeriv.laplacianCLM ℂ E 𝓢'(E, F)).map_smul c f.toDistr
 
 end Sobolev