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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
haefg' :
  ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
⊢ let f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯;
  UnifIntegrable f' p μ

Tactic:
set f' := fun n => (haef n).mk (μ := μ)

Premises used: MeasureTheory.AEStronglyMeasurable.mk
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
haefg' :
  ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
hui'₁ :
  let f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯;
  UnifIntegrable f' p μ
⊢ let f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯;
  UnifTight f' p μ

Tactic:
set f' := fun n => (haef n).mk (μ := μ)

Premises used: MeasureTheory.AEStronglyMeasurable.mk
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
haefg' :
  ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
⊢ let g' := AEStronglyMeasurable.mk g ⋯;
  StronglyMeasurable g'

Tactic:
set g' := hg'.aestronglyMeasurable.mk (μ := μ)

Premises used: MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.MemLp.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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
haefg' :
  ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
hg₁ :
  let g' := AEStronglyMeasurable.mk g ⋯;
  StronglyMeasurable g'
⊢ let g' := AEStronglyMeasurable.mk g ⋯;
  g =ᶠ[ae μ] g'

Tactic:
set g' := hg'.aestronglyMeasurable.mk (μ := μ)

Premises used: MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.MemLp.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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
haefg' :
  ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
hg₁ :
  let g' := AEStronglyMeasurable.mk g ⋯;
  StronglyMeasurable g'
hgg'₁ :
  let g' := AEStronglyMeasurable.mk g ⋯;
  g =ᶠ[ae μ] g'
⊢ let g' := AEStronglyMeasurable.mk g ⋯;
  MemLp g' p μ

Tactic:
set g' := hg'.aestronglyMeasurable.mk (μ := μ)

Premises used: MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.MemLp.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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
haefg' :
  ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
hg₁ :
  let g' := AEStronglyMeasurable.mk g ⋯;
  StronglyMeasurable g'
hgg'₁ :
  let g' := AEStronglyMeasurable.mk g ⋯;
  g =ᶠ[ae μ] g'
hg''₁ :
  let g' := AEStronglyMeasurable.mk g ⋯;
  MemLp g' p μ
⊢ let g' := AEStronglyMeasurable.mk g ⋯;
  ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))

Tactic:
set g' := hg'.aestronglyMeasurable.mk (μ := μ)

Premises used: MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.MemLp.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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
⊢ ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'

Tactic:
have haefg (n : ℕ) : f n - g =ᵐ[μ] f' n - g' := (hff' n).sub hgg'
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
⊢ ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (f' n - g') p μ

Tactic:
have hsnfg (n : ℕ) := eLpNorm_congr_ae (p := p) (haefg 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
hsnfg : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (f' n - g') p μ
apply : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f' n - g') p μ) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
apply Filter.Tendsto.congr (fun n => (hsnfg n).symm)

Premises used: Filter.Tendsto.congr, Eq.symm
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
hsnfg : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (f' n - g') p μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f' n - g') p μ) atTop (𝓝 0)

Tactic:
tendsto_Lp_of_tendsto_ae_of_meas hp hp' hf hg hg'' hui' hut' haefg'

Premises used: _private.0.MeasureTheory.tendsto_Lp_of_tendsto_ae_of_meas
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
hsnfg : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (f' n - g') p μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f' n - g') p μ) atTop (𝓝 0)

Tactic:
exact tendsto_Lp_of_tendsto_ae_of_meas hp hp' hf hg hg'' hui' hut' haefg'

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

Tactic:
tendsto_of_subseq_tendsto fun ns hns => ?_

Premises used: Filter.tendsto_of_subseq_tendsto
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
refine :
  ∀ (ns : ℕ → ℕ) (hns : Tendsto ns atTop atTop),
    ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_of_subseq_tendsto fun ns hns => ?_

Premises used: Filter.tendsto_of_subseq_tendsto
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
obtain :
  ∀ (ms : ℕ → ℕ),
    StrictMono ms →
      ∀ (hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ms i)) x) atTop (𝓝 (g x))),
        ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
⊢ ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns

Premises used: MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
⟨ms,
    tendsto_Lp_of_tendsto_ae hp hp' (fun _ => hf _) hg
      (fun ε hε => -- `UnifIntegrable` on a subsequence
        let ⟨δ, hδ, hδ'⟩ := hui hε
        ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
      (fun ε hε => -- `UnifTight` on a subsequence
        let ⟨s, hμs, hfε⟩ := hut hε
        ⟨s, hμs, fun i => hfε _⟩)
      hms'⟩

Premises used: MeasureTheory.tendsto_Lp_of_tendsto_ae, _private.0.MeasureTheory.tendsto_Lp_of_tendstoInMeasure.match_2, Exists, Ne, _private.0.MeasureTheory.tendsto_Lp_of_tendstoInMeasure.match_1, And, And.intro, Exists.intro, Top.top, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.UnifTight
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
exact ⟨ms,
    tendsto_Lp_of_tendsto_ae hp hp' (fun _ => hf _) hg
      (fun ε hε => -- `UnifIntegrable` on a subsequence
        let ⟨δ, hδ, hδ'⟩ := hui hε
        ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
      (fun ε hε => -- `UnifTight` on a subsequence
        let ⟨s, hμs, hfε⟩ := hut hε
        ⟨s, hμs, fun i => hfε _⟩)
      hms'⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UniformIntegrable f p μ
i : ι
⊢ AEStronglyMeasurable (f i) μ

Tactic:
hf.1 i

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UniformIntegrable f p μ
⊢ UnifIntegrable f p μ

Tactic:
hf.2.1

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UniformIntegrable f p μ
i : ι
⊢ MemLp (f i) p μ

Tactic:
⟨hf.1 i,
    let ⟨_, _, hC⟩ := hf.2
    lt_of_le_of_lt (hC i) ENNReal.coe_lt_top⟩

Premises used: lt_of_le_of_lt, MeasureTheory.MemLp, And.right, And.left, And.intro, LT.lt, Top.top, _private.0.MeasureTheory.UniformIntegrable.memLp.match_1, ENNReal.coe_lt_top, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
⊢ 0 < ε / 2

Tactic:
have hε2 : 0 < ε / 2 := half_pos hε
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
obtain :
  ∀ (δ₁ : ℝ) (hδ₁_pos : 0 < δ₁)
    (hfδ₁ :
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ₁, hδ₁_pos, hfδ₁⟩ := hf hε2
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
obtain :
  ∀ (δ₂ : ℝ) (hδ₂_pos : 0 < δ₂)
    (hgδ₂ :
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ₂, hδ₂_pos, hgδ₂⟩ := hg hε2
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
⟨min δ₁ δ₂, lt_min hδ₁_pos hδ₂_pos, fun i s hs hμs => ?_⟩

Premises used: lt_min, Exists.intro, Min.min
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
refine :
  ∀ (i : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (min δ₁ δ₂)),
    eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨min δ₁ δ₂, lt_min hδ₁_pos hδ₂_pos, fun i s hs hμs => ?_⟩