awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNorm f p μ ≤ ENNReal.ofReal C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
exact eLpNorm_le_of_ae_nnnorm_bound (hfC.mono fun x hx => hx.trans C.le_coe_toNNReal)

Premises used: MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound, Filter.Eventually.mono, LE.le.trans, Real.le_coe_toNNReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
⊢ eLpNorm f p μ = eLpNorm g p μ

Tactic:
le_antisymm (eLpNorm_mono_enorm_ae <| EventuallyEq.le hfg)
    (eLpNorm_mono_enorm_ae <| (EventuallyEq.symm hfg).le)

Premises used: Filter.EventuallyEq.le, le_antisymm, MeasureTheory.eLpNorm_mono_enorm_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
⊢ eLpNorm f p μ = eLpNorm g p μ

Tactic:
le_antisymm (eLpNorm_mono_nnnorm_ae <| EventuallyEq.le hfg)
    (eLpNorm_mono_nnnorm_ae <| (EventuallyEq.symm hfg).le)

Premises used: MeasureTheory.eLpNorm_mono_nnnorm_ae, Filter.EventuallyEq.le, le_antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖
⊢ eLpNorm f p μ = eLpNorm g p μ

Tactic:
eLpNorm_congr_nnnorm_ae <| hfg.mono fun _x hx => NNReal.eq hx

Premises used: NNReal.eq, Filter.Eventually.mono, MeasureTheory.eLpNorm_congr_nnnorm_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
f : α → E
x : α
⊢ ‖(s.indicator f - t.indicator f) x‖ = ‖(s ∆ t).indicator f x‖

Tactic:
simp [Set.apply_indicator_symmDiff norm_neg]

Premises used: Set.apply_indicator_symmDiff, norm_neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
⊢ eLpNorm' (ε := ℝ) (fun (a : α) ↦ ‖f a‖) q μ = eLpNorm' f q μ

Tactic:
simp [eLpNorm'_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (a : α) ↦ ‖f a‖ₑ) q μ = eLpNorm' f q μ

Tactic:
simp [eLpNorm'_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ = eLpNorm f p μ

Tactic:
eLpNorm_congr_norm_ae <| Eventually.of_forall fun _ => norm_norm _

Premises used: Filter.Eventually.of_forall, norm_norm, MeasureTheory.eLpNorm_congr_norm_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ = eLpNorm f p μ

Tactic:
eLpNorm_congr_enorm_ae <| Eventually.of_forall fun _ => enorm_enorm _

Premises used: MeasureTheory.eLpNorm_congr_enorm_ae, Filter.Eventually.of_forall, enorm_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
simp_rw : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
simp_rw₁ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q) * q)
simp_rw₂ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
simp_rw₃ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
simp_rw₄ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))
simp_rw₅ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
simp_rw₆ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₇ : (∫⁻ (a : α), (‖f a‖ₑ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₈ : (∫⁻ (a : α), ‖f a‖ₑ ^ (q * p) ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q

Tactic:
simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div,
    mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm, mul_one, enorm_eq_self, ← ENNReal.rpow_mul, mul_comm]

Premises used: ENNReal.rpow_mul, MeasureTheory.eLpNorm', mul_assoc, Ne.symm, one_div, mul_comm, enorm_eq_self, mul_one, inv_mul_cancel₀, one_div_mul_one_div, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : α → ℝ
hf : ∀ᵐ (x : α) ∂μ, 0 ≤ f x
⊢ eLpNorm (ENNReal.ofReal ∘ f) p μ = eLpNorm f p μ

Tactic:
eLpNorm_congr_enorm_ae <| hf.mono fun _x hx ↦ Real.enorm_ofReal_of_nonneg hx

Premises used: MeasureTheory.eLpNorm_congr_enorm_ae, Filter.Eventually.mono, Real.enorm_ofReal_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
simp_rw : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
simp_rw₁ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q) * q)
simp_rw₂ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
simp_rw₃ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
simp_rw₄ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))
simp_rw₅ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
simp_rw₆ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₇ : (∫⁻ (a : α), ENNReal.ofReal ‖‖f a‖ ^ q‖ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₈ : (∫⁻ (a : α), ENNReal.ofReal |‖f a‖ ^ q| ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₉ : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₁₀ :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (q * p) ∂μ) ^ p⁻¹
simp_rw₁₁ :
  (∫⁻ (a : α), (ENNReal.ofReal ‖f a‖ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (q * p) ∂μ) ^ p⁻¹
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q

Tactic:
simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div,
    mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm, mul_one, ← ofReal_norm,
    Real.norm_eq_abs, abs_eq_self.mpr (Real.rpow_nonneg (norm_nonneg _) _), mul_comm p,
    ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ENNReal.rpow_mul]

Premises used: Iff.mpr, ENNReal.rpow_mul, MeasureTheory.eLpNorm', mul_assoc, ENNReal.ofReal_rpow_of_nonneg, LT.lt.le, Ne.symm, one_div, mul_comm, Real.rpow_nonneg, ofReal_norm, mul_one, abs_eq_self, inv_mul_cancel₀, norm_nonneg, one_div_mul_one_div, Real.norm_eq_abs, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
pos : ∀ (h0 : p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
neg : ∀ (h0 : ¬p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
by_cases h0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : p = 0
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
simp [h0, ENNReal.zero_rpow_of_pos hq_pos]

Premises used: ENNReal.zero_rpow_of_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
neg : ∀ (hp_top : ¬p = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
pos : essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) q
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
simp only [hp_top, eLpNorm_exponent_top, ENNReal.top_mul', hq_pos.not_ge,
      ENNReal.ofReal_eq_zero, if_false, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]

Premises used: MeasureTheory.eLpNorm_exponent_top, ENNReal.ofReal_eq_zero, if_false, MeasureTheory.eLpNormEssSup_eq_essSup_enorm, ENNReal.top_mul', LT.lt.not_ge
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ)

Tactic:
have h_rpow : essSup (‖‖f ·‖ₑ ^ q‖ₑ) μ = essSup (‖f ·‖ₑ ^ q) μ := by congr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ)
⊢ StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ q

Tactic:
have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hq_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ)
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ q
⊢ Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ q

