-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem unifTight_of_tendsto_Lp_zero (hp' : p ≠ ∞) (hf : ∀ n, MemLp (f n) p μ)
    (hf_tendsto : Tendsto (fun n ↦ eLpNorm (f n) p μ) atTop (𝓝 0)) : UnifTight f p μ := fun ε hε ↦by
  rw [ENNReal.tendsto_atTop_zero] at hf_tendsto
  obtain ⟨N, hNε⟩ := hf_tendsto ε (by simpa only [gt_iff_lt, ENNReal.coe_pos])
  let F : Fin N → α → β := fun n => f n
  have hF : ∀ n, MemLp (F n) p μ := fun n => hf n
  obtain ⟨s, hμs, hFε⟩ := unifTight_fin hp' hF hε
  refine ⟨s, hμs, fun n => ?_⟩
  by_cases hn : n < N
  · exact hFε ⟨n, hn⟩
  · exact (eLpNorm_indicator_le _).trans (hNε n (not_lt.mp hn))

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ⊤
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
n : ℕ
hn : n < N
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ ↑ε

Tactic:
exact hFε ⟨n, hn⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
have hF : ∀ n, MemLp (F n) p μ := fun n => hf n

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
obtain ⟨s, hμs, hFε⟩ := unifTight_fin hp' hF hε

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ⊤
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
let F : Fin N → α → β := fun n => f n

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ⊤
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
n : ℕ
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ ↑ε

Tactic:
by_cases hn : n < N

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ⊤
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
n : ℕ
hn : n < N
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ ↑ε

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ⊤
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
n : ℕ
hn : ¬n < N
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ ↑ε

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ⊤
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
n : ℕ
hn : ¬n < N
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ ↑ε

Tactic:
exact (eLpNorm_indicator_le _).trans (hNε n (not_lt.mp hn))

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ⊤
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
refine ⟨s, hμs, fun n => ?_⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ⊤
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
n : ℕ
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ ↑ε

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
obtain ⟨N, hNε⟩ := hf_tendsto ε (by simpa only [gt_iff_lt, ENNReal.coe_pos])

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε