-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem MemLp.exists_eLpNorm_indicator_compl_lt {β : Type*} [NormedAddCommGroup β] (hp_top : p ≠ ∞)
    {f : α → β} (hf : MemLp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ s : Set α, MeasurableSet s ∧ μ s < ∞ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
f : α → β
ε : ℝ≥0∞
hε : ε ≠ 0
hp_top : 0 ≠ ⊤
hf : MemLp f 0 μ
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) 0 μ < ε

Tactic:
use ∅

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
f : α → β
ε : ℝ≥0∞
hε : ε ≠ 0
hp_top : 0 ≠ ⊤
hf : MemLp f 0 μ
⊢ MeasurableSet ∅ ∧ μ ∅ < ⊤ ∧ eLpNorm (∅ᶜ.indicator f) 0 μ < ε

Proof state:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε✝ : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : μ s < ⊤
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
refine ⟨s, hsm, hs, ?_⟩

Result:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε✝ : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : μ s < ⊤
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ eLpNorm (sᶜ.indicator f) p μ < ε

Proof state:
case hε
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ε ^ p.toReal ≠ 0

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal

Tactic:
apply exists_setLintegral_compl_lt

Result:
case hf
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ⊤

case hε
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ε ^ p.toReal ≠ 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
rcases eq_or_ne p 0 with rfl | hp₀

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
f : α → β
ε : ℝ≥0∞
hε : ε ≠ 0
hp_top : 0 ≠ ⊤
hf : MemLp f 0 μ
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) 0 μ < ε

case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Proof state:
case hf
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ⊤

Tactic:
exact ((eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp_top).1 hf.2).ne

Result:
no goals

Proof state:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε✝ : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : μ s < ⊤
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ 0 < p.toReal

Tactic:
simp [ENNReal.toReal_pos, *]

Result:
no goals

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
f : α → β
ε : ℝ≥0∞
hε : ε ≠ 0
hp_top : 0 ≠ ⊤
hf : MemLp f 0 μ
⊢ MeasurableSet ∅ ∧ μ ∅ < ⊤ ∧ eLpNorm (∅ᶜ.indicator f) 0 μ < ε

Tactic:
simp [pos_iff_ne_zero.2 hε]

Result:
no goals

Proof state:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε✝ : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : μ s < ⊤
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
rwa [eLpNorm_indicator_eq_eLpNorm_restrict hsm.compl,
  eLpNorm_eq_lintegral_rpow_enorm hp₀ hp_top, one_div, ENNReal.rpow_inv_lt_iff]

Result:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_6
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ⊤
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε✝ : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : μ s < ⊤
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ 0 < p.toReal