awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
pos :
  ∀ (Ef : Set α) (hmEf : MeasurableSet Ef) (hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
obtain ⟨Ef, hmEf, hμEf, hfε⟩ := hut.exists_measurableSet_indicator hε'.ne'

Premises used: LT.lt.ne', MeasureTheory.UnifTight.exists_measurableSet_indicator
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
⊢ MeasurableSet (Ef ∪ Eg)

Tactic:
have hmE := hmEf.union hmEg
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
hmE : MeasurableSet (Ef ∪ Eg)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ef ∪ Eg) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hfmE := (measure_union_le Ef Eg).trans_lt (add_lt_top.mpr ⟨hμEf, hμEg⟩)
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
hmE : MeasurableSet (Ef ∪ Eg)
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ef ∪ Eg) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ let E := Ef ∪ Eg;
  MeasurableSet E

Tactic:
set E : Set α := Ef ∪ Eg

Premises used: Set
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
hmE : MeasurableSet (Ef ∪ Eg)
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ef ∪ Eg) : ℝ≥0∞) (∞ : ℝ≥0∞)
hmE₁ :
  let E := Ef ∪ Eg;
  MeasurableSet E
⊢ let E := Ef ∪ Eg;
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
set E : Set α := Ef ∪ Eg

Premises used: Set
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ MemLp g p (μ.restrict E)

Tactic:
have hgE' := MemLp.restrict E hg'
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
⊢ UnifIntegrable f p (μ.restrict E)

Tactic:
have huiE := hui.restrict E
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
⊢ ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))

Tactic:
have hfgE : (∀ᵐ x ∂(μ.restrict E), Tendsto (fun n => f n x) atTop (𝓝 (g x))) :=
    ae_restrict_of_ae hfg
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have ffmE := Fact.mk hfmE
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p (μ.restrict E)) atTop (𝓝 0)

Tactic:
have hInner := tendsto_Lp_finite_of_tendsto_ae_of_meas hp hp' hf hg hgE' huiE hfgE
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p (μ.restrict E)) atTop (𝓝 0)
⊢ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε

Tactic:
rw [ENNReal.tendsto_atTop_zero] at hInner

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
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
pos :
  ∀ (N : ℕ) (hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
obtain ⟨N, hfngε⟩ := hInner (ε / 3) hε'

Premises used: HDiv.hDiv, 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ε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
h : ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
use N
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
⊢ AEStronglyMeasurable (E.indicator (f n - g)) μ

Tactic:
have hmfngE : AEStronglyMeasurable _ μ := (((hf n).sub hg).indicator hmE).aestronglyMeasurable
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
⊢ eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3

Tactic:
have hfngEε := calc
    eLpNorm (E.indicator (f n - g)) p μ
      = eLpNorm (f n - g) p (μ.restrict E) := eLpNorm_indicator_eq_eLpNorm_restrict hmE
    _ ≤ ε / 3                              := hfngε n hn
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
⊢ AEStronglyMeasurable (Eᶜ.indicator g) μ

Tactic:
have hmgEc : AEStronglyMeasurable _ μ := (hg.indicator hmE.compl).aestronglyMeasurable
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
unfold : eLpNorm ((Ef ∪ Eg)ᶜ.indicator g) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ
⊢ eLpNorm (Eᶜ.indicator g) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ

Tactic:
unfold E
-- 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
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
rw : eLpNorm ((Efᶜ ∩ Egᶜ).indicator g) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ
rw₁ rw₂ : eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ
⊢ eLpNorm ((Ef ∪ Eg)ᶜ.indicator g) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ

Tactic:
rw [compl_union, ← indicator_indicator]

Premises used: Set.compl_union, Set.indicator_indicator