-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.eLpNorm_indicator_le (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) (hf : MemLp f p μ) {ε : ℝ}
    (hε : 0 < ε) :
    ∃ (δ : ℝ) (_ : 0 < δ), ∀ s, MeasurableSet s → μ s ≤ ENNReal.ofReal δ →
      eLpNorm (s.indicator f) p μ ≤ 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 μ
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
have hℒp := hf

Result:
α : 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 μ
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator f) p μ = eLpNorm (s.indicator f') p μ

Tactic:
rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, eLpNorm_indicator_eq_eLpNorm_restrict hs]

Result:
case h.e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f' p (μ.restrict s)

Proof state:
case intro.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 ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
convert hδ s hs hμs using 1

Result:
case h.e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator f) p μ = eLpNorm (s.indicator f') p μ

Proof state:
case intro.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 ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨δ, hδpos, fun s hs hμs => ?_⟩

Result:
case intro.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 ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f' p (μ.restrict s)

Tactic:
exact eLpNorm_congr_ae heq.restrict

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδpos, hδ⟩ := (hℒp.ae_eq heq).eLpNorm_indicator_le_of_meas hp_one hp_top hf' hε

Result:
case intro.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 ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 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 μ
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨⟨f', hf', heq⟩, _⟩ := hf

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε