-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp_1 : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hnp : 0 < (↑n : ℝ) - (↑p : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
h2γ : γ * n' = p'
h3γ : ((↑γ : ℝ) - 1) * q = (↑p' : ℝ)
h4γ : (↑γ : ℝ) ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun (x : E) ↦ ‖u x‖ ^ (↑γ : ℝ)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)
this :
  (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑n' : ℝ)) ≤
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ)) *
      (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q)
eLpNorm :
  (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑p' : ℝ)) ≤
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))
eLpNorm₁ :
  (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ)) =
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
      MeasureTheory.eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ MeasureTheory.eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
      MeasureTheory.eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
calc
    eLpNorm u p' μ
      = (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / (p' : ℝ)) := eLpNorm_nnreal_eq_lintegral hp'0
    _ ≤ C * γ * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) := by
      rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]
    _ = eLpNormLESNormFDerivOfEqInnerConst μ p * eLpNorm (fderiv ℝ u) (↑p) μ := by
      suffices (C : ℝ) * γ = eLpNormLESNormFDerivOfEqInnerConst μ p by
        rw [eLpNorm_nnreal_eq_lintegral h0p]
        congr
        norm_cast at this ⊢
      simp_rw [eLpNormLESNormFDerivOfEqInnerConst, γ]
      refold_let n n' C
      rw [NNReal.coe_mul, NNReal.coe_mk, Real.coe_toNNReal', mul_eq_mul_left_iff, eq_comm,
        max_eq_left_iff]
      left
      positivity

Premises used: Real, ENNReal.ofNNReal, HDiv.hDiv, fderiv, MeasureTheory.eLpNorm_nnreal_eq_lintegral, ENorm.enorm, HPow.hPow, OfNat.ofNat, NNReal.toReal, MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst, MeasureTheory.lintegral, MeasureTheory.eLpNorm