fix for leanprover/lean4#11581

kim-em · kim-em · commit 522f58068183 · 2025-12-11T11:56:49.000+11:00
diff --git a/Mathlib/Analysis/Normed/Lp/SmoothApprox.lean b/Mathlib/Analysis/Normed/Lp/SmoothApprox.lean
@@ -19,6 +19,8 @@ functions for `p < ∞`.
 This result is recorded in `MeasureTheory.MemLp.exist_sub_eLpNorm_le`.
 -/
 
+@[expose] public section
+
 variable {α β E F : Type*} [MeasurableSpace E] [NormedAddCommGroup F]
 
 open scoped Nat NNReal ContDiff
