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' : ℝ)
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 e_a₁ e_a₂ e_a₃ :
  ∀ (this : C * γ = eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)),
    C * γ = eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
⊢ (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) = (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞)

Tactic:
norm_cast at this ⊢
-- 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)
suffices : (↑C : ℝ) * (↑γ : ℝ) = (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑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:
suffices (C : ℝ) * γ = eLpNormLESNormFDerivOfEqInnerConst μ p by
        rw [eLpNorm_nnreal_eq_lintegral h0p]
        congr
        norm_cast at this ⊢
-- 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)
simp_rw :
  (↑C : ℝ) * (↑(NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯) : ℝ) =
    (↑(eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ) *
          ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 / ((↑(finrank ℝ E) : ℝ) - (↑p : ℝ))).toNNReal) :
      ℝ)
⊢ (↑C : ℝ) * (↑γ : ℝ) = (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ)

Tactic:
simp_rw [eLpNormLESNormFDerivOfEqInnerConst, γ]

Premises used: MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst
-- 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)
refold_let :
  (↑C : ℝ) * (↑(NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯) : ℝ) =
    (↑(C * ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))).toNNReal) : ℝ)
⊢ (↑C : ℝ) * (↑(NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯) : ℝ) =
    (↑(eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ) *
          ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 / ((↑(finrank ℝ E) : ℝ) - (↑p : ℝ))).toNNReal) :
      ℝ)

Tactic:
refold_let n n' C
-- 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)
rw : 0 ≤ (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ)) ∨ (↑C : ℝ) = 0
⊢ (↑C : ℝ) * (↑(NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯) : ℝ) =
    (↑(C * ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))).toNNReal) : ℝ)

Tactic:
rw [NNReal.coe_mul, NNReal.coe_mk, Real.coe_toNNReal', mul_eq_mul_left_iff, eq_comm,
        max_eq_left_iff]

Premises used: Real.coe_toNNReal', mul_eq_mul_left_iff, NNReal.coe_mk, max_eq_left_iff, eq_comm, NNReal.coe_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' : ℝ)
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)
h : 0 ≤ (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
⊢ 0 ≤ (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ)) ∨ (↑C : ℝ) = 0

Tactic:
left
-- 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)
⊢ 0 ≤ (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))

Tactic:
positivity
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
⊢ ContDiff ℝ 1 v

Tactic:
have hv : ContDiff ℝ 1 v := e.contDiff.comp hu
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
⊢ HasCompactSupport v

Tactic:
have h2v : HasCompactSupport v := h2u.comp_left e.map_zero
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ

Tactic:
have := eLpNorm_le_eLpNorm_fderiv_of_eq_inner μ hv h2v hp hn hp'
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
x : E
rw rw₁ :
  norm (E := E →L[ℝ] F') (fderiv ℝ (⇑e : (a : F) → F') (u x) ∘SL fderiv ℝ u x) =
    norm (E := E →L[ℝ] F') (fderiv ℝ (⇑e : (a : F) → F') (u x) ∘SL fderiv ℝ u x)
⊢ norm (E := E →L[ℝ] F') (fderiv ℝ v x) = norm (E := E →L[ℝ] F') (fderiv ℝ (⇑e : (a : F) → F') (u x) ∘SL fderiv ℝ u x)

Tactic:
rw [fderiv_comp x e.differentiableAt (hu.differentiable one_ne_zero x)]

Premises used: ContinuousLinearEquiv.differentiableAt, fderiv_comp, ContDiff.differentiable, one_ne_zero
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
x : E
simp_rw : ‖(↑e : F →L[ℝ] F')‖ * norm (E := E →L[ℝ] F) (fderiv ℝ u x) = (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
simp_rw₁ :
  ‖(↑e : F →L[ℝ] F')‖ * norm (E := E →L[ℝ] F) (fderiv ℝ u x) =
    (↑‖(↑e : F →L[ℝ] F')‖₊ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
⊢ norm (E := F →L[ℝ] F') (fderiv ℝ (⇑e : (a : F) → F') (u x)) * norm (E := E →L[ℝ] F) (fderiv ℝ u x) =
    (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)

Tactic:
simp_rw [e.fderiv, C₂, coe_nnnorm]

Premises used: ContinuousLinearEquiv.fderiv, coe_nnnorm
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
⊢ ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)

Tactic:
have h4v : ∀ x, ‖fderiv ℝ v x‖ ≤ C₂ * ‖fderiv ℝ u x‖ := fun x ↦ calc
    ‖fderiv ℝ v x‖
      = ‖(fderiv ℝ e (u x)).comp (fderiv ℝ u x)‖ := by
      rw [fderiv_comp x e.differentiableAt (hu.differentiable one_ne_zero x)]
    _ ≤ ‖fderiv ℝ e (u x)‖ * ‖fderiv ℝ u x‖ :=
      (fderiv ℝ e (u x)).opNorm_comp_le (fderiv ℝ u x)
    _ = C₂ * ‖fderiv ℝ u x‖ := by simp_rw [e.fderiv, C₂, coe_nnnorm]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
simp_rw :
  eLpNorm u (↑p' : ℝ≥0∞) μ =
    eLpNorm (ε := F) (comp (β := F') (⇑e.symm : (a : F') → F) ((⇑e : (a : F) → F') ∘ u)) (↑p' : ℝ≥0∞) μ
simp_rw₁ :
  eLpNorm u (↑p' : ℝ≥0∞) μ =
    eLpNorm.{u_4, u_3} (ε := F) (fun (x : E) ↦ (e.symm : (a : F') → F) ((e : (a : F) → F') (u x) : F')) (↑p' : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ = eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ

Tactic:
simp_rw [v, Function.comp_def, e.symm_apply_apply]

Premises used: Function.comp_def, ContinuousLinearEquiv.symm_apply_apply