awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ HasCompactSupport (u ∘ update (β := fun (a : ι) ↦ ℝ) x i)

Tactic:
exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)

Premises used: HasCompactSupport.comp_isClosedEmbedding, isClosedEmbedding_update
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ ≤
    ∫⁻ (xᵢ : ℝ),
      enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))

Tactic:
?_
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hfg :
  ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ ≤
    ∫⁻ (xᵢ : ℝ),
      enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))
⊢ ‖u x‖ₑ ≤
    ∫⁻ (xᵢ : ℝ),
      enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))

Tactic:
calc ‖u x‖ₑ
    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ := by
        apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
        · exact hu.comp (by convert! contDiff_update 1 x i)
        · exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)
    _ ≤ ∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ := ?_

Premises used: Set.Iic
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hfg : Measure.restrict volume (Set.Iic (x i)) ≤ volume
hfg₁ :
  ∀ (y : ℝ),
    ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ ≤
      enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y))
⊢ ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ ≤
    ∫⁻ (xᵢ : ℝ),
      enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))

Tactic:
gcongr with y
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Measure.restrict volume (Set.Iic (x i)) ≤ volume

Tactic:
Measure.restrict_le_self

Premises used: MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Measure.restrict volume (Set.Iic (x i)) ≤ volume

Tactic:
exact Measure.restrict_le_self

Premises used: MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
y : ℝ
rw rw₁ :
  enorm.{u_3} (E := F)
      ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
          (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
        F) =
    enorm.{u_3} (E := F)
      ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
          (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
        F)
⊢ ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ =
    enorm.{u_3} (E := F)
      ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
          (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
        F)

Tactic:
rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]

Premises used: fderiv_comp_deriv, Differentiable.differentiableAt, HasDerivAt.differentiableAt, hasDerivAt_update, ContDiff.differentiable, one_ne_zero
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
y : ℝ
⊢ enorm.{u_3} (E := F)
      ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
          (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
        F) ≤
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y)) *
      ‖deriv (update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ

Tactic:
ContinuousLinearMap.le_opENorm _ _

Premises used: ContinuousLinearMap.le_opENorm
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
y : ℝ
⊢ enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y)) *
      ‖deriv (update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ ≤
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
      (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y))

Tactic:
simp [deriv_update, Pi.enorm_single]

Premises used: Pi.enorm_single, deriv_update
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
y : ℝ
calc :
  ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ =
    enorm.{u_3} (E := F)
      ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
          (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
        F)
calc₁ :
  enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y)) *
      ‖deriv (update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ ≤
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
      (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y))
⊢ ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ ≤
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
      (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y))

Tactic:
calc ‖deriv (u ∘ update x i) y‖ₑ = ‖fderiv ℝ u (update x i y) (deriv (update x i) y)‖ₑ := by
        rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ * ‖deriv (update x i) y‖ₑ := ContinuousLinearMap.le_opENorm _ _
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ := by simp [deriv_update, Pi.enorm_single]

Premises used: Real, Function.update, deriv, Function.comp, fderiv, ContinuousLinearMap.le_opENorm, DFunLike.coe
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι_1 : Type u_1
A : ι_1 → Type u_2
inst : (i : ι_1) → MeasurableSpace (A i)
μ_1 : (i : ι_1) → Measure (A i)
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : FiniteDimensional ℝ E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
p : ℝ
ι : Type := Fin (finrank ℝ E)
rw : finrank ℝ E = #ι
rw₁ rw₂ : finrank ℝ E = finrank ℝ E
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)

Tactic:
rw [finrank_fintype_fun_eq_card, Fintype.card_fin (finrank ℝ E)]

Premises used: Real, Fintype.card_fin, Module.finrank_fintype_fun_eq_card, Module.finrank
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι_1 : Type u_1
A : ι_1 → Type u_2
inst : (i : ι_1) → MeasurableSpace (A i)
μ_1 : (i : ι_1) → Measure (A i)
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : FiniteDimensional ℝ E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
p : ℝ
ι : Type := Fin (finrank ℝ E)
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)

Tactic:
have : finrank ℝ E = finrank ℝ (ι → ℝ) := by
    rw [finrank_fintype_fun_eq_card, Fintype.card_fin (finrank ℝ E)]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι_1 : Type u_1
