awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
obtain :
  ∀ (n : ℕ) (hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨n, hn⟩ := Finite.exists_equiv_fin ι

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)
g : Fin n → α → β := f ∘ (⇑hn.some.symm : (a : Fin n) → ι)
⊢ ∀ (i : Fin n), MemLp (g i) p μ

Tactic:
have hg : ∀ i, MemLp (g i) p μ := fun _ => hf _
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)
g : Fin n → α → β := f ∘ (⇑hn.some.symm : (a : Fin n) → ι)
hg : ∀ (i : Fin n), MemLp (g i) p μ
obtain :
  ∀ (s : Set α) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨s, hμs, hfε⟩ := unifTight_fin hp_top hg hε

Premises used: _private.0.MeasureTheory.unifTight_fin
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)
g : Fin n → α → β := f ∘ (⇑hn.some.symm : (a : Fin n) → ι)
hg : ∀ (i : Fin n), MemLp (g i) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)
g : Fin n → α → β := f ∘ (⇑hn.some.symm : (a : Fin n) → ι)
hg : ∀ (i : Fin n), MemLp (g i) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
refine : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
refine ⟨s, hμs, fun i => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
inst_1 : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty.{u_3 + 1} (ι ≃ Fin n)
g : Fin n → α → β := f ∘ (⇑hn.some.symm : (a : Fin n) → ι)
hg : ∀ (i : Fin n), MemLp (g i) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ (↑ε : ℝ≥0∞)
i : ι
⊢ eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
simpa only [g, Function.comp_apply, Equiv.symm_apply_apply] using hfε (hn.some i)

Premises used: Equiv.symm_apply_apply, Nonempty.some, Function.comp_apply, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop (𝓝 0)
ε : ℝ≥0
hε : 0 < ε
rw :
  ∀ (hf_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε) ⦃ε : ℝ≥0⦄ (hε : 0 < ε),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
rw [ENNReal.tendsto_atTop_zero] at hf_tendsto

Premises used: ENNReal.tendsto_atTop_zero
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 < ε
⊢ (↑ε : ℝ≥0∞) > 0

Tactic:
simpa only [gt_iff_lt, ENNReal.coe_pos]

Premises used: ENNReal.coe_pos, gt_iff_lt
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 < ε
obtain :
  ∀ (N : ℕ) (hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ (↑ε : ℝ≥0∞)),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

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

Premises used: ENNReal.ofNNReal
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
⊢ ∀ (n : Fin N), MemLp (F n) p μ

Tactic:
have hF : ∀ n, MemLp (F n) p μ := fun n => hf n
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
obtain :
  ∀ (s : Set α) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)),
    ∃ (s : Set α),
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

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

Premises used: _private.0.MeasureTheory.unifTight_fin
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)
refine : ∀ (n : ℕ), eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
refine ⟨s, hμs, fun n => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)
n : ℕ
pos : ∀ (hn : n < N), eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)
neg : ∀ (hn : N ≤ n), eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
by_cases! hn : n < N
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)
n : ℕ
hn : n < N
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)

Tactic:
hFε ⟨n, hn⟩

Premises used: Fin.mk
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)
n : ℕ
hn : N ≤ n
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)

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

Premises used: MeasureTheory.eLpNorm_indicator_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : 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 μ ≤ (↑ε : ℝ≥0∞)
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ (↑ε : ℝ≥0∞)
n : ℕ
hn : N ≤ n
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ (↑ε : ℝ≥0∞)

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

Premises used: MeasureTheory.eLpNorm_indicator_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
h : ∀ (n : ℕ), f n = HAdd.hAdd (α := ℕ → α → β) (β := (n : ℕ) → α → β) (fun (x : ℕ) ↦ g) (fun (n : ℕ) ↦ f n - g) n
⊢ f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g

Tactic:
ext1 n
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
n : ℕ
⊢ f n = HAdd.hAdd (α := ℕ → α → β) (β := (n : ℕ) → α → β) (fun (x : ℕ) ↦ g) (fun (n : ℕ) ↦ f n - g) n

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
⊢ f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g

