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 : 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
⊢ (↑p : ℝ).HolderConjugate q

Tactic:
have hq : Real.HolderConjugate p q := .conjExponent 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 : 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
⊢ p ≠ 0

Tactic:
have h0p : p ≠ 0 := zero_lt_one.trans hp |>.ne'
-- 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 : 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
⊢ (↑p : ℝ) ≠ 1

Tactic:
have h1p : (p : ℝ) ≠ 1 := hq.lt.ne'
-- 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 : 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
⊢ (↑p : ℝ) - 1 ≠ 0

Tactic:
have h3p : (p : ℝ) - 1 ≠ 0 := sub_ne_zero_of_ne h1p
-- 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 : 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
simp_rw : (↑n' : ℝ)⁻¹ - q⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
⊢ 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)

Tactic:
simp_rw -zeta [one_div, hp']

Premises used: one_div
-- 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 : 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
rw : (↑p : ℝ)⁻¹ - (↑(↑n : ℝ≥0) : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
⊢ (↑n' : ℝ)⁻¹ - q⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹

Tactic:
rw [← hq.one_sub_inv, ← hn.coe.one_sub_inv, sub_sub_sub_cancel_left]

Premises used: Real.HolderConjugate.one_sub_inv, NNReal.HolderConjugate.coe, sub_sub_sub_cancel_left
-- 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 : 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
⊢ (↑p : ℝ)⁻¹ - (↑(↑n : ℝ≥0) : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹

Tactic:
simp only [NNReal.coe_natCast, NNReal.coe_inv]

Premises used: NNReal.coe_natCast, NNReal.coe_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 : 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' : ℝ)

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]
-- 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 : 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 ≤ (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))

Tactic:
positivity
-- 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 : 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 : ℝ))) ⋯
⊢ (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))

Tactic:
have h0γ : (γ : ℝ) = p * (n - 1) / (n - p) := 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 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 : ℝ))
rwa : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ 1 < (↑γ : ℝ)

Tactic:
rwa [h0γ, one_lt_div hnp, mul_sub, mul_one, sub_lt_sub_iff_right, lt_mul_iff_one_lt_left]

Premises used: mul_sub, one_lt_div, sub_lt_sub_iff_right, lt_mul_iff_one_lt_left, mul_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 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 : ℝ))
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
hn.coe.pos

Premises used: NNReal.HolderConjugate.coe, Real.HolderTriple.pos, 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 : 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 : ℝ))
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
exact hn.coe.pos

Premises used: NNReal.HolderConjugate.coe, Real.HolderTriple.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 : 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 < (↑γ : ℝ)

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
-- 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 : 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 < (↑γ : ℝ)
rw :
  ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ)) * ((↑(↑n : ℝ≥0) : ℝ) / ((↑(↑n : ℝ≥0) : ℝ) - 1)))⁻¹ =
    (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
⊢ γ * n' = p'

Tactic:
rw [← NNReal.coe_inj, ← inv_inj, hp', NNReal.coe_mul, h0γ, hn.coe.conjugate_eq]

Premises used: NNReal.HolderConjugate.coe, Real.HolderConjugate.conjugate_eq, inv_inj, NNReal.coe_mul, NNReal.coe_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 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 < (↑γ : ℝ)
⊢ ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ)) * ((↑(↑n : ℝ≥0) : ℝ) / ((↑(↑n : ℝ≥0) : ℝ) - 1)))⁻¹ =
    (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹

Tactic:
simp [field]
-- 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 : 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'

Tactic:
have h2γ : γ * n' = p' := by
    rw [← NNReal.coe_inj, ← inv_inj, hp', NNReal.coe_mul, h0γ, hn.coe.conjugate_eq]
    simp [field]
-- 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 : 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'
rw :
  (((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ)) - 1) * ((↑p : ℝ) / ((↑p : ℝ) - 1)))⁻¹ =
    (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
⊢ ((↑γ : ℝ) - 1) * q = (↑p' : ℝ)

Tactic:
rw [← inv_inj, hp', h0γ, hq.conjugate_eq]

Premises used: Real.HolderConjugate.conjugate_eq, 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 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 : ℝ)) = (↑n : ℝ) * ((↑p : ℝ) - 1)

Tactic:
ring
-- 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 : 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 : ℝ)) = (↑n : ℝ) * ((↑p : ℝ) - 1)

Tactic:
have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
-- 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 : 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'
this : (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 - ((↑n : ℝ) - (↑p : ℝ)) = (↑n : ℝ) * ((↑p : ℝ) - 1)
⊢ (((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ)) - 1) * ((↑p : ℝ) / ((↑p : ℝ) - 1)))⁻¹ =
    (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹

Tactic:
simp [field, this]