-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_indicator_eq_eLpNorm_restrict (hs : MeasurableSet s) :
    eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

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
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : p = 0
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
simp_rw [eLpNorm_eq_lintegral_rpow_enorm hp_zero hp_top]

Result:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α) in s, ‖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
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
suffices (∫⁻ x, (‖s.indicator f x‖ₑ) ^ p.toReal ∂μ) =
    ∫⁻ x in s, ‖f x‖ₑ ^ p.toReal ∂μ by rw [this]

Result:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ ∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ = ∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ ∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : α), s.indicator (fun x => ‖f x‖ₑ ^ p.toReal) a ∂μ

Tactic:
congr

Result:
case neg.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (fun x => ‖s.indicator f x‖ₑ ^ p.toReal) = fun a => s.indicator (fun x => ‖f x‖ₑ ^ p.toReal) a

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : p = 0
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
simp only [hp_zero, eLpNorm_exponent_zero]

Result:
no goals

Proof state:
case neg.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (fun x => ‖s.indicator f x‖ₑ ^ p.toReal) = fun a => s.indicator (fun x => ‖f x‖ₑ ^ p.toReal) a

Tactic:
simp_rw [enorm_indicator_eq_indicator_enorm]

Result:
case neg.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (fun x => s.indicator (fun a => ‖f a‖ₑ) x ^ p.toReal) = fun a => s.indicator (fun x => ‖f x‖ₑ ^ p.toReal) a

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
this : ∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ = ∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
rw [this]

Result:
no goals

Proof state:
case neg.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ 0 ^ p.toReal = 0

Tactic:
simp [ENNReal.toReal_pos hp_zero hp_top]

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ ∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ = ∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
rw [← lintegral_indicator hs]

Result:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ ∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : α), s.indicator (fun x => ‖f x‖ₑ ^ p.toReal) a ∂μ

Proof state:
case neg.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (fun x => s.indicator (fun a => ‖f a‖ₑ) x ^ p.toReal) = fun a => s.indicator (fun x => ‖f x‖ₑ ^ p.toReal) a

Tactic:
rw [eq_comm, ← Function.comp_def (fun x : ℝ≥0∞ => x ^ p.toReal), Set.indicator_comp_of_zero,
  Function.comp_def]

Result:
case neg.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ 0 ^ p.toReal = 0

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
simp_rw [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm,
   enorm_indicator_eq_indicator_enorm, ENNReal.essSup_indicator_eq_essSup_restrict hs]

Result:
no goals