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‖ ^ (↑γ : ℝ)
⊢ ContDiff ℝ 1 v

Tactic:
have hv : ContDiff ℝ 1 v := hu.norm_rpow h1γ
-- 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
⊢ HasCompactSupport v

Tactic:
have h2v : HasCompactSupport v := h2u.norm.rpow_const h4γ
-- 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' : ℝ)
rw : (∫⁻ (x : E), ‖u x‖ₑ ^ (↑(γ * n') : ℝ) ∂μ) ^ (1 / (↑n' : ℝ)) = (∫⁻ (x : E), ‖v x‖ₑ ^ (↑n' : ℝ) ∂μ) ^ (1 / (↑n' : ℝ))
⊢ (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑n' : ℝ)) = eLpNorm v (↑n' : ℝ≥0∞) μ

Tactic:
rw [← h2γ, eLpNorm_nnreal_eq_lintegral hn.symm.pos.ne']

Premises used: NNReal.HolderConjugate.symm, LT.lt.ne', MeasureTheory.eLpNorm_nnreal_eq_lintegral, NNReal.HolderTriple.pos
-- 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‖ₑ ^ (↑(γ * n') : ℝ) ∂μ) ^ (1 / (↑n' : ℝ)) = (∫⁻ (x : E), ‖v x‖ₑ ^ (↑n' : ℝ) ∂μ) ^ (1 / (↑n' : ℝ))

Tactic:
simp (discharger := positivity) [v, Real.enorm_rpow_of_nonneg, ENNReal.rpow_mul]

Premises used: ENNReal.rpow_mul, Real.enorm_rpow_of_nonneg
-- 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' : ℝ)
rw rw₁ :
  (↑C : ℝ≥0∞) * ∫⁻ (x : E), enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ∂μ =
    (↑C : ℝ≥0∞) * ∫⁻ (x : E), enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ∂μ
⊢ (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] ℝ) (fderiv ℝ v) 1 μ =
    (↑C : ℝ≥0∞) * ∫⁻ (x : E), enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ∂μ

Tactic:
rw [eLpNorm_one_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm
-- 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' : ℝ)
rw :
  (↑C : ℝ≥0∞) * ∫⁻ (x : E), enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ∂μ ≤
    (↑C : ℝ≥0∞) * ∫⁻ (a : E), (↑γ : ℝ≥0∞) * (‖u a‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u a)) ∂μ
rw₁ : Measurable (β := ℝ≥0∞) fun (x : E) ↦ ‖u x‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u x)
⊢ (↑C : ℝ≥0∞) * ∫⁻ (x : E), enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ∂μ ≤
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ∂μ

Tactic:
rw [mul_assoc, ← lintegral_const_mul γ]

Premises used: ENNReal.ofNNReal, mul_assoc, MeasureTheory.lintegral_const_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' : ℝ)
bc :
  ∀ (x : E),
    enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ≤
      (↑γ : ℝ≥0∞) * (‖u x‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u x))
⊢ (↑C : ℝ≥0∞) * ∫⁻ (x : E), enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ∂μ ≤
    (↑C : ℝ≥0∞) * ∫⁻ (a : E), (↑γ : ℝ≥0∞) * (‖u a‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u a)) ∂μ

Tactic:
gcongr
-- 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
bc :
  enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ≤ (↑γ : ℝ≥0∞) * ‖u x‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u x)
⊢ enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ≤
    (↑γ : ℝ≥0∞) * (‖u x‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u x))

Tactic:
simp_rw [← mul_assoc]

Premises used: mul_assoc
-- 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
⊢ enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ≤ (↑γ : ℝ≥0∞) * ‖u x‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u x)

Tactic:
enorm_fderiv_norm_rpow_le (hu.differentiable one_ne_zero) h1γ

Premises used: enorm_fderiv_norm_rpow_le, ContDiff.differentiable, one_ne_zero
-- 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
⊢ enorm (E := E →L[ℝ] ℝ) (fderiv ℝ v x) ≤ (↑γ : ℝ≥0∞) * ‖u x‖ₑ ^ ((↑γ : ℝ) - 1) * enorm (E := E →L[ℝ] F') (fderiv ℝ u x)

Tactic:
exact enorm_fderiv_norm_rpow_le (hu.differentiable one_ne_zero) h1γ

Premises used: enorm_fderiv_norm_rpow_le, ContDiff.differentiable, one_ne_zero
-- 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' : ℝ)
funProp : ?m ≤ ?x✝
funProp₁ : MeasurableEmbedding (β := ℝ≥0) fun (x2 : F') ↦ ‖x2‖₊
funProp₂ : inst_2 ≤ inst_2
funProp₃ :
  MeasurableEmbedding (β := ℝ≥0∞ × ℝ≥0∞) fun (x : E) ↦
    ((↑‖u x‖₊ : ℝ≥0∞) ^ ((↑γ : ℝ) - 1), (↑(nnnorm (E := E →L[ℝ] F') (fderiv ℝ u x)) : ℝ≥0∞))
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦
    (↑‖u x‖₊ : ℝ≥0∞) ^ ((↑γ : ℝ) - 1) * (↑(nnnorm (E := E →L[ℝ] F') (fderiv ℝ u x)) : ℝ≥0∞)

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

Tactic:
gcongr
-- 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' : ℝ)
⊢ ∫⁻ (a : E),
      HMul.hMul (α := E → ℝ≥0∞) (β := E → ℝ≥0∞) (fun (x : E) ↦ ‖u x‖ₑ ^ ((↑γ : ℝ) - 1))
        (fun (x : E) ↦ enorm (E := E →L[ℝ] F') (fderiv ℝ u x)) a ∂μ ≤
    (∫⁻ (a : E), (‖u a‖ₑ ^ ((↑γ : ℝ) - 1)) ^ (↑p : ℝ).conjExponent ∂μ) ^ (1 / (↑p : ℝ).conjExponent) *
      (∫⁻ (a : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u a) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))

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

Premises used: Real.HolderConjugate.symm, ENNReal.lintegral_mul_le_Lp_mul_Lq, Real.HolderConjugate.conjExponent