awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' : ℝ)
h : ∀ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) = (‖u x‖ₑ ^ ((↑γ : ℝ) - 1)) ^ (↑p : ℝ).conjExponent
bc : AEMeasurable (β := ℝ≥0∞) (fun (x : E) ↦ ‖u x‖ₑ ^ ((↑γ : ℝ) - 1)) μ
bc₁ : AEMeasurable (β := ℝ≥0∞) (fun (x : E) ↦ enorm (E := E →L[ℝ] F') (fderiv ℝ u x)) μ
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ∂μ ≤
    (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))

Tactic:
convert!
          ENNReal.lintegral_mul_le_Lp_mul_Lq μ (.symm <| .conjExponent <| show 1 < (p : ℝ) from hp)
            ?_ ?_ using 5

Premises used: Real.HolderConjugate.symm, ENNReal.lintegral_mul_le_Lp_mul_Lq, Real.HolderConjugate.conjExponent
-- 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' : ℝ)
x : E
⊢ ‖u x‖ₑ ^ (↑p' : ℝ) = (‖u x‖ₑ ^ ((↑γ : ℝ) - 1)) ^ (↑p : ℝ).conjExponent

Tactic:
simp [γ, n, q, ← ENNReal.rpow_mul, ← h3γ]

Premises used: ENNReal.rpow_mul
-- 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' : ℝ)
⊢ let this := borel F';
  BorelSpace F'

Tactic:
borelize F'
-- 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 : MeasurableSpace F' := borel F'
this_1 : BorelSpace F'
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : E) ↦ ‖u x‖ₑ ^ ((↑γ : ℝ) - 1)) μ

Tactic:
fun_prop
-- 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' : ℝ)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : E) ↦ enorm (E := E →L[ℝ] F') (fderiv ℝ u x)) μ

Tactic:
fun_prop
-- 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' : ℝ)
⊢ (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) *
      ((∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q) *
        (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))) =
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ)) *
      (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q)

Tactic:
ring
-- 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' : ℝ)
⊢ (∫⁻ (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)

Tactic:
have :=
  calc (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / (n' : ℝ)) = eLpNorm v n' μ := by
        rw [← h2γ, eLpNorm_nnreal_eq_lintegral hn.symm.pos.ne']
        simp (discharger := positivity) [v, Real.enorm_rpow_of_nonneg, ENNReal.rpow_mul]
    _ ≤ C * eLpNorm (fderiv ℝ v) 1 μ := eLpNorm_le_eLpNorm_fderiv_one μ hv h2v hn
    _ = C * ∫⁻ x, ‖fderiv ℝ v x‖ₑ ∂μ := by rw [eLpNorm_one_eq_lintegral_enorm]
    _ ≤ C * γ * ∫⁻ x, ‖u x‖ₑ ^ ((γ : ℝ) - 1) * ‖fderiv ℝ u x‖ₑ ∂μ := by
      rw [mul_assoc, ← lintegral_const_mul γ]
      · gcongr
        simp_rw [← mul_assoc]
        exact enorm_fderiv_norm_rpow_le (hu.differentiable one_ne_zero) h1γ
      dsimp [enorm]
      fun_prop
    _ ≤ C * γ * ((∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / q) *
        (∫⁻ x, ‖fderiv ℝ u x‖ₑ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ))) := by
        gcongr
        convert!
          ENNReal.lintegral_mul_le_Lp_mul_Lq μ (.symm <| .conjExponent <| show 1 < (p : ℝ) from hp)
            ?_ ?_ using 5
        · simp [γ, n, q, ← ENNReal.rpow_mul, ← h3γ]
        · borelize F'
          fun_prop
        · fun_prop
    _ = C * γ * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) *
      (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / q) := by ring
-- 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 u (↑p' : ℝ≥0∞) μ = (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑p' : ℝ))

Tactic:
eLpNorm_nnreal_eq_lintegral hp'0

Premises used: MeasureTheory.eLpNorm_nnreal_eq_lintegral
-- 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)
rwa :
  (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑n' : ℝ) - 1 / q) ≤
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))
rwa₁ :
  (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑n' : ℝ)) / (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q) ≤
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))
rwa₂ rwa₃ rwa₄ rwa₅ :
  (∫⁻ (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)
⊢ (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑p' : ℝ)) ≤
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))

Tactic:
rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]

Premises used: ENNReal.rpow_sub, ENNReal.div_le_iff
-- 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_1 :
  (∫⁻ (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)
this : (↑C : ℝ) * (↑γ : ℝ) = (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ)
rw :
  (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ)) =
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))
⊢ (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ)) =
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
rw [eLpNorm_nnreal_eq_lintegral h0p]

Premises used: MeasureTheory.eLpNorm_nnreal_eq_lintegral
-- 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_1 :
  (∫⁻ (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)
this : (↑C : ℝ) * (↑γ : ℝ) = (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ)
e_a : (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) = (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞)
⊢ (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ)) =
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))

Tactic:
congr