awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
refine_3 :
  ∀ (C : ℝ≥0) (hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)),
    ∃ (C : ℝ≥0),
      ∀ (i : ℕ),
        eLpNorm.{u_1, u_4} (ε := E)
            ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i) p μ ≤
          (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E)
          ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i) p μ ≤
        (↑C : ℝ≥0∞)

Tactic:
obtain ⟨C, hC⟩ := hf₃
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
refine_3 :
  ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E) (∑ x ∈ Finset.range i, HSMul.hSMul (α := ℝ) (↑i : ℝ)⁻¹ (f x)) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E)
          ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i) p μ ≤
        (↑C : ℝ≥0∞)

Tactic:
simp_rw [Finset.smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E) (∑ x ∈ Finset.range i, HSMul.hSMul (α := ℝ) (↑i : ℝ)⁻¹ (f x)) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
⟨C, fun n => (eLpNorm_sum_le (fun i _ => (hf₁ i).const_smul _) hp).trans ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul, Nat.cast, Inv.inv, Exists.intro, LE.le.trans, MeasureTheory.eLpNorm_sum_le
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
refine_3 : ∀ (n : ℕ), ∑ i ∈ Finset.range n, eLpNorm (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E) (∑ x ∈ Finset.range i, HSMul.hSMul (α := ℝ) (↑i : ℝ)⁻¹ (f x)) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
refine ⟨C, fun n => (eLpNorm_sum_le (fun i _ => (hf₁ i).const_smul _) hp).trans ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
refine_3 : ∑ i ∈ Finset.range 0, eLpNorm (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
refine_3₁ : ∀ (hn : n ≠ 0), ∑ i ∈ Finset.range n, eLpNorm (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range n, eLpNorm (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range 0, eLpNorm (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
hn : n ≠ 0
refine_3 : enorm (E := ℝ) (↑n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range n, eLpNorm (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
simp_rw [eLpNorm_const_smul, ← Finset.mul_sum]

Premises used: Finset.mul_sum, MeasureTheory.eLpNorm_const_smul
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
hn : n ≠ 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
hn : n ≠ 0
refine_3 : HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (f i) p μ) (↑n : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
⊢ enorm (E := ℝ) (↑n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
rw [enorm_inv (by positivity), Real.enorm_natCast, ← ENNReal.div_eq_inv_mul]

Premises used: Real.enorm_natCast, enorm_inv, ENNReal.div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
hn : n ≠ 0
⊢ HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (f i) p μ) (↑n : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)

Tactic:
ENNReal.div_le_of_le_mul' ?_

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
hn : n ≠ 0
refine_3 : ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ (↑n : ℝ≥0∞) * (↑C : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (f i) p μ) (↑n : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)

Tactic:
refine ENNReal.div_le_of_le_mul' ?_

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ (↑n : ℝ≥0∞) * (↑C : ℝ≥0∞)

Tactic:
simpa using Finset.sum_le_card_nsmul (.range n) _ _ fun i _ => hC i

Premises used: Finset.range, Finset.sum_le_card_nsmul
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
⊢ UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) p
    μ

Tactic:
uniformIntegrable_average hp hf

Premises used: MeasureTheory.uniformIntegrable_average
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
h :
  ∀ (n : ℕ),
    HDiv.hDiv (α := α → ℝ) (∑ i ∈ Finset.range n, f i) (↑n : α → ℝ) =
      HSMul.hSMul (α := ℝ) (β := α → ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)
⊢ UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := α → ℝ) (∑ i ∈ Finset.range n, f i) (↑n : α → ℝ)) p μ

Tactic:
convert! uniformIntegrable_average hp hf using 2 with n

Premises used: MeasureTheory.uniformIntegrable_average
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
n : ℕ
h :
  ∀ (x : α),
    HDiv.hDiv (α := α → ℝ) (β := α → ℝ) (∑ i ∈ Finset.range n, f i) (↑n : α → ℝ) x =
      HSMul.hSMul (α := ℝ) (β := α → ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i) x
⊢ HDiv.hDiv (α := α → ℝ) (∑ i ∈ Finset.range n, f i) (↑n : α → ℝ) =
    HSMul.hSMul (α := ℝ) (β := α → ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
n : ℕ
x : α
⊢ HDiv.hDiv (α := α → ℝ) (β := α → ℝ) (∑ i ∈ Finset.range n, f i) (↑n : α → ℝ) x =
    HSMul.hSMul (α := ℝ) (β := α → ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i) x

Tactic:
simp [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
⊢ UniformIntegrable (β := β)
    (fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦ (↑f : α → β)) p
    μ

Tactic:
⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_tendstoInMeasure u (fun i => hUI.1 i), ?_⟩

Premises used: MeasureTheory.UniformIntegrable, MeasureTheory.UnifIntegrable.unifIntegrable_of_tendstoInMeasure, _private.0.MeasureTheory.UnifIntegrable.unifIntegrable_of_tendstoInMeasure.match_1, And.right, And.left, And.intro, Subtype.val, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
refine_1 :
  ∀ (x : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (f : α → β) (s : κ → ι)
    (hs : TendstoInMeasure μ (fn ∘ s) u f),
    AEStronglyMeasurable.{u_1, u_2} (β := β)
      ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦ (↑f : α → β))
        (Subtype.mk (p := fun (x : α → β) ↦
          Membership.mem (γ := Set (α → β)) {g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} x) f ⋯))
      μ
refine_2 :
  ∃ (C : ℝ≥0),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)
⊢ UniformIntegrable (β := β)
    (fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦ (↑f : α → β)) p
    μ

Tactic:
refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_tendstoInMeasure u (fun i => hUI.1 i), ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
x : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))
f : α → β
s : κ → ι
hs : TendstoInMeasure μ (fn ∘ s) u f
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β)
    ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦ (↑f : α → β))
      (Subtype.mk (p := fun (x : α → β) ↦
        Membership.mem (γ := Set (α → β)) {g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} x) f ⋯))
    μ

