-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.eLpNorm_indicator_le' (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) (hf : MemLp f p μ)
    (hmeas : StronglyMeasurable f) {ε : ℝ} (hε : 0 < ε) :
    ∃ (δ : ℝ) (_ : 0 < δ), ∀ s, MeasurableSet s → μ s ≤ ENNReal.ofReal δ →
      eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.104230 s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.104230 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f + {x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤ 2 * ENNReal.ofReal ε

Tactic:
refine le_trans (eLpNorm_add_le ?_ ?_ hp_one) ?_

Result:
case intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.104230 s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.104230 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ AEStronglyMeasurable ({x | M ≤ ↑‖f x‖₊}.indicator f) (μ.restrict s)

case intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.104230 s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.104230 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ AEStronglyMeasurable ({x | ‖f x‖ < M}.indicator f) (μ.restrict s)

case intro.intro.intro.intro.refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.104230 s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.104230 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p (μ.restrict s) + eLpNorm ({x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤
    2 * ENNReal.ofReal ε

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ (if x ∈ {x | ‖f x‖ < M} then ‖f x‖ else 0) < ?m.104517

Tactic:
split_ifs with h

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

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x : α
h : x ∉ {x | ‖f x‖ < M}
⊢ 0 < ?m.104517

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

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x : α
h : x ∉ {x | ‖f x‖ < M}
⊢ 0 < ?m.104517

Tactic:
exacts [h, hMpos]

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.104230 s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.104230 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p (μ.restrict s) + eLpNorm ({x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤
    2 * ENNReal.ofReal ε

Tactic:
rw [two_mul]

Result:
case intro.intro.intro.intro.refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.104230 s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.104230 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p (μ.restrict s) + eLpNorm ({x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤
    ENNReal.ofReal ε + ENNReal.ofReal ε

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.104230 s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.104230 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ AEStronglyMeasurable ({x | M ≤ ↑‖f x‖₊}.indicator f) (μ.restrict s)

Tactic:
exact StronglyMeasurable.aestronglyMeasurable
  (hmeas.indicator (measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe))

Result:
no goals