awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
inr :
  eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) =
    eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
refine (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos).trans (le_of_eq ?_)

Premises used: MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
inr : 1 / p.toReal = p.toReal⁻¹
⊢ eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) =
    eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ 1 / p.toReal = p.toReal⁻¹

Tactic:
one_div _

Premises used: one_div
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ 1 / p.toReal = p.toReal⁻¹

Tactic:
exact one_div _

Premises used: one_div
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
⊢ p < ∞

Tactic:
have hp_lt_top : p < ∞ := hpq.trans_lt (lt_top_iff_ne_top.mpr hq_top)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
⊢ 0 < p.toReal

Tactic:
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_lt_top.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
hp_pos : 0 < p.toReal
inr :
  eLpNorm' f p.toReal μ ≤
    eLpNorm' f q.toReal μ *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
⊢ eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_lt_top.ne, eLpNorm_eq_eLpNorm' hq0_lt.ne.symm hq_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm', Ne.symm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
hp_pos : 0 < p.toReal
⊢ p.toReal ≤ q.toReal

Tactic:
have hpq_real : p.toReal ≤ q.toReal := ENNReal.toReal_mono hq_top hpq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
hp_pos : 0 < p.toReal
hpq_real : p.toReal ≤ q.toReal
⊢ eLpNorm' f p.toReal μ ≤
    eLpNorm' f q.toReal μ *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)

Tactic:
eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp_pos hpq_real hf

Premises used: MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
hp_pos : 0 < p.toReal
hpq_real : p.toReal ≤ q.toReal
⊢ eLpNorm' f p.toReal μ ≤
    eLpNorm' f q.toReal μ *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)

Tactic:
exact eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp_pos hpq_real hf

Premises used: MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst_2 : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)

Tactic:
have h_le_μ := eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp0_lt hpq hf
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst_2 : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
h_le_μ :
  eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
rwa :
  ∀ (h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) 1 (1 / p - 1 / q)),
    eLpNorm' f p μ ≤ eLpNorm' f q μ
rwa₁ : ∀ (h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * 1), eLpNorm' f p μ ≤ eLpNorm' f q μ
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ), eLpNorm' f p μ ≤ eLpNorm' f q μ
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ

Tactic:
rwa [measure_univ, ENNReal.one_rpow, mul_one] at h_le_μ

Premises used: ENNReal.one_rpow, MeasureTheory.IsProbabilityMeasure.measure_univ, mul_one
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
inst_2 : IsProbabilityMeasure μ
⊢ eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q) = eLpNormEssSup f μ

Tactic:
simp [measure_univ]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
inst_2 : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
⊢ eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal) =
    eLpNorm f q μ

Tactic:
simp [measure_univ]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
inl : ∀ (hp_nonpos : p ≤ 0), eLpNorm' f p μ < ∞
inr : ∀ (hp_pos : 0 < p), eLpNorm' f p μ < ∞
⊢ eLpNorm' f p μ < ∞

Tactic:
rcases le_or_gt p 0 with hp_nonpos | hp_pos

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
inl : eLpNorm' f 0 μ < ∞
⊢ eLpNorm' f p μ < ∞

Tactic:
rw [le_antisymm hp_nonpos hp_nonneg]

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ eLpNorm' f 0 μ < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
⊢ 0 < q

Tactic:
have hq_pos : 0 < q := lt_of_lt_of_le hp_pos hpq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)

Tactic:
eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp_pos hpq hf

Premises used: MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
rw :
  eLpNorm' f q μ < ∞ ∧ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) < ∞ ∨
    eLpNorm' f q μ = 0 ∨ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) = 0
⊢ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) < ∞

Tactic:
rw [ENNReal.mul_lt_top_iff]

Premises used: ENNReal.mul_lt_top_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
refine : 0 ≤ 1 / p - 1 / q
⊢ eLpNorm' f q μ < ∞ ∧ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) < ∞ ∨
    eLpNorm' f q μ = 0 ∨ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) = 0

Tactic:
refine Or.inl ⟨hfq_lt_top, ENNReal.rpow_lt_top_of_nonneg ?_ (by finiteness)⟩

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
rwa : 1 / q ≤ 1 / p - 0
rwa₁ : 1 / q ≤ 1 / p
rwa₂ : q⁻¹ ≤ 1 / p
rwa₃ : q⁻¹ ≤ p⁻¹
rwa₄ rwa₅ rwa₆ rwa₇ : p ≤ q
⊢ 0 ≤ 1 / p - 1 / q

Tactic:
rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]

