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

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x✝ x : α
hx : x ∈ {x | M ⊔ 1 ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}

Tactic:
rw [Set.mem_setOf_eq] at hx

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x✝ x : α
hx : M ⊔ 1 ≤ ↑‖f x‖₊
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}

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

Tactic:
refine Set.indicator_le_indicator_of_subset (fun x hx => ?_) (fun x => norm_nonneg (f x)) x

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x✝ x : α
hx : x ∈ {x | M ⊔ 1 ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}

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

Tactic:
obtain ⟨M, hM⟩ := hf.eLpNorm_indicator_norm_ge_le hmeas hε

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

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x✝ x : α
hx : M ⊔ 1 ≤ ↑‖f x‖₊
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}

Tactic:
exact (max_le_iff.1 hx).1

Result:
no goals

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

Tactic:
refine
  ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), le_trans (eLpNorm_mono fun x => ?_) hM⟩

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

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

Tactic:
rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ {x | M ⊔ 1 ≤ ↑‖f x‖₊}.indicator (fun a => ‖f a‖) x ≤ {x | M ≤ ↑‖f x‖₊}.indicator (fun a => ‖f a‖) x