-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.eLpNorm_indicator_norm_ge_le (hf : MemLp f p μ) (hmeas : StronglyMeasurable f) {ε : ℝ}
    (hε : 0 < ε) : ∃ M : ℝ, eLpNorm ({ x | M ≤ ‖f x‖₊ }.indicator f) p μ ≤ ENNReal.ofReal ε

Proof state:
case neg.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨M ^ (1 / p.toReal), ?_⟩

Result:
case neg.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
⊢ eLpNorm ({x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
by_cases hp_ne_top : p = ∞

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : p = ⊤
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∈ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator (fun a => ‖f a‖ₑ) x ^ p.toReal =
    {x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun a => ‖‖f a‖ ^ p.toReal‖ₑ) x

Tactic:
rw [Set.indicator_of_mem hx, Set.indicator_of_mem, Real.enorm_of_nonneg (by positivity),
  ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) ENNReal.toReal_nonneg, ofReal_norm]

Result:
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∈ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : p = ⊤
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
subst hp_ne_top

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : MemLp f ⊤ μ
hp_ne_zero : ¬⊤ = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) ⊤ μ ≤ ENNReal.ofReal ε

Proof state:
case neg.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
⊢ ∫⁻ (x : α), ‖{x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator f x‖ₑ ^ p.toReal ∂μ ≤ ENNReal.ofReal (ε ^ p.toReal)

Tactic:
convert hM using 3 with x

Result:
case h.e'_3.h.e'_4.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
⊢ ‖{x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator f x‖ₑ ^ p.toReal =
    ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ

Proof state:
case pos.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : MemLp f ⊤ μ
hp_ne_zero : ¬⊤ = 0
M : ℝ
hM : eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) ⊤ μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨M, ?_⟩

Result:
case pos.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : MemLp f ⊤ μ
hp_ne_zero : ¬⊤ = 0
M : ℝ
hM : eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0
⊢ eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) ⊤ μ ≤ ENNReal.ofReal ε

Proof state:
case h.e'_3.h.e'_4.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
⊢ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator (fun a => ‖f a‖ₑ) x ^ p.toReal =
    {x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun a => ‖‖f a‖ ^ p.toReal‖ₑ) x

Tactic:
by_cases hx : x ∈ { x : α | M ^ (1 / p.toReal) ≤ ‖f x‖₊ }

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∈ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator (fun a => ‖f a‖ₑ) x ^ p.toReal =
    {x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun a => ‖‖f a‖ ^ p.toReal‖ₑ) x

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∉ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator (fun a => ‖f a‖ₑ) x ^ p.toReal =
    {x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun a => ‖‖f a‖ ^ p.toReal‖ₑ) x