fix

leanprover-community · Oct 19, 2024 · 53b3b7b · 53b3b7b
1 parent 8c84091
commit 53b3b7b
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean b/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
@@ -537,8 +537,7 @@ theorem eLpNorm_le_eLpNorm_fderiv_of_eq_inner  {u : E → F'}
   have h4u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ ≠ ∞ := by
     refine lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top (NNReal.coe_pos_iff_ne_zero.mpr h0p') ?_
       |>.ne
-    dsimp only
-    rw [NNReal.val_eq_coe, ← eLpNorm_nnreal_eq_eLpNorm' h0p']
+    rw [← eLpNorm_nnreal_eq_eLpNorm' h0p']
     exact hu.continuous.memℒp_of_hasCompactSupport (μ := μ) h2u |>.eLpNorm_lt_top
   have h5u : (∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ) ^ (1 / q) ≠ 0 :=
     ENNReal.rpow_pos (pos_iff_ne_zero.mpr h3u) h4u |>.ne'