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
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)
h : ∀ᵐ (x : E) ∂μ, nnnorm (E := F) (((⇑e.symm : (a : F') → F) ∘ v) x) ≤ C₁ * ‖v x‖₊
⊢ eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ ≤ C₁ • eLpNorm v (↑p' : ℝ≥0∞) μ

Tactic:
apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul

Premises used: MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_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
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)
⊢ ∀ᵐ (x : E) ∂μ, nnnorm (E := F) (((⇑e.symm : (a : F') → F) ∘ v) x) ≤ C₁ * ‖v x‖₊

Tactic:
Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)

Premises used: ContinuousLinearEquiv.symm, Filter.Eventually.of_forall, ContinuousLinearMap.le_opNNNorm, ContinuousLinearEquiv.toContinuousLinearMap
-- 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)
⊢ ∀ᵐ (x : E) ∂μ, nnnorm (E := F) (((⇑e.symm : (a : F') → F) ∘ v) x) ≤ C₁ * ‖v x‖₊

Tactic:
exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)

Premises used: ContinuousLinearEquiv.symm, Filter.Eventually.of_forall, ContinuousLinearMap.le_opNNNorm, ContinuousLinearEquiv.toContinuousLinearMap
-- 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)
⊢ C₁ • eLpNorm v (↑p' : ℝ≥0∞) μ = (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ

Tactic:
rfl

Premises used: rfl
-- 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)
rw :
  (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * ((↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ)
⊢ (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- 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)
⊢ (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * ((↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ)

Tactic:
gcongr
-- 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)
bc :
  eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ ≤
    (↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * ((↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ)

Tactic:
gcongr
-- 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)
⊢ eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ ≤
    (↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p

Premises used: ENNReal.ofNNReal, Filter.Eventually.of_forall, MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_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
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)
⊢ eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ ≤
    (↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
exact eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p

Premises used: ENNReal.ofNNReal, Filter.Eventually.of_forall, MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_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
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 :
  (↑(nnnorm.{u_3} (E := F' →L[ℝ] F) (↑(ContinuousLinearEquiv.symm toEuclidean) : F' →L[ℝ] F)) : ℝ≥0∞) *
        (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
      ((↑(nnnorm.{u_3} (E := F →L[ℝ] F') (↑toEuclidean : F →L[ℝ] F')) : ℝ≥0∞) *
        eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ) =
    (↑(nnnorm.{u_3} (E := EuclideanSpace ℝ (Fin (finrank ℝ F)) →L[ℝ] F)
                (↑(ContinuousLinearEquiv.symm toEuclidean) : EuclideanSpace ℝ (Fin (finrank ℝ F)) →L[ℝ] F) *
              eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ) *
            nnnorm.{u_3} (E := F →L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ F)))
              (↑toEuclidean : F →L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ F)))) :
        ℝ≥0∞) *
      eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * ((↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ) =
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]

Premises used: MeasureTheory.SNormLESNormFDerivOfEqConst
-- 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)
⊢ (↑(nnnorm.{u_3} (E := F' →L[ℝ] F) (↑(ContinuousLinearEquiv.symm toEuclidean) : F' →L[ℝ] F)) : ℝ≥0∞) *
        (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
      ((↑(nnnorm.{u_3} (E := F →L[ℝ] F') (↑toEuclidean : F →L[ℝ] F')) : ℝ≥0∞) *
        eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ) =
    (↑(nnnorm.{u_3} (E := EuclideanSpace ℝ (Fin (finrank ℝ F)) →L[ℝ] F)
                (↑(ContinuousLinearEquiv.symm toEuclidean) : EuclideanSpace ℝ (Fin (finrank ℝ F)) →L[ℝ] F)) :
            ℝ≥0∞) *
          (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
        (↑(nnnorm.{u_3} (E := F →L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ F)))
              (↑toEuclidean : F →L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ F)))) :
          ℝ≥0∞) *
      eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
simp_rw [mul_assoc]

Premises used: mul_assoc
-- 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)
calc : eLpNorm u (↑p' : ℝ≥0∞) μ = eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ
calc₁ : eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ ≤ C₁ • eLpNorm v (↑p' : ℝ≥0∞) μ
calc₂ :
  (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
calc₃ :
  (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * ((↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ)
calc₄ :
  (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * ((↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ) =
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
calc eLpNorm u p' μ
      = eLpNorm (e.symm ∘ v) p' μ := by simp_rw [v, Function.comp_def, e.symm_apply_apply]
    _ ≤ C₁ • eLpNorm v p' μ := by
      apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
      exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)
    _ = C₁ * eLpNorm v p' μ := rfl
    _ ≤ C₁ * C * eLpNorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
    _ ≤ C₁ * C * (C₂ * eLpNorm (fderiv ℝ u) p μ) := by
      gcongr; exact eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p
    _ = SNormLESNormFDerivOfEqConst F μ p * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
      push_cast
      simp_rw [mul_assoc]

Premises used: ContinuousLinearEquiv.symm, Real, ENNReal.ofNNReal, HMul.hMul, Function.comp, fderiv, MeasureTheory.SNormLESNormFDerivOfEqConst, DFunLike.coe, NNReal.toReal, rfl, MeasureTheory.eLpNorm
-- 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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hpq : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
hs : Bornology.IsBounded s
pos :
  ∀ (hq0 : q = 0),
    eLpNorm u (↑q : ℝ≥0∞) μ ≤
      (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
neg :
  ∀ (hq0 : ¬q = 0),
    eLpNorm u (↑q : ℝ≥0∞) μ ≤
      (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
by_cases hq0 : q = 0
-- 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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hpq : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
hs : Bornology.IsBounded s
hq0 : q = 0
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
simp [hq0]
-- 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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hpq : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹)⁻¹
rw : (↑p⁻¹ : ℝ) - (↑(↑(finrank ℝ E) : ℝ≥0)⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
rw₁ : (↑(finrank ℝ E) : ℝ≥0)⁻¹ ≤ p⁻¹
⊢ (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹

Tactic:
rw [inv_inv, NNReal.coe_sub]

Premises used: inv_inv, NNReal.coe_sub
-- 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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hpq : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹)⁻¹
⊢ (↑p⁻¹ : ℝ) - (↑(↑(finrank ℝ E) : ℝ≥0)⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹

Tactic:
simp
-- 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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hpq : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹)⁻¹
hb : 0 < p
⊢ (↑(finrank ℝ E) : ℝ≥0)⁻¹ ≤ p⁻¹

Tactic:
gcongr
-- 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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hpq : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹)⁻¹
⊢ (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹

Tactic:
have hp' : p'⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹ := by
    rw [inv_inv, NNReal.coe_sub]
    · simp
    · gcongr