awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 < HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1
⊢ eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ) *
      (1 * HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 / HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1).toNNReal =
    eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ)
have h : eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ) * Real.toNNReal 1 =
  eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ)
Tactic: field_simp
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have hq : (↑p : ℝ).HolderConjugate q
Tactic: have hq : Real.HolderConjugate p q := .conjExponent hp
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h0p : p ≠ 0
Tactic: have h0p : p ≠ 0 := zero_lt_one.trans hp |>.ne'
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h1p : (↑p : ℝ) ≠ 1
Tactic: have h1p : (p : ℝ) ≠ 1 := hq.lt.ne'
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h3p : (↑p : ℝ) - 1 ≠ 0
Tactic: have h3p : (p : ℝ) - 1 ≠ 0 := sub_ne_zero_of_ne h1p
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
⊢ 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
have simp_rw : (↑n' : ℝ)⁻¹ - q⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
Tactic: simp_rw -zeta [one_div, 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
⊢ (↑n' : ℝ)⁻¹ - q⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
have rw : (↑p : ℝ)⁻¹ - (↑(↑n : ℝ≥0) : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
Tactic: rw [← hq.one_sub_inv, ← hn.coe.one_sub_inv, sub_sub_sub_cancel_left]
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
Tactic: have h2q : 1 / n' - 1 / q = 1 / p' := by
    simp_rw -zeta [one_div, hp']
    rw [← hq.one_sub_inv, ← hn.coe.one_sub_inv, sub_sub_sub_cancel_left]
    simp only [NNReal.coe_natCast, NNReal.coe_inv]
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
Tactic: have h0γ : (γ : ℝ) = p * (n - 1) / (n - p) := rfl
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
⊢ 1 < (↑γ : ℝ)
have rwa : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: rwa [h0γ, one_lt_div hnp, mul_sub, mul_one, sub_lt_sub_iff_right, lt_mul_iff_one_lt_left]
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h1γ : 1 < (↑γ : ℝ)
Tactic: have h1γ : 1 < (γ : ℝ) := by
    rwa [h0γ, one_lt_div hnp, mul_sub, mul_one, sub_lt_sub_iff_right, lt_mul_iff_one_lt_left]
    exact hn.coe.pos
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
⊢ γ * n' = p'
have rw : ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ)) * ((↑(↑n : ℝ≥0) : ℝ) / ((↑(↑n : ℝ≥0) : ℝ) - 1)))⁻¹ =
  (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
Tactic: rw [← NNReal.coe_inj, ← inv_inj, hp', NNReal.coe_mul, h0γ, hn.coe.conjugate_eq]
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h2γ : γ * n' = p'
Tactic: have h2γ : γ * n' = p' := by
    rw [← NNReal.coe_inj, ← inv_inj, hp', NNReal.coe_mul, h0γ, hn.coe.conjugate_eq]
    simp [field]
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
h2γ : γ * n' = p'
⊢ ((↑γ : ℝ) - 1) * q = (↑p' : ℝ)
have rw : (((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ)) - 1) * ((↑p : ℝ) / ((↑p : ℝ) - 1)))⁻¹ =
  (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
Tactic: rw [← inv_inj, hp', h0γ, hq.conjugate_eq]
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
h2γ : γ * n' = p'
⊢ (((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ)) - 1) * ((↑p : ℝ) / ((↑p : ℝ) - 1)))⁻¹ =
    (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
have this : (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 - ((↑n : ℝ) - (↑p : ℝ)) = (↑n : ℝ) * ((↑p : ℝ) - 1)
Tactic: have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
h2γ : γ * n' = p'
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h3γ : ((↑γ : ℝ) - 1) * q = (↑p' : ℝ)
Tactic: have h3γ : (γ - 1) * q = p' := by
    rw [← inv_inj, hp', h0γ, hq.conjugate_eq]
    have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
    simp [field, 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
h2γ : γ * n' = p'
h3γ : ((↑γ : ℝ) - 1) * q = (↑p' : ℝ)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h4γ : (↑γ : ℝ) ≠ 0
Tactic: have h4γ : (γ : ℝ) ≠ 0 := (zero_lt_one.trans h1γ).ne'
-- 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 : 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 : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
h2γ : γ * n' = p'
h3γ : ((↑γ : ℝ) - 1) * q = (↑p' : ℝ)
h4γ : (↑γ : ℝ) ≠ 0
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have pos : ∀ (h3u : ∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ = 0),
  eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: by_cases h3u : ∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ = 0