awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 : ℝ)
⊢ (↑t : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (1 / (↑q : ℝ≥0∞).toReal - 1 / (↑p' : ℝ≥0∞).toReal)
have 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)
Tactic: rw [ENNReal.coe_rpow_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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)
⊢ (↑t : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (1 / (↑q : ℝ≥0∞).toReal - 1 / (↑p' : ℝ≥0∞).toReal)
have h₁ : 0 ≤ 1 / (↑q : ℝ) - 1 / (↑p' : ℝ)
Tactic: rw [ENNReal.coe_rpow_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 ≤ 1 / (↑q : ℝ) - 1 / (↑p' : ℝ)
have h : 0 ≤ (↑q : ℝ)⁻¹ - (↑p' : ℝ)⁻¹
Tactic: rw [one_div, one_div]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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'⁻¹ : ℝ)
have h : 0 ≤ (↑q⁻¹ : ℝ) - ((↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹)
Tactic: rw [hp']
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞) = eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
have rw : eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞) = eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
Tactic: rw [eLpNorm_restrict_eq_of_support_subset h2u]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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
have apply : support u ⊆ closure s
Tactic: apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
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 (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞) ≤
    (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
have h2u' : HasCompactSupport u
Tactic: have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 : ℝ)
⊢ (↑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∞) μ
have 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∞) μ
Tactic: simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc : eLpNorm u (↑q : ℝ≥0∞) μ = eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s)
Tactic: calc eLpNorm u q μ
      = eLpNorm u q (μ.restrict s) := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ eLpNorm u p' (μ.restrict s) * t := by
        convert! eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
        rw [ENNReal.coe_rpow_of_nonneg]
        · simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]
        · rw [one_div, one_div]
          norm_cast
          rw [hp']
          simpa using hpq
    _ = eLpNorm u p' μ * t := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ (C * eLpNorm (fderiv ℝ u) p μ) * t := by
        have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
        rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast h2p.pos) hp']
    _ = eLpNormLESNormFDerivOfLeConst F μ s p q * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]; ring
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 : ℝ)
calc : eLpNorm u (↑q : ℝ≥0∞) μ = eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s)
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc₁ : eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s) ≤ eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞)
Tactic: calc eLpNorm u q μ
      = eLpNorm u q (μ.restrict s) := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ eLpNorm u p' (μ.restrict s) * t := by
        convert! eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
        rw [ENNReal.coe_rpow_of_nonneg]
        · simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]
        · rw [one_div, one_div]
          norm_cast
          rw [hp']
          simpa using hpq
    _ = eLpNorm u p' μ * t := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ (C * eLpNorm (fderiv ℝ u) p μ) * t := by
        have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
        rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast h2p.pos) hp']
    _ = eLpNormLESNormFDerivOfLeConst F μ s p q * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]; ring
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 : ℝ)
calc : eLpNorm u (↑q : ℝ≥0∞) μ = eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s)
calc₁ : eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s) ≤ eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞)
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc₂ : eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞) = eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
Tactic: calc eLpNorm u q μ
      = eLpNorm u q (μ.restrict s) := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ eLpNorm u p' (μ.restrict s) * t := by
        convert! eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
        rw [ENNReal.coe_rpow_of_nonneg]
        · simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]
        · rw [one_div, one_div]
          norm_cast
          rw [hp']
          simpa using hpq
    _ = eLpNorm u p' μ * t := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ (C * eLpNorm (fderiv ℝ u) p μ) * t := by
        have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
        rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast h2p.pos) hp']
    _ = eLpNormLESNormFDerivOfLeConst F μ s p q * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]; ring
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 : ℝ)
calc : eLpNorm u (↑q : ℝ≥0∞) μ = eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s)
calc₁ : eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s) ≤ eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞)
calc₂ : eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞) = eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc₃ : eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞) ≤ (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
Tactic: calc eLpNorm u q μ
      = eLpNorm u q (μ.restrict s) := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ eLpNorm u p' (μ.restrict s) * t := by
        convert! eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
        rw [ENNReal.coe_rpow_of_nonneg]
        · simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]
        · rw [one_div, one_div]
          norm_cast
          rw [hp']
          simpa using hpq
    _ = eLpNorm u p' μ * t := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ (C * eLpNorm (fderiv ℝ u) p μ) * t := by
        have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
        rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast h2p.pos) hp']
    _ = eLpNormLESNormFDerivOfLeConst F μ s p q * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]; ring
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 : ℝ)
calc : eLpNorm u (↑q : ℝ≥0∞) μ = eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s)
calc₁ : eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s) ≤ eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞)
calc₂ : eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞) = eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
calc₃ :
  eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞) ≤
    (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc₄ : (↑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: calc eLpNorm u q μ
      = eLpNorm u q (μ.restrict s) := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ eLpNorm u p' (μ.restrict s) * t := by
        convert! eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
        rw [ENNReal.coe_rpow_of_nonneg]
        · simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]
        · rw [one_div, one_div]
          norm_cast
          rw [hp']
          simpa using hpq
    _ = eLpNorm u p' μ * t := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ (C * eLpNorm (fderiv ℝ u) p μ) * t := by
        have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
        rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast h2p.pos) hp']
    _ = eLpNormLESNormFDerivOfLeConst F μ s p q * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]; ring
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hs : Bornology.IsBounded s
⊢ eLpNorm u (↑p : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p p) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have refine : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑p : ℝ)⁻¹
Tactic: refine eLpNorm_le_eLpNorm_fderiv_of_le μ hu h2u hp h2p ?_ hs
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
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 : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hs : Bornology.IsBounded s
⊢ (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑p⁻¹ : ℝ)
have simp : LE.le (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)⁻¹
Tactic: simp only [tsub_le_iff_right, le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.Analysis.Hofer (goal)
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
⊢ ∃ ε' > 0, ∃ (x' : X), ε' ≤ ε ∧ d x' x ≤ 2 * ε ∧ ε * ϕ x ≤ ε' * ϕ x' ∧ ∀ (y : X), d x' y ≤ ε' → ϕ y ≤ 2 * ϕ x'
have by_contra! : ∀
  (H :
    ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
      ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y),
  False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Analysis.Hofer (goal)
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H :
  ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
    ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
have rw : 0 < HPow.hPow (α := ℝ) 2 k
Tactic: rw [div_mul_eq_mul_div, le_div_iff₀, mul_assoc, mul_le_mul_iff_right₀ ε_pos, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Hofer (hypothesis)
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H :
  ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
    ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
⊢ False
have reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
Tactic: have reformulation : ∀ (x') (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x' := by
    intro x' k
    rw [div_mul_eq_mul_div, le_div_iff₀, mul_assoc, mul_le_mul_iff_right₀ ε_pos, mul_comm]
    positivity