-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem _root_.MeasurableEmbedding.eLpNorm_map_measure {g : β → F} (hf : MeasurableEmbedding f) :
    eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ⊤
⊢ (∫⁻ (a : α), ‖g (f a)‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by_cases hp_zero : p = 0

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by_cases hp : p = ∞

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ⊤
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ⊤
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp only [hp_zero, eLpNorm_exponent_zero]

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ⊤
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp_rw [eLpNorm_eq_lintegral_rpow_enorm hp_zero hp]

Result:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ⊤
⊢ (∫⁻ (x : β), ‖g x‖ₑ ^ p.toReal ∂Measure.map f μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ⊤
⊢ (∫⁻ (x : β), ‖g x‖ₑ ^ p.toReal ∂Measure.map f μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
rw [hf.lintegral_map]

Result:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ⊤
⊢ (∫⁻ (a : α), ‖g (f a)‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ⊤
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp_rw [hp, eLpNorm_exponent_top]

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ⊤
⊢ eLpNormEssSup g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → F
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ⊤
⊢ eLpNormEssSup g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Tactic:
exact hf.essSup_map_measure

Result:
no goals