Tactic:
have : f = (fun _ => g) + fun n => f n - g := by ext1 n; simp
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
rw : UnifTight (HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g) p μ
⊢ UnifTight f p μ

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifTight (HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g) p μ

Tactic:
UnifTight.add ?_ ?_ (fun _ => hg.aestronglyMeasurable)
      fun n => (hf n).1.sub hg.aestronglyMeasurable

Premises used: MeasureTheory.UnifTight.add, MeasureTheory.AEStronglyMeasurable.sub, And.left, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
refine_1 : UnifTight.{u_1, u_2, 0} (β := β) (fun (x : ℕ) ↦ g) p μ
refine_2 : UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ f n - g) p μ
⊢ UnifTight (HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g) p μ

Tactic:
refine UnifTight.add ?_ ?_ (fun _ => hg.aestronglyMeasurable)
      fun n => (hf n).1.sub hg.aestronglyMeasurable

Premises used: MeasureTheory.UnifTight.add, MeasureTheory.AEStronglyMeasurable.sub, And.left, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifTight.{u_1, u_2, 0} (β := β) (fun (x : ℕ) ↦ g) p μ

Tactic:
unifTight_const hp' hg

Premises used: MeasureTheory.unifTight_const
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ f n - g) p μ

Tactic:
unifTight_of_tendsto_Lp_zero hp' (fun n => (hf n).sub hg) hfg

Premises used: _private.0.MeasureTheory.unifTight_of_tendsto_Lp_zero, MeasureTheory.MemLp.sub
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ f n - g) p μ

Tactic:
exact unifTight_of_tendsto_Lp_zero hp' (fun n => (hf n).sub hg) hfg

Premises used: _private.0.MeasureTheory.unifTight_of_tendsto_Lp_zero, MeasureTheory.MemLp.sub
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
rw : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
rw [ENNReal.tendsto_atTop_zero]

Premises used: ENNReal.tendsto_atTop_zero
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
pos : ∀ (hfinε : ε ≠ ∞), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
neg : ∀ (hfinε : ¬ε ≠ ∞), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
by_cases hfinε : ε ≠ ∞
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ¬ε ≠ ∞
neg : ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ∞
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
rw [not_ne_iff.mp hfinε]

Premises used: not_ne_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ¬ε ≠ ∞
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ∞

Tactic:
⟨0, fun n _ => le_top⟩

Premises used: le_top, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ¬ε ≠ ∞
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ∞

Tactic:
exact ⟨0, fun n _ => le_top⟩
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
pos :
  ∀ (hg' : MemLp (m0 := m) g p 0) (hui : @UnifIntegrable _ _ _ _ m f p 0) (hut : @UnifTight _ _ _ _ m f p 0)
    (hfg : ∀ᵐ (x : α) ∂0, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))),
    ∃ (N : ℕ), ∀ n ≥ N, @eLpNorm _ _ _ m (f n - g) p 0 ≤ ε
pos₁ : ∀ (hμ : μ ≠ 0), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
obtain rfl | hμ := eq_or_ne μ 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hg' : MemLp (m0 := m) g p 0
hui : @UnifIntegrable _ _ _ _ m f p 0
hut : @UnifTight _ _ _ _ m f p 0
hfg : ∀ᵐ (x : α) ∂0, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ ∃ (N : ℕ), ∀ n ≥ N, @eLpNorm _ _ _ m (f n - g) p 0 ≤ ε

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
⊢ 0 < ε / 3

Tactic:
have hε' : 0 < ε / 3 := ENNReal.div_pos hε.ne' (ofNat_ne_top)
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
pos :
  ∀ (Eg : Set α) (hmEg : MeasurableSet Eg) (hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
obtain ⟨Eg, hmEg, hμEg, hgε⟩ := MemLp.exists_eLpNorm_indicator_compl_lt hp' hg' hε'.ne'

Premises used: LT.lt.ne', MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt