-- 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 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:
conv_rhs => rw [← enorm_norm]

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

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
⊢ essSup (fun x => ‖f x‖ₑ ^ q) μ = essSup (fun x => ‖f x‖ₑ) μ ^ q

Tactic:
let iso := h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj

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) μ
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

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 μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
rw [eLpNorm_eq_eLpNorm' h0 hp_top, eLpNorm_eq_eLpNorm' _ _]

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 * 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 ≠ ⊤

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:
have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hq_pos

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) μ
h_rpow_mono : StrictMono fun x => 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 = ⊤
⊢ ENNReal.ofReal q ≠ 0

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

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
⊢ eLpNorm (fun x => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
by_cases h0 : p = 0

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
⊢ 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
⊢ eLpNorm (fun x => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ 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) μ
h_rpow_mono : StrictMono fun x => x ^ q
⊢ essSup (fun x => ‖f x‖ₑ ^ q) μ = essSup (fun x => ‖f x‖ₑ) μ ^ q

Tactic:
have h_rpow_surj := (ENNReal.rpow_left_bijective hq_pos.ne.symm).2

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) μ
h_rpow_mono : StrictMono fun x => x ^ q
h_rpow_surj : Function.Surjective fun y => y ^ q
⊢ 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
⊢ eLpNorm (fun x => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
simp [h0, ENNReal.zero_rpow_of_pos hq_pos]

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 = ⊤
⊢ essSup (fun x => ‖‖f x‖ ^ q‖ₑ) μ = essSup (fun x => ‖f x‖ₑ ^ q) μ

Tactic:
congr

Result:
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