diff --git a/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean b/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean
index c9f1cf7..fe32b1d 100644
--- a/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean
+++ b/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean
@@ -7,82 +7,4 @@ module
 
 public import Mathlib.Analysis.Fourier.FourierTransform
 
-@[expose] public noncomputable section
-
-variable {V W E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
-
-variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V]
-  [NormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W]
-  [FiniteDimensional ℝ W]
-
-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
+/-! Everything this file used to define is now in Mathlib. -/
diff --git a/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean b/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean
index 9477fa6..6a39194 100644
--- a/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean
+++ b/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean
@@ -43,7 +43,10 @@ theorem Lp.fourierTransformZeroAtInftyCLM_toLp_apply (f : 𝓢(V, E)) (x : V) :
       · apply SchwartzMap.denseRange_toLpCLM
         norm_num
       use 1
-      simpa using norm_fourier_toBoundedContinuousFunction_le_toLp_one
+      intro f
+      have e : ‖toZeroAtInftyCLM ℂ V E (𝓕 f)‖ = ‖(𝓕 f).toBoundedContinuousFunction‖ := by
+        rw [← norm_toZeroAtInfty]; rfl
+      simpa [e] using norm_fourier_toBoundedContinuousFunction_le_toLp_one f
     _ = 𝓕 f x := by simp
 
 @[simp]
@@ -54,7 +57,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 [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
@@ -83,7 +86,10 @@ theorem Lp.fourierTransformInvZeroAtInftyCLM_toLp_apply (f : 𝓢(V, E)) (x : V)
       · apply SchwartzMap.denseRange_toLpCLM
         norm_num
       use 1
-      simpa using norm_fourierInv_toBoundedContinuousFunction_le_toLp_one
+      intro f
+      have e : ‖toZeroAtInftyCLM ℂ V E (𝓕⁻ f)‖ = ‖(𝓕⁻ f).toBoundedContinuousFunction‖ := by
+        rw [← norm_toZeroAtInfty]; rfl
+      simpa [e] using 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..3164815 100644
--- a/DirichletProblem/Sobolev/Basic.lean
+++ b/DirichletProblem/Sobolev/Basic.lean
@@ -300,8 +300,9 @@ 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
-      (LineDeriv.laplacianCLM ℂ E 𝓢'(E, F)).map_smul c f.toDistr
+    have h := (LineDeriv.laplacianCLM ℂ E 𝓢'(E, F)).map_smul c f.toDistr
+    simp only [TemperedDistribution.laplacianCLM_apply] at h
+    simpa only [laplacian_toDistr, toDistr_smul, RingHom.id_apply] using h
 
 end Sobolev