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
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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
⊢ (↑p' : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹

Tactic:
have H : (p' : ℝ)⁻¹ ≤ (↑q)⁻¹ := trans hp' hpq
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
H : (↑p' : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
norm_cast : ∀ (H : p'⁻¹ ≤ q⁻¹), q ≤ p'
⊢ (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)

Tactic:
norm_cast at H ⊢
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
ha : 0 < p'
hb : 0 < q
⊢ q ≤ p'

Tactic:
rwa [inv_le_inv₀] at H

Premises used: inv_le_inv₀
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
simp : (↑(finrank ℝ E) : ℝ≥0)⁻¹ < p⁻¹
⊢ 0 < p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹

Tactic:
simp only [tsub_pos_iff_lt]

Premises used: tsub_pos_iff_lt
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ 0 < p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹

Tactic:
have : 0 < p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹ := by
        simp only [tsub_pos_iff_lt]
        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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
this : 0 < p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹
⊢ 0 < 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
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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ 0 < q

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
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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
⊢ (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)

Tactic:
have : (q : ℝ≥0∞) ≤ p' := by
    have H : (p' : ℝ)⁻¹ ≤ (↑q)⁻¹ := trans hp' hpq
    norm_cast at H ⊢
    rwa [inv_le_inv₀] at H
    · dsimp
      have : 0 < p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹ := by
        simp only [tsub_pos_iff_lt]
        gcongr
      positivity
    · 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
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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
rw rw₁ : eLpNorm u (↑q : ℝ≥0∞) μ = eLpNorm u (↑q : ℝ≥0∞) μ
⊢ eLpNorm u (↑q : ℝ≥0∞) μ = eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s)

Tactic:
rw [eLpNorm_restrict_eq_of_support_subset h2u]

Premises used: MeasureTheory.eLpNorm_restrict_eq_of_support_subset
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
⊢ eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s) ≤
    eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) *
      HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (1 / (↑q : ℝ≥0∞).toReal - 1 / (↑p' : ℝ≥0∞).toReal)

Tactic:
eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable

Premises used: ContDiff.continuous, MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ, Continuous.aestronglyMeasurable
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
h :
  (↑t : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (1 / (↑q : ℝ≥0∞).toReal - 1 / (↑p' : ℝ≥0∞).toReal)
⊢ eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s) ≤ eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞)

Tactic:
convert! eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable

Premises used: ContDiff.continuous, MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ, Continuous.aestronglyMeasurable
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
h :
  (↑(ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s)) : ℝ≥0∞) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ)) =
    HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (1 / (↑q : ℝ≥0∞).toReal - 1 / (↑p' : ℝ≥0∞).toReal)
h₁ : 0 ≤ 1 / (↑q : ℝ) - 1 / (↑p' : ℝ)
⊢ (↑t : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (1 / (↑q : ℝ≥0∞).toReal - 1 / (↑p' : ℝ≥0∞).toReal)

Tactic:
rw [ENNReal.coe_rpow_of_nonneg]

Premises used: ENNReal.coe_rpow_of_nonneg
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
⊢ (↑(ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s)) : ℝ≥0∞) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ)) =
    HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (1 / (↑q : ℝ≥0∞).toReal - 1 / (↑p' : ℝ≥0∞).toReal)

Tactic:
simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]

Premises used: ENNReal.coe_toNNReal, Bornology.IsBounded.measure_lt_top, LT.lt.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
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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
h : 0 ≤ (↑q : ℝ)⁻¹ - (↑p' : ℝ)⁻¹
⊢ 0 ≤ 1 / (↑q : ℝ) - 1 / (↑p' : ℝ)

Tactic:
rw [one_div, one_div]

Premises used: one_div
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
h : 0 ≤ (↑q⁻¹ : ℝ) - ((↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹)
⊢ 0 ≤ (↑q⁻¹ : ℝ) - (↑p'⁻¹ : ℝ)

Tactic:
rw [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
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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
⊢ 0 ≤ (↑q⁻¹ : ℝ) - ((↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹)

Tactic:
simpa using hpq
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
rw rw₁ : eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞) = eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
⊢ eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞) = eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞)

Tactic:
rw [eLpNorm_restrict_eq_of_support_subset h2u]

Premises used: MeasureTheory.eLpNorm_restrict_eq_of_support_subset
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
apply : support u ⊆ closure s
⊢ HasCompactSupport u

Tactic:
apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure

Premises used: HasCompactSupport.of_support_subset_isCompact, Bornology.IsBounded.isCompact_closure
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
⊢ support u ⊆ closure s

Tactic:
h2u.trans subset_closure

Premises used: subset_closure, HasSubset.Subset.trans
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
⊢ support u ⊆ closure s

Tactic:
exact h2u.trans subset_closure

Premises used: subset_closure, HasSubset.Subset.trans
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
⊢ HasCompactSupport u

Tactic:
have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
h2u' : HasCompactSupport u
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞) ≤
    (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ * (↑t : ℝ≥0∞)

Tactic:
rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast h2p.pos) hp']

Premises used: LT.lt.pos, Real, congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, LT.lt, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, congrFun', Nat.cast_zero, Eq.symm, Module.finrank, Eq.trans
-- 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)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
simp_rw :
  (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ * (↑t : ℝ≥0∞) =
    (↑(ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑(p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹)⁻¹ : ℝ))) :
          ℝ≥0∞) *
        (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) *
      eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ * (↑t : ℝ≥0∞) =
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]

Premises used: ENNReal.coe_mul, MeasureTheory.eLpNormLESNormFDerivOfLeConst