Tactic:
have h_rpow_surj := (ENNReal.rpow_left_bijective hq_pos.ne.symm).2
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ)
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ q
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ q
iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ q) h_rpow_mono h_rpow_surj
⊢ essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ = HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) q

Tactic:
(iso.essSup_apply (fun x => ‖f x‖ₑ) μ).symm

Premises used: ENNReal.rpow, OrderIso.essSup_apply, ENorm.enorm, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ)
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ q
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ q
iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ q) h_rpow_mono h_rpow_surj
⊢ essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ = HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) q

Tactic:
exact (iso.essSup_apply (fun x => ‖f x‖ₑ) μ).symm

Premises used: OrderIso.essSup_apply, ENorm.enorm, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ p * ENNReal.ofReal q ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
neg : eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q
rw : p * ENNReal.ofReal q ≠ 0
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
rw [eLpNorm_eq_eLpNorm' h0 hp_top, eLpNorm_eq_eLpNorm' _ (by finiteness)]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ p * ENNReal.ofReal q ≠ 0

Tactic:
mul_ne_zero h0 ?_

Premises used: mul_ne_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
refine : ENNReal.ofReal q ≠ 0
⊢ p * ENNReal.ofReal q ≠ 0

Tactic:
refine mul_ne_zero h0 ?_

Premises used: mul_ne_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
rwa : ¬ENNReal.ofReal q = 0
rwa₁ : ¬q ≤ 0
rwa₂ rwa₃ rwa₄ rwa₅ : 0 < q
⊢ ENNReal.ofReal q ≠ 0

Tactic:
rwa [Ne, ENNReal.ofReal_eq_zero, not_le]

Premises used: not_le, ENNReal.ofReal_eq_zero, Ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
neg : eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p.toReal * q) μ ^ q
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q

Tactic:
rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal hq_pos.le]

Premises used: LT.lt.le, ENNReal.toReal_ofReal, ENNReal.toReal_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p.toReal * q) μ ^ q

Tactic:
eLpNorm'_enorm_rpow f p.toReal q hq_pos

Premises used: ENNReal.toReal, MeasureTheory.eLpNorm'_enorm_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p.toReal * q) μ ^ q

Tactic:
exact eLpNorm'_enorm_rpow f p.toReal q hq_pos

Premises used: ENNReal.toReal, MeasureTheory.eLpNorm'_enorm_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
rw : eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
rw [← eLpNorm_enorm_rpow f hq_pos]

