awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
inl :
  ∀ (hfC : ∀ᵐ (x : α) ∂0, ‖f x‖ₑ ≤ C),
    @eLpNorm _ _ _ m0 f p 0 ≤
      C • HPow.hPow (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have inr : ∀ (hμ : NeZero μ), eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have pos : ∀ (hp : p = 0), eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
pos : ∀ (hp : p = 0), eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have neg : ∀ (hp : ¬p = 0), eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
Tactic: have : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ := hfC.mono fun x hx ↦ hx.trans (le_refl C)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have neg : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ C) p μ =
  C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: refine (eLpNorm_mono_enorm_ae this).trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ C) p μ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have neg : ‖C‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) =
  C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: rw [eLpNorm_const _ hp (NeZero.ne μ), one_div, enorm_eq_self, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
neg :
  ‖C‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ C) p μ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have neg₁ : ‖C‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
  C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: rw [eLpNorm_const _ hp (NeZero.ne μ), one_div, enorm_eq_self, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
neg :
  ‖C‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
neg₁ :
  ‖C‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ C) p μ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have neg₂ : C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
  C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: rw [eLpNorm_const _ hp (NeZero.ne μ), one_div, enorm_eq_self, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
neg :
  ‖C‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
neg₁ :
  ‖C‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
neg₂ :
  C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ C) p μ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have neg₃ : C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
  C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: rw [eLpNorm_const _ hp (NeZero.ne μ), one_div, enorm_eq_self, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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 μ ≤ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal C
have rw : eLpNorm f p μ ≤ ENNReal.ofReal C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: rw [← mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₁ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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)
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₂ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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)
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₃ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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)
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₄ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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))
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₅ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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)
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₆ : (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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⁻¹
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₇ : (∫⁻ (a : α), (‖f a‖ₑ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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⁻¹
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₈ : (∫⁻ (a : α), ‖f a‖ₑ ^ (q * p) ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₁ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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)
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₂ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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)
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₃ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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)
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₄ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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))
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₅ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
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)
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₆ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
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]