-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_norm_rpow (f : α → F) (hq_pos : 0 < q) :
    eLpNorm (fun x => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm' (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]

Result:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm' (fun x => ‖f x‖ ^ q) p.toReal μ = eLpNorm' f (p.toReal * q) μ ^ q

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
⊢ eLpNorm (fun x => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm (fun x => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm (fun x => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm' (fun x => ‖f x‖ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q

α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ 0

α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤

Tactic:
swap

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ 0

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm' (fun x => ‖f x‖ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q

α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm' (fun x => ‖f x‖ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q

α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤

Tactic:
swap

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm' (fun x => ‖f x‖ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm (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_le,
  ENNReal.ofReal_eq_zero, if_false, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ essSup (fun x => ‖‖f x‖ ^ q‖ₑ) μ = essSup (fun x => ‖f x‖ₑ) μ ^ q

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ‖‖f x‖ ^ q‖ₑ) μ = essSup (fun x => ‖f x‖ₑ ^ q) μ
⊢ essSup (fun x => ‖‖f x‖ ^ q‖ₑ) μ = essSup (fun x => ‖f x‖ₑ) μ ^ q

Tactic:
rw [h_rpow]

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ‖‖f x‖ ^ q‖ₑ) μ = essSup (fun x => ‖f x‖ₑ ^ q) μ
⊢ essSup (fun x => ‖f x‖ₑ ^ q) μ = essSup (fun x => ‖f x‖ₑ) μ ^ q

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤

Tactic:
exact ENNReal.mul_ne_top hp_top ENNReal.ofReal_ne_top

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ 0

Tactic:
refine mul_ne_zero h0 ?_

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ ENNReal.ofReal q ≠ 0

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ‖‖f x‖ ^ q‖ₑ) μ = essSup (fun x => ‖f x‖ₑ ^ q) μ
h_rpow_mono : StrictMono fun x => x ^ q
h_rpow_surj : Function.Surjective fun y => y ^ q
iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun x => x ^ q) h_rpow_mono h_rpow_surj
⊢ essSup (fun x => ‖f x‖ₑ ^ q) μ = essSup (fun x => ‖f x‖ₑ) μ ^ q

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

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm' (fun x => ‖f x‖ ^ q) p.toReal μ = eLpNorm' f (p.toReal * q) μ ^ q

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

Result:
no goals

Proof state:
case e_f.h
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ‖‖f x‖ ^ q‖ₑ = ‖‖f x‖‖ₑ ^ q

Tactic:
rw [← Real.enorm_rpow_of_nonneg (norm_nonneg _) hq_pos.le]

Result:
no goals

Proof state:
case e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ (fun x => ‖‖f x‖ ^ q‖ₑ) = fun x => ‖f x‖ₑ ^ q

Tactic:
ext1 x

Result:
case e_f.h
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ‖‖f x‖ ^ q‖ₑ = ‖f x‖ₑ ^ q