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)⁻¹
rw : c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹ * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
rw₁ rw₂ : c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
⊢ C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p

Tactic:
rw [h0C, inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']

Premises used: LT.lt.ne', inv_mul_cancel_right₀, NNReal.rpow_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 : ℝ
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)⁻¹
⊢ C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p

Tactic:
have hC : C * c ^ p = c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p := by
    rw [h0C, inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']
-- 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
simp :
  (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑C : ℝ≥0∞) *
      ((↑c : ℝ≥0∞) *
          ∫⁻ (x : E),
            enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p

Tactic:
simp only [h2c, ENNReal.smul_def, lintegral_smul_measure, smul_eq_mul]

Premises used: MeasureTheory.lintegral_smul_measure, ENNReal.smul_def, smul_eq_mul
-- 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)
⊢ ContDiff ℝ 1 v

Tactic:
have hv : ContDiff ℝ 1 v := hu.comp e.symm.contDiff
-- 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
⊢ HasCompactSupport v

Tactic:
have h2v : HasCompactSupport v := h2u.comp_homeomorph e.symm.toHomeomorph
-- 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 = ∫⁻ (y : ι → ℝ), ‖v y‖ₑ ^ p

Tactic:
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
refine : Measurable (β := ℝ≥0∞) fun (x : E) ↦ ‖u x‖ₑ ^ p
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume = ∫⁻ (y : ι → ℝ), ‖v y‖ₑ ^ p

Tactic:
refine 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
⊢ let this := borel F;
  BorelSpace F

Tactic:
borelize F
-- 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
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦ ‖u x‖ₑ ^ p

Tactic:
hu.continuous.measurable.nnnorm.coe_nnreal_ennreal.pow_const _

Premises used: Measurable.coe_nnreal_ennreal, ContDiff.continuous, Measurable.nnnorm, Continuous.measurable, Measurable.pow_const
-- 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
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦ ‖u x‖ₑ ^ p

Tactic:
exact hu.continuous.measurable.nnnorm.coe_nnreal_ennreal.pow_const _

Premises used: Measurable.coe_nnreal_ennreal, ContDiff.continuous, Measurable.nnnorm, Continuous.measurable, Measurable.pow_const
-- 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
h :
  ∀ (y : ι → ℝ),
    Eq (α := (ι → ℝ) →L[ℝ] F) (fderiv ℝ v y)
      (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y)
⊢ (∫⁻ (y : ι → ℝ), enorm (E := (ι → ℝ) →L[ℝ] F) (fderiv ℝ v y)) ^ p =
    (∫⁻ (y : ι → ℝ),
        enorm (E := (ι → ℝ) →L[ℝ] F)
          (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y)) ^
      p

Tactic:
congr! with y
-- 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
y : ι → ℝ
h : DifferentiableAt ℝ (F := E) (⇑e.symm : (a : ι → ℝ) → E) y
⊢ Eq (α := (ι → ℝ) →L[ℝ] F) (fderiv ℝ v y)
    (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y)

Tactic:
apply fderiv_comp _ (hu.differentiable one_ne_zero _)

Premises used: 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
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
y : ι → ℝ
⊢ DifferentiableAt ℝ (F := E) (⇑e.symm : (a : ι → ℝ) → E) y

Tactic:
e.symm.differentiableAt

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.differentiableAt
-- 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
y : ι → ℝ
⊢ DifferentiableAt ℝ (F := E) (⇑e.symm : (a : ι → ℝ) → E) y

Tactic:
exact e.symm.differentiableAt

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.differentiableAt
-- 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
h₁ :
  ∀ (y : ι → ℝ),
    enorm (E := (ι → ℝ) →L[ℝ] F)
        (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y) ≤
      enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ
⊢ (∫⁻ (y : ι → ℝ),
        enorm (E := (ι → ℝ) →L[ℝ] F)
          (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y)) ^
      p ≤
    (∫⁻ (y : ι → ℝ),
        enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ) ^
      p

Tactic:
gcongr with y
-- 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
y : ι → ℝ
h₁ :
  enorm (E := (ι → ℝ) →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL (↑e.symm : (ι → ℝ) →L[ℝ] E)) ≤
    enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ
⊢ enorm (E := (ι → ℝ) →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y) ≤
    enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ

Tactic:
rw [e.symm.fderiv]

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.fderiv
-- 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
y : ι → ℝ
⊢ enorm (E := (ι → ℝ) →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL (↑e.symm : (ι → ℝ) →L[ℝ] E)) ≤
    enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ

Tactic:
apply ContinuousLinearMap.opENorm_comp_le

Premises used: ContinuousLinearMap.opENorm_comp_le