awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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) : ℝ)⁻¹
hp'0 : ¬p' = 0
hn₁ :
  let n := finrank ℝ E;
  0 < n
⊢ let n := finrank ℝ E;
  (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹

Tactic:
set n := finrank ℝ E

Premises used: Real, Module.finrank
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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)
⊢ 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'
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ℝ)⁻¹
rwa : ∀ (this : (↑n : ℝ)⁻¹ < (↑p : ℝ)⁻¹), LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ (↑p : ℝ) < (↑n : ℝ)

Tactic:
rwa [NNReal.coe_inv, sub_pos,
      inv_lt_inv₀ _ (zero_lt_one.trans_le (NNReal.coe_le_coe.mpr hp))] at this

Premises used: Iff.mpr, sub_pos, zero_lt_one, NNReal.coe_inv, LT.lt.trans_le, NNReal.coe_le_coe, inv_lt_inv₀
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : (↑n : ℝ)⁻¹ < (↑p : ℝ)⁻¹
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
exact_mod_cast hn
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ℝ)

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
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ℝ)
⊢ 2 ≤ n

Tactic:
have h0n : 2 ≤ n := Nat.succ_le_of_lt <| Nat.one_lt_cast.mp <| hp.trans_lt h2p
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 < n
⊢ LT.lt (α := ℝ≥0) 1 (↑n : ℝ≥0)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
⊢ NNReal.HolderConjugate (↑n : ℝ≥0) n'

Tactic:
have hn : NNReal.HolderConjugate n n' := .conjExponent (by norm_cast)
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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'
⊢ LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)

Tactic:
have h1n : 1 ≤ (n : ℝ≥0) := hn.lt.le
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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)
simp_rw : LT.lt (α := ℝ) 1 (↑n : ℝ)
⊢ 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1

Tactic:
simp_rw [sub_pos]

Premises used: sub_pos
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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)
⊢ LT.lt (α := ℝ) 1 (↑n : ℝ)

Tactic:
hn.coe.lt

Premises used: NNReal.HolderConjugate.coe, Real.HolderTriple.lt, NNReal.toReal
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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)
⊢ LT.lt (α := ℝ) 1 (↑n : ℝ)

Tactic:
exact hn.coe.lt

Premises used: NNReal.HolderConjugate.coe, Real.HolderTriple.lt
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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

Tactic:
have h2n : (0 : ℝ) < n - 1 := by simp_rw [sub_pos]; exact hn.coe.lt
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
simp_rw : (↑p : ℝ) < (↑n : ℝ)
⊢ 0 < (↑n : ℝ) - (↑p : ℝ)

Tactic:
simp_rw [sub_pos]

Premises used: sub_pos
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
⊢ (↑p : ℝ) < (↑n : ℝ)

Tactic:
h2p
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
⊢ (↑p : ℝ) < (↑n : ℝ)

Tactic:
exact h2p
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
⊢ 0 < (↑n : ℝ) - (↑p : ℝ)

Tactic:
have hnp : (0 : ℝ) < n - p := by simp_rw [sub_pos]; exact h2p
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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∞) μ
neg₁ :
  ∀ (hp : 1 < p),
    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∞) μ

Tactic:
rcases hp.eq_or_lt with rfl | hp

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 (↑n' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) 1 μ

Tactic:
eLpNorm_le_eLpNorm_fderiv_one μ hu h2u hn

Premises used: MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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∞)
h₁ : (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑1 : ℝ)) : ℝ≥0∞) = (↑(eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)) : ℝ≥0∞)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑1 : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑1 : ℝ≥0∞) μ

Tactic:
convert! eLpNorm_le_eLpNorm_fderiv_one μ hu h2u hn using 2

Premises used: MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ℝ)
this : (↑p' : ℝ) = (↑n' : ℝ)
⊢ (↑p' : ℝ≥0∞) = (↑n' : ℝ≥0∞)

Tactic:
simpa using this
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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' : ℝ) = (↑n' : ℝ)
⊢ (↑p' : ℝ≥0∞) = (↑n' : ℝ≥0∞)

Tactic:
suffices (p' : ℝ) = n' by simpa using this
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹ = (↑n' : ℝ)⁻¹
⊢ (↑p' : ℝ) = (↑n' : ℝ)

Tactic:
rw [← inv_inj, hp']

Premises used: inv_inj
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ℝ)
⊢ (↑1⁻¹ : ℝ) - (↑n : ℝ)⁻¹ = (↑n' : ℝ)⁻¹

Tactic:
simp [field, n', NNReal.conjExponent, *]

Premises used: NNReal.conjExponent
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : eLpNormLESNormFDerivOfEqInnerConst μ 1 = eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)
⊢ (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑1 : ℝ)) : ℝ≥0∞) = (↑(eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)) : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 :
  eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ) *
      (1 * HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 / HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1).toNNReal =
    eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ)
⊢ eLpNormLESNormFDerivOfEqInnerConst μ 1 = eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)

Tactic:
simp_rw [n', n, eLpNormLESNormFDerivOfEqInnerConst]

Premises used: MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
h :
  eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ) * Real.toNNReal 1 =
    eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ)
⊢ 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:
field_simp
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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)) : ℝ) * Real.toNNReal 1 =
    eLpNormLESNormFDerivOneConst μ (↑(NNReal.conjExponent (↑(finrank ℝ E) : ℝ≥0)) : ℝ)

Tactic:
simp