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
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
calc : eLpNorm u (↑p' : ℝ≥0∞) μ = eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc₁ : eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ ≤ C₁ • eLpNorm v (↑p' : ℝ≥0∞) μ
Tactic: calc eLpNorm u p' μ
      = eLpNorm (e.symm ∘ v) p' μ := by simp_rw [v, Function.comp_def, e.symm_apply_apply]
    _ ≤ C₁ • eLpNorm v p' μ := by
      apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
      exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)
    _ = C₁ * eLpNorm v p' μ := rfl
    _ ≤ C₁ * C * eLpNorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
    _ ≤ C₁ * C * (C₂ * eLpNorm (fderiv ℝ u) p μ) := by
      gcongr; exact eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p
    _ = SNormLESNormFDerivOfEqConst F μ p * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
      push_cast
      simp_rw [mul_assoc]
-- 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
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
calc : eLpNorm u (↑p' : ℝ≥0∞) μ = eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ
calc₁ : eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ ≤ C₁ • eLpNorm v (↑p' : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc₂ : (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ ≤
  (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
Tactic: calc eLpNorm u p' μ
      = eLpNorm (e.symm ∘ v) p' μ := by simp_rw [v, Function.comp_def, e.symm_apply_apply]
    _ ≤ C₁ • eLpNorm v p' μ := by
      apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
      exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)
    _ = C₁ * eLpNorm v p' μ := rfl
    _ ≤ C₁ * C * eLpNorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
    _ ≤ C₁ * C * (C₂ * eLpNorm (fderiv ℝ u) p μ) := by
      gcongr; exact eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p
    _ = SNormLESNormFDerivOfEqConst F μ p * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
      push_cast
      simp_rw [mul_assoc]
-- 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
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
calc : eLpNorm u (↑p' : ℝ≥0∞) μ = eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ
calc₁ : eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ ≤ C₁ • eLpNorm v (↑p' : ℝ≥0∞) μ
calc₂ :
  (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc₃ : (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ ≤
  (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * ((↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ)
Tactic: calc eLpNorm u p' μ
      = eLpNorm (e.symm ∘ v) p' μ := by simp_rw [v, Function.comp_def, e.symm_apply_apply]
    _ ≤ C₁ • eLpNorm v p' μ := by
      apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
      exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)
    _ = C₁ * eLpNorm v p' μ := rfl
    _ ≤ C₁ * C * eLpNorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
    _ ≤ C₁ * C * (C₂ * eLpNorm (fderiv ℝ u) p μ) := by
      gcongr; exact eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p
    _ = SNormLESNormFDerivOfEqConst F μ p * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
      push_cast
      simp_rw [mul_assoc]
-- 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
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
calc : eLpNorm u (↑p' : ℝ≥0∞) μ = eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ
calc₁ : eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ ≤ C₁ • eLpNorm v (↑p' : ℝ≥0∞) μ
calc₂ :
  (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
calc₃ :
  (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * ((↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc₄ : (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * ((↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ) =
  (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: calc eLpNorm u p' μ
      = eLpNorm (e.symm ∘ v) p' μ := by simp_rw [v, Function.comp_def, e.symm_apply_apply]
    _ ≤ C₁ • eLpNorm v p' μ := by
      apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
      exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)
    _ = C₁ * eLpNorm v p' μ := rfl
    _ ≤ C₁ * C * eLpNorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
    _ ≤ C₁ * C * (C₂ * eLpNorm (fderiv ℝ u) p μ) := by
      gcongr; exact eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p
    _ = SNormLESNormFDerivOfEqConst F μ p * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
      push_cast
      simp_rw [mul_assoc]
-- 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
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have pos : ∀ (hq0 : q = 0),
  eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: by_cases hq0 : q = 0
-- 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
pos :
  ∀ (hq0 : q = 0),
    eLpNorm u (↑q : ℝ≥0∞) μ ≤
      (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have neg : ∀ (hq0 : ¬q = 0),
  eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: by_cases hq0 : q = 0
-- 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)⁻¹)⁻¹
⊢ (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
have rw : (↑p⁻¹ : ℝ) - (↑(↑(finrank ℝ E) : ℝ≥0)⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
Tactic: rw [inv_inv, NNReal.coe_sub]
-- 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)⁻¹)⁻¹
rw : (↑p⁻¹ : ℝ) - (↑(↑(finrank ℝ E) : ℝ≥0)⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
⊢ (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
have rw₁ : (↑(finrank ℝ E) : ℝ≥0)⁻¹ ≤ p⁻¹
Tactic: rw [inv_inv, NNReal.coe_sub]
-- 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)⁻¹)⁻¹
⊢ (↑(finrank ℝ E) : ℝ≥0)⁻¹ ≤ p⁻¹
have hb : 0 < p
Tactic: gcongr
-- 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)⁻¹)⁻¹
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
Tactic: have hp' : p'⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹ := by
    rw [inv_inv, NNReal.coe_sub]
    · simp
    · gcongr
-- 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) : ℝ)⁻¹
⊢ (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
have H : (↑p' : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
Tactic: have H : (p' : ℝ)⁻¹ ≤ (↑q)⁻¹ := trans hp' hpq
-- 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) : ℝ)⁻¹
H : (↑p' : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
⊢ (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
have norm_cast : ∀ (H : p'⁻¹ ≤ q⁻¹), q ≤ p'
Tactic: norm_cast at H ⊢
Cleared hypotheses: H
-- 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) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ q ≤ p'
have ha : 0 < p'
Tactic: rwa [inv_le_inv₀] at H
-- 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) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
ha : 0 < p'
⊢ q ≤ p'
have hb : 0 < q
Tactic: rwa [inv_le_inv₀] at H
-- 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) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ 0 < p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹
have simp : (↑(finrank ℝ E) : ℝ≥0)⁻¹ < p⁻¹
Tactic: simp only [tsub_pos_iff_lt]
-- 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) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ (↑(finrank ℝ E) : ℝ≥0)⁻¹ < p⁻¹
have hb : 0 < p
Tactic: gcongr
-- 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) : ℝ)⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ 0 < p'
have this : 0 < p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹
Tactic: have : 0 < p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹ := by
        simp only [tsub_pos_iff_lt]
        gcongr
-- 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) : ℝ)⁻¹
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have this : (↑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
-- 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∞) μ = eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s)
have rw : eLpNorm u (↑q : ℝ≥0∞) μ = eLpNorm u (↑q : ℝ≥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 : ℝ)
⊢ eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s) ≤ eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞)
have h : (↑t : ℝ≥0∞) =
  HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 / (↑q : ℝ≥0∞).toReal - 1 / (↑p' : ℝ≥0∞).toReal)
Tactic: convert! eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable