awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
hf : Measurable (β := ℝ≥0∞) fun (y : ι → ℝ) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))
⊢ (∫⁻ (y : ι → ℝ),
        enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ) ^
      p =
    (‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ *
        ∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^
      p

Tactic:
rw [lintegral_mul_const, mul_comm]

Premises used: MeasureTheory.lintegral_mul_const, mul_comm
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x11 : E) ↦ fderiv ℝ u x11) ?μ
funProp₁ : inst_4 ≤ inst_4
funProp₂ : MeasurableEmbedding (β := E →L[ℝ] F) fun (y11 : E) ↦ fderiv ℝ u y11
funProp₃ :
  LE.le (α := MeasurableSpace (ι → ℝ)) (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) MeasureSpace.toMeasurableSpace
funProp₄ : MeasurableEmbedding.{0, u_4} (β := E) fun (y : ι → ℝ) ↦ (e.symm : (a : ι → ℝ) → E) y
⊢ Measurable (β := ℝ≥0∞) fun (y : ι → ℝ) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))

Tactic:
fun_prop
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
rw :
  ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ ^ p *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
rw₁ :
  (↑‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ : ℝ≥0∞) ^ p *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
rw₂ rw₃ :
  (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
⊢ (‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ *
        ∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^
      p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p

Tactic:
rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, enorm_eq_nnnorm, ← ENNReal.coe_rpow_of_nonneg _ h0p]

Premises used: ENNReal.mul_rpow_of_nonneg, ENNReal.coe_rpow_of_nonneg, enorm_eq_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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
e_a :
  ∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) =
    ∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume
⊢ (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p

Tactic:
congr
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
rw : Measurable (β := ℝ≥0∞) fun (x : E) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u x)
⊢ ∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) =
    ∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume

Tactic:
rw [lintegral_map _ e.symm.continuous.measurable]

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.continuous, Continuous.measurable, MeasureTheory.lintegral_map
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x : E) ↦ fderiv ℝ u x) ?μ
funProp₁ : inst_4 ≤ inst_4
funProp₂ : MeasurableEmbedding (β := E →L[ℝ] F) fun (x : E) ↦ fderiv ℝ u x
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u x)

Tactic:
fun_prop
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p

