-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem unifTight_const {g : α → β} (hp_ne_top : p ≠ ∞) (hg : MemLp g p μ) :
    UnifTight (fun _ : ι => g) p μ

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε

Tactic:
by_cases hε_top : ε = ∞

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ↑ε = ⊤
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ⊤
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε

Proof state:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ⊤
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε

Tactic:
obtain ⟨s, _, hμs, hgε⟩ := hg.exists_eLpNorm_indicator_compl_lt hp_ne_top (coe_ne_zero.mpr hε.ne')

Result:
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ⊤
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hgε : eLpNorm (sᶜ.indicator g) p μ < ↑ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ↑ε = ⊤
⊢ μ ∅ ≠ ⊤

Tactic:
measurability

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ↑ε = ⊤
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε

Tactic:
exact ⟨∅, (by measurability), fun _ => hε_top.symm ▸ le_top⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
⊢ UnifTight (fun x => g) p μ

Tactic:
intro ε hε

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε

Proof state:
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ⊤
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ⊤
hgε : eLpNorm (sᶜ.indicator g) p μ < ↑ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε

Tactic:
exact ⟨s, ne_of_lt hμs, fun _ => hgε.le⟩

Result:
no goals