-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem Integrable.uniformIntegrable_condExp {ι : Type*} [IsFiniteMeasure μ] {g : α → ℝ}
    (hint : Integrable g μ) {ℱ : ι → MeasurableSpace α} (hℱ : ∀ i, ℱ i ≤ m0) :
    UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδ, h⟩ := hg.eLpNorm_indicator_le le_rfl ENNReal.one_ne_top hε

Result:
case neg.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε

Tactic:
by_cases hne : eLpNorm g 1 μ = 0

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : eLpNorm g 1 μ = 0
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε

case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε

Proof state:
case neg.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε

Tactic:
have hCpos : 0 < C := mul_pos (inv_pos.2 hδ) (ENNReal.toNNReal_pos hne hg.eLpNorm_lt_top.ne)

Result:
case neg.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : ↑C ^ ENNReal.toReal 1 * μ {x | ↑C ≤ ↑‖(μ[g|ℱ n]) x‖₊} ≤ eLpNorm (μ[g|ℱ n]) 1 μ ^ ENNReal.toReal 1
⊢ μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ

Tactic:
rw [ENNReal.one_toReal, ENNReal.rpow_one, ENNReal.rpow_one, mul_comm, ←
  ENNReal.le_div_iff_mul_le (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne'))
    (Or.inl ENNReal.coe_lt_top.ne)] at this

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | ↑C ≤ ↑‖(μ[g|ℱ n]) x‖₊} ≤ eLpNorm (μ[g|ℱ n]) 1 μ / ↑C
⊢ μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ eLpNorm (μ[g|ℱ n]) 1 μ / ↑C
⊢ μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ

Tactic:
refine this.trans ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ eLpNorm (μ[g|ℱ n]) 1 μ / ↑C
⊢ eLpNorm (μ[g|ℱ n]) 1 μ / ↑C ≤ ENNReal.ofReal δ