awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this_1 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this_1
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p
⊢ (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑C : ℝ≥0∞) *
      ((↑c : ℝ≥0∞) *
          ∫⁻ (x : E),
            enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p
have this₁ : (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
  (↑C : ℝ≥0∞) * (↑(c ^ p) : ℝ≥0∞) *
    (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^ p
Tactic: rw [← ENNReal.mul_le_mul_iff_right h3c ENNReal.coe_ne_top, ← mul_assoc, ← ENNReal.coe_mul, ← hC,
    ENNReal.coe_mul] at this
Cleared hypotheses: this
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : NNReal.HolderConjugate (↑(finrank ℝ E) : ℝ≥0) p
⊢ eLpNorm u (↑p : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOneConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) 1 μ
have h0p : 0 < (↑p : ℝ)
Tactic: have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
-- 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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : NNReal.HolderConjugate (↑(finrank ℝ E) : ℝ≥0) p
h0p : 0 < (↑p : ℝ)
⊢ eLpNorm u (↑p : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOneConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) 1 μ
have rw : ∫⁻ (x : E), ‖u x‖ₑ ^ (↑p : ℝ) ∂μ ≤
  (↑(lintegralPowLePowLIntegralFDerivConst μ (↑p : ℝ)) : ℝ≥0∞) *
    (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ (↑p : ℝ)
Tactic: rw [eLpNorm_one_eq_lintegral_enorm,
    ← ENNReal.rpow_le_rpow_iff h0p, ENNReal.mul_rpow_of_nonneg _ _ h0p.le,
    ← ENNReal.coe_rpow_of_nonneg _ h0p.le, eLpNormLESNormFDerivOneConst, ← NNReal.rpow_mul,
    eLpNorm_nnreal_pow_eq_lintegral hp.symm.pos.ne',
    inv_mul_cancel₀ h0p.ne', NNReal.rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have pos : ∀ (hp'0 : p' = 0),
  eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: by_cases hp'0 : p' = 0
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
pos :
  ∀ (hp'0 : p' = 0),
    eLpNorm u (↑p' : ℝ≥0∞) μ ≤
      (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have neg : ∀ (hp'0 : ¬p' = 0),
  eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: by_cases hp'0 : p' = 0
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
⊢ (↑p : ℝ) < (↑n : ℝ)
have this : 0 < (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
Tactic: have : 0 < p⁻¹ - (n : ℝ)⁻¹ :=
      NNReal.coe_lt_coe.mpr (pos_iff_ne_zero.mpr (inv_ne_zero hp'0)) |>.trans_eq hp'
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
this : 0 < (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
⊢ (↑p : ℝ) < (↑n : ℝ)
have rwa : ∀ (this : (↑n : ℝ)⁻¹ < (↑p : ℝ)⁻¹), LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: rwa [NNReal.coe_inv, sub_pos,
      inv_lt_inv₀ _ (zero_lt_one.trans_le (NNReal.coe_le_coe.mpr hp))] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h2p : (↑p : ℝ) < (↑n : ℝ)
Tactic: have h2p : (p : ℝ) < n := by
    have : 0 < p⁻¹ - (n : ℝ)⁻¹ :=
      NNReal.coe_lt_coe.mpr (pos_iff_ne_zero.mpr (inv_ne_zero hp'0)) |>.trans_eq hp'
    rwa [NNReal.coe_inv, sub_pos,
      inv_lt_inv₀ _ (zero_lt_one.trans_le (NNReal.coe_le_coe.mpr hp))] at this
    exact_mod_cast hn
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h0n : 2 ≤ n
Tactic: have h0n : 2 ≤ n := Nat.succ_le_of_lt <| Nat.one_lt_cast.mp <| hp.trans_lt h2p
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
⊢ LT.lt (α := ℝ≥0) 1 (↑n : ℝ≥0)
have norm_cast : 1 < n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have hn₁ : NNReal.HolderConjugate (↑n : ℝ≥0) n'
Tactic: have hn : NNReal.HolderConjugate n n' := .conjExponent (by norm_cast)
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
Tactic: have h1n : 1 ≤ (n : ℝ≥0) := hn.lt.le
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
⊢ 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
have simp_rw : LT.lt (α := ℝ) 1 (↑n : ℝ)
Tactic: simp_rw [sub_pos]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
Tactic: have h2n : (0 : ℝ) < n - 1 := by simp_rw [sub_pos]; exact hn.coe.lt
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have hnp : 0 < (↑n : ℝ) - (↑p : ℝ)
Tactic: have hnp : (0 : ℝ) < n - p := by simp_rw [sub_pos]; exact h2p
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hnp : 0 < (↑n : ℝ) - (↑p : ℝ)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have neg : ∀ (hp : LE.le (α := ℝ≥0) 1 1) (hp' : (↑p' : ℝ)⁻¹ = (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹) (h2p : (↑1 : ℝ) < (↑n : ℝ))
  (hnp : 0 < (↑n : ℝ) - (↑1 : ℝ)),
  eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑1 : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑1 : ℝ≥0∞) μ
Tactic: rcases hp.eq_or_lt with rfl | hp
Cleared hypotheses: p, hp, hp', h2p, hnp
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hnp : 0 < (↑n : ℝ) - (↑p : ℝ)
neg :
  ∀ (hp : LE.le (α := ℝ≥0) 1 1) (hp' : (↑p' : ℝ)⁻¹ = (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹) (h2p : (↑1 : ℝ) < (↑n : ℝ))
    (hnp : 0 < (↑n : ℝ) - (↑1 : ℝ)),
    eLpNorm u (↑p' : ℝ≥0∞) μ ≤
      (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑1 : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑1 : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have neg₁ : ∀ (hp : 1 < p),
  eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: rcases hp.eq_or_lt with rfl | hp
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hp : LE.le (α := ℝ≥0) 1 1
hp' : (↑p' : ℝ)⁻¹ = (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹
h2p : (↑1 : ℝ) < (↑n : ℝ)
hnp : 0 < (↑n : ℝ) - (↑1 : ℝ)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑1 : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑1 : ℝ≥0∞) μ
have h : (↑p' : ℝ≥0∞) = (↑n' : ℝ≥0∞)
Tactic: convert! eLpNorm_le_eLpNorm_fderiv_one μ hu h2u hn using 2
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hp : LE.le (α := ℝ≥0) 1 1
hp' : (↑p' : ℝ)⁻¹ = (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹
h2p : (↑1 : ℝ) < (↑n : ℝ)
hnp : 0 < (↑n : ℝ) - (↑1 : ℝ)
h : (↑p' : ℝ≥0∞) = (↑n' : ℝ≥0∞)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑1 : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑1 : ℝ≥0∞) μ
have h₁ : (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑1 : ℝ)) : ℝ≥0∞) = (↑(eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)) : ℝ≥0∞)
Tactic: convert! eLpNorm_le_eLpNorm_fderiv_one μ hu h2u hn using 2
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hp : LE.le (α := ℝ≥0) 1 1
hp' : (↑p' : ℝ)⁻¹ = (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹
h2p : (↑1 : ℝ) < (↑n : ℝ)
hnp : 0 < (↑n : ℝ) - (↑1 : ℝ)
⊢ (↑p' : ℝ≥0∞) = (↑n' : ℝ≥0∞)
have h : (↑p' : ℝ) = (↑n' : ℝ)
Tactic: suffices (p' : ℝ) = n' by simpa using this
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hp : LE.le (α := ℝ≥0) 1 1
hp' : (↑p' : ℝ)⁻¹ = (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹
h2p : (↑1 : ℝ) < (↑n : ℝ)
hnp : 0 < (↑n : ℝ) - (↑1 : ℝ)
⊢ (↑p' : ℝ) = (↑n' : ℝ)
have h : (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹ = (↑n' : ℝ)⁻¹
Tactic: rw [← inv_inj, hp']
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hp : LE.le (α := ℝ≥0) 1 1
hp' : (↑p' : ℝ)⁻¹ = (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹
h2p : (↑1 : ℝ) < (↑n : ℝ)
hnp : 0 < (↑n : ℝ) - (↑1 : ℝ)
⊢ (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑1 : ℝ)) : ℝ≥0∞) = (↑(eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)) : ℝ≥0∞)
have h : eLpNormLESNormFDerivOfEqInnerConst μ 1 = eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hp : LE.le (α := ℝ≥0) 1 1
hp' : (↑p' : ℝ)⁻¹ = (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹
h2p : (↑1 : ℝ) < (↑n : ℝ)
hnp : 0 < (↑n : ℝ) - (↑1 : ℝ)
⊢ eLpNormLESNormFDerivOfEqInnerConst μ 1 = eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)
have h : eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ) *
    (1 * HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 / HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1).toNNReal =
  eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ)
Tactic: simp_rw [n', n, eLpNormLESNormFDerivOfEqInnerConst]