-- 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.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
this : ∀ (n : ι), μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨C, fun n => le_trans ?_ (h {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} (hmeas n C) (this n))⟩

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
this : ∀ (n : ι), μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
n : ι
⊢ eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator (μ[g|ℱ n])) 1 μ ≤ eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator g) 1 μ

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‖₊}
⊢ UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ

Tactic:
have hg : MemLp g 1 μ := memLp_one_iff_integrable.2 hint

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 μ
⊢ UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ

Proof state:
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 : g =ᶠ[ae μ] 0
n : ι
⊢ {x | 0 ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator (μ[g|ℱ n]) =ᶠ[ae μ] 0

Tactic:
filter_upwards [condExp_congr_ae (m := ℱ n) hne] with x hx

Result:
case h
α : 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 : g =ᶠ[ae μ] 0
n : ι
x : α
hx : (μ[g|ℱ n]) x = (μ[0|ℱ n]) x
⊢ {x | 0 ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator (μ[g|ℱ n]) x = 0 x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
⊢ UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ

Tactic:
let A : MeasurableSpace α := m0

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
⊢ UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ

Proof state:
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 : g =ᶠ[ae μ] 0
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨0, fun n => (le_of_eq <|
  (eLpNorm_eq_zero_iff ((stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable.indicator
    (hmeas n 0)) one_ne_zero).2 ?_).trans (zero_le _)⟩

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 : g =ᶠ[ae μ] 0
n : ι
⊢ {x | 0 ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator (μ[g|ℱ n]) =ᶠ[ae μ] 0

Proof state:
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 ε

Tactic:
rw [eLpNorm_eq_zero_iff hg.1 one_ne_zero] at hne

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 : g =ᶠ[ae μ] 0
⊢ ∃ 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 : ι), μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ

Tactic:
intro n

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 : ι
⊢ μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