diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean b/Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
index 520a3c06f5342d..a085ad71f5afc5 100644
--- a/Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
+++ b/Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
@@ -5,13 +5,19 @@ Authors: Moritz Doll
 -/
 module
 
-public import Mathlib.Analysis.LocallyConvex.WithSeminorms
+public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
+public import Mathlib.Analysis.Distribution.TemperateGrowth
 public import Mathlib.Analysis.Normed.Group.ZeroAtInfty
-public import Mathlib.Analysis.Normed.Lp.SmoothApprox
 public import Mathlib.Analysis.SpecialFunctions.Pow.Real
-public import Mathlib.Analysis.Distribution.TemperateGrowth
-public import Mathlib.Topology.Algebra.UniformFilterBasis
 public import Mathlib.MeasureTheory.Function.L2Space
+public import Mathlib.Tactic.FunProp
+public import Mathlib.Topology.Algebra.UniformFilterBasis
+
+import Mathlib.Analysis.Calculus.ContDiff.Bounds
+import Mathlib.Analysis.Calculus.ContDiff.Operations
+import Mathlib.Analysis.Normed.Lp.SmoothApprox
+import Mathlib.Tactic.MoveAdd
+
 
 /-!
 # Schwartz space
@@ -230,7 +236,7 @@ variable [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [Nor
 instance instSMul : SMul 𝕜 𝓢(E, F) :=
   ⟨fun c f =>
     { toFun := c • (f : E → F)
-      smooth' := (f.smooth _).const_smul c
+      smooth' := by exact (f.smooth _).const_smul c
       decay' k n := by
         use f.seminormAux k n * ‖c‖
         intro x
@@ -263,13 +269,13 @@ private theorem seminormAux_smul_le (k n : ℕ) (c : 𝕜) (f : 𝓢(E, F)) :
 instance instNSMul : SMul ℕ 𝓢(E, F) :=
   ⟨fun c f =>
     { toFun := c • (f : E → F)
-      smooth' := (f.smooth _).const_smul c
+      smooth' := by exact (f.smooth _).const_smul c
       decay' := by simpa [← Nat.cast_smul_eq_nsmul ℝ] using ((c : ℝ) • f).decay' }⟩
 
 instance instZSMul : SMul ℤ 𝓢(E, F) :=
   ⟨fun c f =>
     { toFun := c • (f : E → F)
-      smooth' := (f.smooth _).const_smul c
+      smooth' := by exact (f.smooth _).const_smul c
       decay' := by simpa [← Int.cast_smul_eq_zsmul ℝ] using ((c : ℝ) • f).decay' }⟩
 
 end SMul
@@ -278,7 +284,7 @@ section Zero
 
 instance instZero : Zero 𝓢(E, F) :=
   ⟨{  toFun := fun _ => 0
-      smooth' := contDiff_const
+      smooth' := by exact contDiff_const
       decay' := fun _ _ => ⟨1, fun _ => by simp⟩ }⟩
 
 instance instInhabited : Inhabited 𝓢(E, F) :=
@@ -305,7 +311,7 @@ section Neg
 
 instance instNeg : Neg 𝓢(E, F) :=
   ⟨fun f =>
-    ⟨-f, (f.smooth _).neg, fun k n => by
+    ⟨-f, by exact (f.smooth _).neg, fun k n => by
       use f.seminormAux k n
       intro x
       grw [f.decay_neg_aux k n x, f.le_seminormAux k n x]⟩⟩
@@ -319,7 +325,7 @@ section Add
 
 instance instAdd : Add 𝓢(E, F) :=
   ⟨fun f g =>
-    ⟨f + g, (f.smooth _).add (g.smooth _), fun k n => by
+    ⟨f + g, by exact (f.smooth _).add (g.smooth _), fun k n => by
       use f.seminormAux k n + g.seminormAux k n
       intro x
       grw [decay_add_le_aux k n f g x, f.le_seminormAux k n x, g.le_seminormAux k n x]⟩⟩
@@ -341,7 +347,7 @@ section Sub
 
 instance instSub : Sub 𝓢(E, F) :=
   ⟨fun f g =>
-    ⟨f - g, (f.smooth _).sub (g.smooth _), by
+    ⟨f - g, by exact (f.smooth _).sub (g.smooth _), by
       intro k n
       refine ⟨f.seminormAux k n + g.seminormAux k n, fun x => ?_⟩
       grw [← f.le_seminormAux k n x, ← g.le_seminormAux k n x]
@@ -681,11 +687,11 @@ variable [NormedSpace 𝕜 E] [NormedSpace 𝕜 G]
 /-- The map `f ↦ (x ↦ B (f x) (g x))` as a continuous `𝕜`-linear map on Schwartz space,
 where `B` is a continuous `𝕜`-linear map and `g` is a function of temperate growth. -/
 def bilinLeftCLM (B : E →L[𝕜] F →L[𝕜] G) {g : D → F} (hg : g.HasTemperateGrowth) :
-    𝓢(D, E) →L[𝕜] 𝓢(D, G) := by
-  refine mkCLM (fun f x => B (f x) (g x))
+    𝓢(D, E) →L[𝕜] 𝓢(D, G) :=
+  mkCLM (fun f x => B (f x) (g x))
     (fun _ _ _ => by simp) (fun _ _ _ => by simp)
     (fun f => (B.bilinearRestrictScalars ℝ).isBoundedBilinearMap.contDiff.comp
-      ((f.smooth ⊤).prodMk hg.1)) ?_
+      ((f.smooth ⊤).prodMk hg.1)) <| by
   rintro ⟨k, n⟩
   rcases hg.norm_iteratedFDeriv_le_uniform n with ⟨l, C, hC, hgrowth⟩
   use
@@ -917,9 +923,9 @@ variable [NormedSpace 𝕜 F]
 /-- Composition with a function on the right is a continuous linear map on Schwartz space
 provided that the function is temperate and growths polynomially near infinity. -/
 def compCLM {g : D → E} (hg : g.HasTemperateGrowth)
-    (hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ x, ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) : 𝓢(E, F) →L[𝕜] 𝓢(D, F) := by
-  refine mkCLM (fun f => f ∘ g) (fun _ _ _ => by simp) (fun _ _ _ => rfl)
-    (fun f => (f.smooth ⊤).comp hg.1) ?_
+    (hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ x, ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) : 𝓢(E, F) →L[𝕜] 𝓢(D, F) :=
+  mkCLM (fun f => f ∘ g) (fun _ _ _ => by simp) (fun _ _ _ => rfl)
+    (fun f => (f.smooth ⊤).comp hg.1) <| by
   rintro ⟨k, n⟩
   rcases hg.norm_iteratedFDeriv_le_uniform n with ⟨l, C, hC, hgrowth⟩
   rcases hg_upper with ⟨kg, Cg, hg_upper'⟩
diff --git a/Mathlib/Analysis/Distribution/TemperateGrowth.lean b/Mathlib/Analysis/Distribution/TemperateGrowth.lean
index 588b7ef54dff03..1697ce5ca93649 100644
--- a/Mathlib/Analysis/Distribution/TemperateGrowth.lean
+++ b/Mathlib/Analysis/Distribution/TemperateGrowth.lean
@@ -5,11 +5,18 @@ Authors: Moritz Doll, Anatole Dedecker, Sébastien Gouëzel
 -/
 module
 
-public import Mathlib.Analysis.Calculus.ContDiff.Bounds
-public import Mathlib.Analysis.SpecialFunctions.JapaneseBracket
-public import Mathlib.Analysis.InnerProductSpace.Calculus
+public import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
+public import Mathlib.Analysis.Calculus.ContDiff.Defs
+public import Mathlib.Analysis.InnerProductSpace.Defs
+public import Mathlib.MeasureTheory.Function.L1Space.Integrable
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
 public import Mathlib.Tactic.MoveAdd
 
+import Mathlib.Analysis.Calculus.ContDiff.Bounds
+import Mathlib.Analysis.InnerProductSpace.Calculus
+import Mathlib.Analysis.SpecialFunctions.JapaneseBracket
+import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
+
 /-! # Functions and measures of temperate growth -/
 
 @[expose] public section
diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
index ec301fdea05376..8b3a6935a071ad 100644
--- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
+++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@@ -5,13 +5,14 @@ Authors: Alex Kontorovich, David Loeffler, Heather Macbeth, Sébastien Gouëzel
 -/
 module
 
-public import Mathlib.Analysis.Calculus.ParametricIntegral
-public import Mathlib.Analysis.Calculus.ContDiff.CPolynomial
+public import Mathlib.Analysis.Calculus.FDeriv.Analytic
 public import Mathlib.Analysis.Fourier.AddCircle
 public import Mathlib.Analysis.Fourier.FourierTransform
-public import Mathlib.Analysis.Calculus.FDeriv.Analytic
-public import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
-public import Mathlib.Analysis.Calculus.ContDiff.Bounds
+
+import Mathlib.Analysis.Calculus.ContDiff.Bounds
+import Mathlib.Analysis.Calculus.ContDiff.CPolynomial
+import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
+import Mathlib.Analysis.Calculus.ParametricIntegral
 
 /-!
 # Derivatives of the Fourier transform
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean b/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
index cf3c8c709aa0a7..44a13b9e764a5d 100644
--- a/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
@@ -10,6 +10,8 @@ public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
 public import Mathlib.Analysis.Calculus.Deriv.Shift
 public import Mathlib.Analysis.SpecificLimits.RCLike
 
+import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+
 /-!
 # Estimates for the complex logarithm
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean
index 996d69a5ee3317..33d46fb89f36b0 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean
@@ -8,6 +8,8 @@ module
 public import Mathlib.Analysis.Meromorphic.Complex
 public import Mathlib.NumberTheory.Harmonic.GammaDeriv
 
+import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+
 /-!
 # The digamma function
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
index 8289d76547c935..37857a5dc55667 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
@@ -5,9 +5,10 @@ Authors: David Loeffler
 -/
 module
 
-public import Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
 public import Mathlib.Analysis.Fourier.PoissonSummation
 
+import Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
+
 /-!
 # Poisson summation applied to the Gaussian
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean
index 96f7c817bb4104..5bfe0f4e1030c1 100644
--- a/Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean
@@ -7,7 +7,8 @@ module
 
 public import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 public import Mathlib.Analysis.SpecialFunctions.NonIntegrable
-public import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
+
+import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
 
 /-!
 # Integrability of Special Functions
diff --git a/Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean b/Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean
index 963b3d3285c928..7b3d0e5781761f 100644
--- a/Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean
@@ -12,6 +12,8 @@ public import Mathlib.Analysis.SpecialFunctions.Log.PosLog
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 public import Mathlib.MeasureTheory.Integral.CircleIntegral
 
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+
 /-!
 # Integrability for Logarithms of Meromorphic Functions
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals/LogTrigonometric.lean b/Mathlib/Analysis/SpecialFunctions/Integrals/LogTrigonometric.lean
index 5a3957a383a4ad..c60ece62981eb6 100644
--- a/Mathlib/Analysis/SpecialFunctions/Integrals/LogTrigonometric.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Integrals/LogTrigonometric.lean
@@ -7,6 +7,9 @@ module
 
 public import Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
 
+import Mathlib.Analysis.Analytic.Order
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+
 /-!
 # Integral of `log ∘ sin`
 
diff --git a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
index 6390825a6ef65a..52a2ab800666ac 100644
--- a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
+++ b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
@@ -5,9 +5,12 @@ Authors: Moritz Doll
 -/
 module
 
-public import Mathlib.Analysis.SpecialFunctions.Integrability.Basic
-public import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
-public import Mathlib.MeasureTheory.Integral.Layercake
+public import Mathlib.MeasureTheory.Function.L1Space.Integrable
+public import Mathlib.MeasureTheory.Measure.Haar.OfBasis
+
+import Mathlib.Analysis.SpecialFunctions.Integrability.Basic
+import Mathlib.MeasureTheory.Integral.Layercake
+import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 
 /-!
 # Japanese Bracket
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
index 2415f5436a99a7..4870807cdd0e94 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
@@ -7,12 +7,13 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Sébasti
 module
 
 public import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
-public import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
 public import Mathlib.Analysis.Calculus.FDeriv.Extend
 public import Mathlib.Analysis.Calculus.Deriv.Prod
 public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 
+import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+
 /-!
 # Derivatives of power function on `ℂ`, `ℝ`, `ℝ≥0`, and `ℝ≥0∞`
 
diff --git a/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean b/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean
index 4036f922576c8c..cd8b3bef764a1d 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean
@@ -5,11 +5,15 @@ Authors: Anatole Dedecker, Yury Kudryashov
 -/
 module
 
+public import Mathlib.Analysis.LocallyConvex.Bounded
+public import Mathlib.Analysis.Normed.Field.Basic
 public import Mathlib.Topology.Algebra.Algebra.Equiv
-public import Mathlib.Topology.Algebra.Module.Equiv
-public import Mathlib.Topology.Algebra.Module.UniformConvergence
-public import Mathlib.Topology.Algebra.SeparationQuotient.Section
 public import Mathlib.Topology.Hom.ContinuousEvalConst
+public import Mathlib.Topology.UniformSpace.UniformConvergenceTopology
+
+import Mathlib.Topology.Algebra.Module.Equiv
+import Mathlib.Topology.Algebra.SeparationQuotient.Section
+import Mathlib.Topology.Algebra.Module.UniformConvergence
 
 /-!
 # Topologies of uniform convergence on the space of continuous linear maps