Premises used: sub_zero, one_div, le_sub_comm, inv_le_inv₀
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : MeasureTheory.eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
eLpNorm' :
  MeasureTheory.eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) < ∞
⊢ MeasureTheory.eLpNorm' f p μ < ∞

Tactic:
calc
    eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q) :=
      eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp_pos hpq hf
    _ < ∞ := by
      rw [ENNReal.mul_lt_top_iff]
      refine Or.inl ⟨hfq_lt_top, ENNReal.rpow_lt_top_of_nonneg ?_ (by finiteness)⟩
      rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]

Premises used: MeasureTheory.eLpNorm', Set.univ, HSub.hSub, MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ, HDiv.hDiv, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hfq : MemLp f q μ
hpq : p ≤ q
⊢ AEStronglyMeasurable f μ

Tactic:
obtain ⟨hfq_m, hfq_lt_top⟩ := hfq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hfq : MemLp f q μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
⊢ eLpNorm f q μ < ∞

Tactic:
obtain ⟨hfq_m, hfq_lt_top⟩ := hfq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
pos : ∀ (hp0 : p = 0), MemLp f p μ
neg : ∀ (hp0 : ¬p = 0), MemLp f p μ
⊢ MemLp f p μ

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p = 0
pos : MemLp f 0 μ
pos₁ pos₂ pos₃ pos₄ : AEStronglyMeasurable f μ
⊢ MemLp f p μ

Tactic:
rwa [hp0, memLp_zero_iff_aestronglyMeasurable]

Premises used: MeasureTheory.memLp_zero_iff_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : ¬p = 0
⊢ p ≠ 0

Tactic:
rw [← Ne] at hp0

Premises used: Ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
⊢ MemLp f p μ

Tactic:
⟨hfq_m, ?_⟩

Premises used: MeasureTheory.MemLp, And.intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
neg : eLpNorm f p μ < ∞
⊢ MemLp f p μ

Tactic:
refine ⟨hfq_m, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
pos : ∀ (hp_top : p = ∞), eLpNorm f p μ < ∞
neg : ∀ (hp_top : ¬p = ∞), eLpNorm f p μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
rwa :
  ∀ (hpq : ∞ ≤ q) (hfq_m : AEStronglyMeasurable f μ) (hfq_lt_top : eLpNorm f q μ < ∞) (hp0 : p ≠ 0) (hp_top : p = ∞),
    q = ∞
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hpq : q = ∞) (hfq_m : AEStronglyMeasurable f μ) (hfq_lt_top : eLpNorm f q μ < ∞) (hp0 : p ≠ 0) (hp_top : p = ∞),
    q = ∞
⊢ q = ∞

Tactic:
rwa [hp_top, top_le_iff] at hpq

Premises used: top_le_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
⊢ q = ∞

Tactic:
have hq_top : q = ∞ := by rwa [hp_top, top_le_iff] at hpq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
hq_top : q = ∞
pos : eLpNorm f ∞ μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
rw [hp_top]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
hq_top : q = ∞
pos pos₁ pos₂ pos₃ :
  ∀ (hfq_lt_top : eLpNorm f ∞ μ < ∞) (hp0 : p ≠ 0) (hp_top : p = ∞) (hq_top : q = ∞), eLpNorm f ∞ μ < ∞
⊢ eLpNorm f ∞ μ < ∞

Tactic:
rwa [hq_top] at hfq_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
⊢ 0 < p.toReal

Tactic:
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
pos : ∀ (hq_top : q = ∞), eLpNorm f p μ < ∞
neg : ∀ (hq_top : ¬q = ∞), eLpNorm f p μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
by_cases hq_top : q = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
pos : eLpNorm' f p.toReal μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNormEssSup f μ < ∞

Tactic:
rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
hfq_lt_top₁ : eLpNormEssSup f μ < ∞
⊢ p ≠ 0

Tactic:
rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
hfq_lt_top₁ : eLpNormEssSup f μ < ∞
hp0₁ : p ≠ 0
⊢ ¬p = ∞

Tactic:
rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
hfq_lt_top₁ : eLpNormEssSup f μ < ∞
hp0₁ : p ≠ 0
hp_top₁ : ¬p = ∞
⊢ 0 < p.toReal

Tactic:
rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
hfq_lt_top₁ : eLpNormEssSup f μ < ∞
hp0₁ : p ≠ 0
hp_top₁ : ¬p = ∞
hp_pos₁ : 0 < p.toReal
⊢ q = ∞

Tactic:
rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNorm' f p.toReal μ < ∞

Tactic:
lt_of_le_of_lt (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos) ?_

Premises used: lt_of_le_of_lt, MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