Tactic:
hs.aestronglyMeasurable (fun n => hUI.1 (s n))

Premises used: And.left, MeasureTheory.TendstoInMeasure.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
x : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))
f : α → β
s : κ → ι
hs : TendstoInMeasure μ (fn ∘ s) u f
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β)
    ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦ (↑f : α → β))
      (Subtype.mk (p := fun (x : α → β) ↦
        Membership.mem (γ := Set (α → β)) {g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} x) f ⋯))
    μ

Tactic:
exact hs.aestronglyMeasurable (fun n => hUI.1 (s n))

Premises used: And.left, MeasureTheory.TendstoInMeasure.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
refine_2 :
  ∀ (C : ℝ≥0) (hC : ∀ (i : ι), eLpNorm (fn i) p μ ≤ (↑C : ℝ≥0∞)),
    ∃ (C : ℝ≥0),
      ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))),
        eLpNorm.{u_1, u_2} (ε := β)
            ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
                (↑f : α → β))
              i)
            p μ ≤
          (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)

Tactic:
obtain ⟨C, hC⟩ := hUI.2.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (fn i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)

Tactic:
⟨C, fun ⟨f, s, hs⟩ => eLpNorm_le_of_tendstoInMeasure
      (Eventually.of_forall fun n => hC (s n)) hs (fun n => hUI.1 (s n))⟩

Premises used: ENNReal.ofNNReal, Filter.Eventually.of_forall, LE.le, MeasureTheory.eLpNorm_le_of_tendstoInMeasure, _private.0.MeasureTheory.UnifIntegrable.unifIntegrable_of_tendstoInMeasure.match_1, And.left, Exists.intro, Subtype.val, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (fn i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)

Tactic:
exact ⟨C, fun ⟨f, s, hs⟩ => eLpNorm_le_of_tendstoInMeasure
      (Eventually.of_forall fun n => hC (s n)) hs (fun n => hUI.1 (s n))⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : κ → α → β