A : ι_1 → Type u_2
inst : (i : ι_1) → MeasurableSpace (A i)
μ_1 : (i : ι_1) → Measure (A i)
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : FiniteDimensional ℝ E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
p : ℝ
ι : Type := Fin (finrank ℝ E)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
⊢ ℝ≥0

Tactic:
exact (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹

Premises used: ContinuousLinearEquiv.symm, HMul.hMul, NNNorm.nnnorm, HPow.hPow, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
set :
  let C := lintegralPowLePowLIntegralFDerivConst μ p;
  ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤
    (↑(lintegralPowLePowLIntegralFDerivConst μ p) : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p

Tactic:
set C := lintegralPowLePowLIntegralFDerivConst μ p

Premises used: MeasureTheory.lintegralPowLePowLIntegralFDerivConst
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
⊢ #ι = finrank ℝ E

Tactic:
have hιcard : #ι = finrank ℝ E := Fintype.card_fin (finrank ℝ E)
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)

Tactic:
simp [hιcard]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)

Tactic:
have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [hιcard]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
rwa rwa₁ rwa₂ rwa₃ : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
⊢ Real.HolderConjugate (↑#ι : ℝ) p

Tactic:
rwa [hιcard]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
⊢ Real.HolderConjugate (↑#ι : ℝ) p

Tactic:
have hp : Real.HolderConjugate #ι p := by rwa [hιcard]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
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 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
⊢ 0 ≤ p

Tactic:
have h0p : 0 ≤ p := hp.symm.nonneg
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
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 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
⊢ 0 < c

Tactic:
have hc : 0 < c := addHaarScalarFactor_pos_of_isAddHaarMeasure ..
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
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 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
⊢ μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)

Tactic:
have h2c : μ = c • ((volume : Measure (ι → ℝ)).map e.symm) := isAddLeftInvariant_eq_smul ..
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
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 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
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)
simp_rw : ¬(↑c : ℝ≥0∞) = 0
simp_rw₁ : ¬c = 0
simp_rw₂ : ¬False
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]

Premises used: ENNReal.coe_eq_zero, ne_eq, LT.lt.ne', not_false_eq_true
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
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 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
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)
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
have h3c : (c : ℝ≥0∞) ≠ 0 := by simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
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 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
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
simp_rw :
  C =
    μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) *
        ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p *
      (μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^ p)⁻¹
simp_rw₁ :
  C =
    μ.addHaarScalarFactor
          (Measure.map (α := Fin (finrank ℝ E) → ℝ) (⇑e.symm : (a : Fin (finrank ℝ E) → ℝ) → E) volume) *
        ‖(↑e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊ ^ p *
      (μ.addHaarScalarFactor
            (Measure.map (α := Fin (finrank ℝ E) → ℝ) (⇑e.symm : (a : Fin (finrank ℝ E) → ℝ) → E) volume) ^
          p)⁻¹
simp_rw₂ :
  lintegralPowLePowLIntegralFDerivConst μ p =
    μ.addHaarScalarFactor
          (Measure.map (α := Fin (finrank ℝ E) → ℝ) (⇑e.symm : (a : Fin (finrank ℝ E) → ℝ) → E) volume) *
        ‖(↑e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊ ^ p *
      (μ.addHaarScalarFactor
            (Measure.map (α := Fin (finrank ℝ E) → ℝ) (⇑e.symm : (a : Fin (finrank ℝ E) → ℝ) → E) volume) ^
          p)⁻¹
simp_rw₃ :
  lintegralPowLePowLIntegralFDerivConst μ p =
    μ.addHaarScalarFactor
          (Measure.map (α := Fin (finrank ℝ E) → ℝ)
            (⇑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.ofFinrankEq this)) : (a : Fin (finrank ℝ E) → ℝ) → E)
            volume) *
        nnnorm (E := (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)
            (↑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.ofFinrankEq this)) : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E) ^
          p *
      (μ.addHaarScalarFactor
            (Measure.map (α := Fin (finrank ℝ E) → ℝ)
              (⇑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.ofFinrankEq this)) : (a : Fin (finrank ℝ E) → ℝ) → E)
              volume) ^
          p)⁻¹
⊢ C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹

Tactic:
simp_rw [c, ι, C, e, lintegralPowLePowLIntegralFDerivConst]

Premises used: MeasureTheory.lintegralPowLePowLIntegralFDerivConst
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
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 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
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
⊢ C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹

Tactic:
have h0C : C = (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹ := by
    simp_rw [c, ι, C, e, lintegralPowLePowLIntegralFDerivConst]