Premises used: MeasureTheory.eLpNorm_enorm_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
symm : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
x : α
⊢ 0 ≤ ‖f x‖ ^ q

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ LE.le (α := ℝ) 0 ((fun (x : α) ↦ ‖f x‖ ^ q) x)) x} a
h₁ h₂ : ∀ (x : α), 0 ≤ ‖f x‖ ^ q
⊢ ∀ᵐ (x : α) ∂μ, LE.le (α := ℝ) 0 ((fun (x : α) ↦ ‖f x‖ ^ q) x)

Tactic:
filter_upwards with x using by positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h : ∀ (x : α), ‖f x‖ₑ ^ q = (ENNReal.ofReal ∘ fun (x : α) ↦ ‖f x‖ ^ q) x
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ

Tactic:
convert! eLpNorm_ofReal (fun x ↦ ‖f x‖ ^ q) (by filter_upwards with x using by positivity)

Premises used: Norm.norm, MeasureTheory.eLpNorm_ofReal, HPow.hPow
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
x : α
h : ENNReal.ofReal ‖f x‖ ^ q = ENNReal.ofReal (‖f x‖ ^ q)
⊢ ‖f x‖ₑ ^ q = (ENNReal.ofReal ∘ fun (x : α) ↦ ‖f x‖ ^ q) x

Tactic:
rw [Function.comp_apply, ← ofReal_norm]

Premises used: Function.comp_apply, ofReal_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
x : α
⊢ 0 ≤ ‖f x‖

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
x : α
⊢ 0 ≤ q

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
x : α
⊢ ENNReal.ofReal ‖f x‖ ^ q = ENNReal.ofReal (‖f x‖ ^ q)

Tactic:
exact ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)

Premises used: ENNReal.ofReal_rpow_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f g : α → ε
hfg : f =ᶠ[ae μ] g
⊢ eLpNorm f p μ = eLpNorm g p μ

Tactic:
eLpNorm_congr_enorm_ae <| hfg.mono fun _x hx => hx ▸ rfl

Premises used: MeasureTheory.eLpNorm_congr_enorm_ae, Eq.rec, Filter.Eventually.mono, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : TopologicalSpace ε
f g : α → ε
hfg : f =ᶠ[ae μ] g
⊢ MemLp f p μ ↔ MemLp g p μ

Tactic:
simp only [MemLp, eLpNorm_congr_ae hfg, aestronglyMeasurable_congr hfg]

Premises used: aestronglyMeasurable_congr, MeasureTheory.MemLp, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : TopologicalSpace ε
f g : α → ε
hfg : f =ᶠ[ae μ] g
hf_Lp : MemLp f p μ
⊢ MemLp g p μ

Tactic:
(memLp_congr_ae hfg).1 hf_Lp

Premises used: MeasureTheory.memLp_congr_ae, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
ε' : Type u_8
inst : TopologicalSpace ε
inst_1 : TopologicalSpace ε'
inst_2 : ContinuousENorm ε
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ eLpNorm g p μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : α → E
g : α → F
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
⊢ eLpNorm g p μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
g : α → ℝ≥0∞
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ g a
⊢ MemLp f p μ

Tactic:
MemLp.of_le_enorm hg hf <| h.mono fun _x hx ↦ le_trans hx le_rfl

Premises used: le_rfl, Filter.Eventually.mono, MeasureTheory.MemLp.of_le_enorm, le_trans
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a
⊢ MemLp f p μ

Tactic:
hg.of_le hf <| h.mono fun _x hx => le_trans hx (le_abs_self _)

Premises used: le_abs_self, MeasureTheory.MemLp.of_le, Filter.Eventually.mono, le_trans
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
ε' : Type u_8
inst : TopologicalSpace ε
inst_1 : TopologicalSpace ε'
inst_2 : ContinuousENorm ε
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
hf : MemLp f p μ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ
⊢ MemLp g p μ

Tactic:
hf.of_le_enorm hg <| EventuallyEq.le <| EventuallyEq.symm h

Premises used: Filter.EventuallyEq.le, MeasureTheory.MemLp.of_le_enorm, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : α → E
g : α → F
hf : MemLp f p μ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖
⊢ MemLp g p μ

Tactic:
hf.mono hg <| EventuallyEq.le <| EventuallyEq.symm h

Premises used: Filter.EventuallyEq.le, MeasureTheory.MemLp.mono, Filter.EventuallyEq.symm