g : α → β
hUI : UniformIntegrable f p μ
htends : TendstoInMeasure μ f u g
⊢ MemLp g p μ

Tactic:
simpa using (hUI.uniformIntegrable_of_tendstoInMeasure u).memLp ⟨g, ⟨fun n => n, htends⟩⟩

Premises used: MeasureTheory.UniformIntegrable.uniformIntegrable_of_tendstoInMeasure, Subtype.mk, MeasureTheory.UniformIntegrable.memLp, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : κ → α → β
g : α → β
hUI : UniformIntegrable f 1 μ
htends : TendstoInMeasure μ f u g
⊢ Integrable g μ

Tactic:
memLp_one_iff_integrable.mp (hUI.memLp_of_tendstoInMeasure htends)

Premises used: MeasureTheory.UniformIntegrable.memLp_of_tendstoInMeasure, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
⊢ UniformIntegrable (β := β)
    (fun
        (f :
          (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
            Type (max u_1 u_2))) ↦
      (↑f : α → β))
    p μ

Tactic:
⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_ae_tendsto u (fun i => hUI.1 i), ?_⟩

Premises used: MeasureTheory.UniformIntegrable, MeasureTheory.UnifIntegrable.unifIntegrable_of_ae_tendsto, And.right, And.left, And.intro, _private.0.MeasureTheory.UnifIntegrable.unifIntegrable_of_ae_tendsto.match_1, Subtype.val, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
refine_1 :
  ∀
    (x :
      (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
        Type (max u_1 u_2)))
    (f : α → β) (s : κ → ι) (hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))),
    AEStronglyMeasurable.{u_1, u_2} (β := β)
      ((fun
            (f :
              (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                Type (max u_1 u_2))) ↦
          (↑f : α → β))
        (Subtype.mk (p := fun (x : α → β) ↦
          Membership.mem (γ := Set (α → β))
            {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
          f ⋯))
      μ
refine_2 :
  ∃ (C : ℝ≥0),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun
                (f :
                  (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                    Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)
⊢ UniformIntegrable (β := β)
    (fun
        (f :
          (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
            Type (max u_1 u_2))) ↦
      (↑f : α → β))
    p μ

Tactic:
refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_ae_tendsto u (fun i => hUI.1 i), ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β)
    ((fun
          (f :
            (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
              Type (max u_1 u_2))) ↦
        (↑f : α → β))
      (Subtype.mk (p := fun (x : α → β) ↦
        Membership.mem (γ := Set (α → β))
          {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
        f ⋯))
    μ

Tactic:
aestronglyMeasurable_of_tendsto_ae u (fun n => hUI.1 (s n)) hs

Premises used: aestronglyMeasurable_of_tendsto_ae, And.left
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β)
    ((fun
          (f :
            (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
              Type (max u_1 u_2))) ↦
        (↑f : α → β))
      (Subtype.mk (p := fun (x : α → β) ↦
        Membership.mem (γ := Set (α → β))
          {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
        f ⋯))
    μ

Tactic:
exact aestronglyMeasurable_of_tendsto_ae u (fun n => hUI.1 (s n)) hs

Premises used: aestronglyMeasurable_of_tendsto_ae, And.left
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
refine_2 :
  ∀ (C : ℝ≥0) (hC : ∀ (i : ι), eLpNorm (fn i) p μ ≤ (↑C : ℝ≥0∞)),
    ∃ (C : ℝ≥0),
      ∀
        (i :
          (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
            Type (max u_1 u_2))),
        eLpNorm.{u_1, u_2} (ε := β)
            ((fun
                  (f :
                    (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                      Type (max u_1 u_2))) ↦
                (↑f : α → β))
              i)
            p μ ≤
          (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun
                (f :
                  (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                    Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)

Tactic:
obtain ⟨C, hC⟩ := hUI.2.2

Premises used: And.right