-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem indicator (hf : UnifIntegrable f p μ) (E : Set α) :
    UnifIntegrable (fun i => E.indicator (f i)) p μ := fun ε hε ↦ by
  obtain ⟨δ, hδ_pos, hε⟩ := hf hε
  refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
  calc
    eLpNorm (s.indicator (E.indicator (f i))) p μ
      = eLpNorm (E.indicator (s.indicator (f i))) p μ

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε✝ : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hε :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun i => E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε✝ : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hε :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator ((fun i => E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε✝ : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hε :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator (E.indicator (f i))) p μ = eLpNorm (E.indicator (s.indicator (f i))) p μ

Tactic:
simp only [indicator_indicator, inter_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun i => E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδ_pos, hε⟩ := hf hε

Result:
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε✝ : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hε :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun i => E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε✝ : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hε :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator ((fun i => E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
calc
  eLpNorm (s.indicator (E.indicator (f i))) p μ
    = eLpNorm (E.indicator (s.indicator (f i))) p μ := by
    simp only [indicator_indicator, inter_comm]
  _ ≤ eLpNorm (s.indicator (f i)) p μ := eLpNorm_indicator_le _
  _ ≤ ENNReal.ofReal ε := hε _ _ hs hμs

Result:
no goals