-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem uniformIntegrable_of' [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞)
    (hf : ∀ i, StronglyMeasurable (f i))
    (h : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0,
      ∀ i, eLpNorm ({ x | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ ≤ ENNReal.ofReal ε) :
    UniformIntegrable f p μ

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ eLpNorm (f i) p μ ≤
    eLpNorm ({x | ‖f i x‖₊ < C}.indicator (f i)) p μ + eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ

Tactic:
refine le_trans (eLpNorm_mono fun x => ?_) (eLpNorm_add_le
  (StronglyMeasurable.aestronglyMeasurable
    ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
  (StronglyMeasurable.aestronglyMeasurable
    ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
⊢ ‖f i x‖ ≤ ‖({x | ‖f i x‖₊ < C}.indicator (f i) + {x | C ≤ ‖f i x‖₊}.indicator (f i)) x‖

Proof state:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : x ∉ {x | ‖f i x‖₊ < C}
⊢ ‖f i x‖ ≤ ‖0 + {x | C ≤ ‖f i x‖₊}.indicator (f i) x‖

Tactic:
rw [Set.indicator_of_mem, zero_add]

Result:
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : x ∉ {x | ‖f i x‖₊ < C}
⊢ x ∈ {x | C ≤ ‖f i x‖₊}

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ ↑C * μ univ ^ p.toReal⁻¹ + 1 ≠ ⊤

Tactic:
exact ENNReal.add_ne_top.2
  ⟨ENNReal.mul_ne_top ENNReal.coe_ne_top (ENNReal.rpow_ne_top_of_nonneg
    (inv_nonneg.2 ENNReal.toReal_nonneg) (measure_lt_top _ _).ne),
  ENNReal.one_ne_top⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
⊢ ‖f i x‖ ≤ ‖(if x ∈ {x | ‖f i x‖₊ < C} then f i x else 0) + {x | C ≤ ‖f i x‖₊}.indicator (f i) x‖

Tactic:
split_ifs with hx

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : x ∈ {x | ‖f i x‖₊ < C}
⊢ ‖f i x‖ ≤ ‖f i x + {x | C ≤ ‖f i x‖₊}.indicator (f i) x‖

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : x ∉ {x | ‖f i x‖₊ < C}
⊢ ‖f i x‖ ≤ ‖0 + {x | C ≤ ‖f i x‖₊}.indicator (f i) x‖

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
obtain ⟨C, hC⟩ := h 1 one_pos

Result:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C