Tactic:
have :=
  calc ∫⁻ x, ‖u x‖ₑ ^ p ∂(volume : Measure (ι → ℝ)).map e.symm
      = ∫⁻ y, ‖v y‖ₑ ^ p := by
        refine lintegral_map ?_ e.symm.continuous.measurable
        borelize F
        exact hu.continuous.measurable.nnnorm.coe_nnreal_ennreal.pow_const _
    _ ≤ (∫⁻ y, ‖fderiv ℝ v y‖ₑ) ^ p := lintegral_pow_le_pow_lintegral_fderiv_aux hp hv h2v
    _ = (∫⁻ y, ‖(fderiv ℝ u (e.symm y)).comp (fderiv ℝ e.symm y)‖ₑ) ^ p := by
        congr! with y
        apply fderiv_comp _ (hu.differentiable one_ne_zero _)
        exact e.symm.differentiableAt
    _ ≤ (∫⁻ y, ‖fderiv ℝ u (e.symm y)‖ₑ * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ) ^ p := by
        gcongr with y
        rw [e.symm.fderiv]
        apply ContinuousLinearMap.opENorm_comp_le
    _ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ * ∫⁻ y, ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p := by
        rw [lintegral_mul_const, mul_comm]
        fun_prop
    _ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p : ℝ≥0) * (∫⁻ y, ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p := by
        rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, enorm_eq_nnnorm, ← ENNReal.coe_rpow_of_nonneg _ h0p]
    _ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p : ℝ≥0)
        * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ∂(volume : Measure (ι → ℝ)).map e.symm) ^ p := by
        congr
        rw [lintegral_map _ e.symm.continuous.measurable]
        fun_prop
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this_1 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this_1
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p
⊢ (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑C : ℝ≥0∞) * (↑(c ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p

Tactic:
rw [← ENNReal.mul_le_mul_iff_right h3c ENNReal.coe_ne_top, ← mul_assoc, ← ENNReal.coe_mul, ← hC,
    ENNReal.coe_mul] at this

Premises used: mul_assoc, ENNReal.coe_mul, ENNReal.mul_le_mul_iff_right, ENNReal.coe_ne_top
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this_1 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this_1
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑C : ℝ≥0∞) * (↑(c ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p
⊢ (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑C : ℝ≥0∞) * (↑(c ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p

Tactic:
this
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this_1 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this_1
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑C : ℝ≥0∞) * (↑(c ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p
⊢ (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑C : ℝ≥0∞) * (↑(c ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p

Tactic:
exact this
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : NNReal.HolderConjugate (↑(finrank ℝ E) : ℝ≥0) p
⊢ 0 < (↑p : ℝ)

Tactic:
have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : NNReal.HolderConjugate (↑(finrank ℝ E) : ℝ≥0) p
h0p : 0 < (↑p : ℝ)
rw :
  ∫⁻ (x : E), ‖u x‖ₑ ^ (↑p : ℝ) ∂μ ≤
    (↑(lintegralPowLePowLIntegralFDerivConst μ (↑p : ℝ)) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ (↑p : ℝ)
⊢ eLpNorm u (↑p : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOneConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) 1 μ

Tactic:
rw [eLpNorm_one_eq_lintegral_enorm,
    ← ENNReal.rpow_le_rpow_iff h0p, ENNReal.mul_rpow_of_nonneg _ _ h0p.le,
    ← ENNReal.coe_rpow_of_nonneg _ h0p.le, eLpNormLESNormFDerivOneConst, ← NNReal.rpow_mul,
    eLpNorm_nnreal_pow_eq_lintegral hp.symm.pos.ne',
    inv_mul_cancel₀ h0p.ne', NNReal.rpow_one]

Premises used: NNReal.HolderConjugate.symm, ENNReal.mul_rpow_of_nonneg, MeasureTheory.eLpNorm_one_eq_lintegral_enorm, NNReal.rpow_mul, ENNReal.coe_rpow_of_nonneg, MeasureTheory.eLpNormLESNormFDerivOneConst, LT.lt.le, LT.lt.ne', NNReal.HolderTriple.pos, ENNReal.rpow_le_rpow_iff, NNReal.rpow_one, MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral, inv_mul_cancel₀
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : NNReal.HolderConjugate (↑(finrank ℝ E) : ℝ≥0) p
h0p : 0 < (↑p : ℝ)
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ (↑p : ℝ) ∂μ ≤
    (↑(lintegralPowLePowLIntegralFDerivConst μ (↑p : ℝ)) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ (↑p : ℝ)

Tactic:
lintegral_pow_le_pow_lintegral_fderiv μ hu h2u hp.coe

Premises used: MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv, NNReal.HolderConjugate.coe
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : NNReal.HolderConjugate (↑(finrank ℝ E) : ℝ≥0) p
h0p : 0 < (↑p : ℝ)
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ (↑p : ℝ) ∂μ ≤
    (↑(lintegralPowLePowLIntegralFDerivConst μ (↑p : ℝ)) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ (↑p : ℝ)

Tactic:
exact lintegral_pow_le_pow_lintegral_fderiv μ hu h2u hp.coe

Premises used: MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv, NNReal.HolderConjugate.coe
-- 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 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
pos :
  ∀ (hp'0 : p' = 0),
    eLpNorm u (↑p' : ℝ≥0∞) μ ≤
      (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
neg :
  ∀ (hp'0 : ¬p' = 0),
    eLpNorm u (↑p' : ℝ≥0∞) μ ≤
      (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
by_cases hp'0 : p' = 0
-- 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 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
hp'0 : p' = 0
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
simp [hp'0]
-- 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 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
hp'0 : ¬p' = 0
⊢ let n := finrank ℝ E;
  0 < n

Tactic:
set n := finrank ℝ E

Premises used: Real, Module.finrank