awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
⊢ eLpNorm.{u_1, u_2} (ε := β)
      (t.indicator
        ((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 ⋯)))
      p μ ≤
    ENNReal.ofReal ε

Tactic:
Lp.eLpNorm_le_of_ae_tendsto
    (Eventually.of_forall (f := u) fun n => hδ' (s n) t ht ht') ?_ ?_

Premises used: Filter.Eventually.of_forall, MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto
-- 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 : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
refine_1 : ∀ (n : κ), AEStronglyMeasurable (t.indicator (fn (s n))) μ
refine_2 :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{u_4, u_2} (β := β) (fun (x_1 : κ) ↦ t.indicator (fn (s x_1)) x) u
      (𝓝
        (t.indicator
          ((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 ⋯))
          x))
⊢ eLpNorm.{u_1, u_2} (ε := β)
      (t.indicator
        ((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 ⋯)))
      p μ ≤
    ENNReal.ofReal ε

Tactic:
refine Lp.eLpNorm_le_of_ae_tendsto
    (Eventually.of_forall (f := u) fun n => hδ' (s n) t ht ht') ?_ ?_

Premises used: Filter.Eventually.of_forall, MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto
-- 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 : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
⊢ ∀ (n : κ), AEStronglyMeasurable (t.indicator (fn (s n))) μ

Tactic:
fun n => (hfn (s n)).indicator ht

Premises used: MeasureTheory.AEStronglyMeasurable.indicator
-- 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 : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
⊢ ∀ (n : κ), AEStronglyMeasurable (t.indicator (fn (s n))) μ

Tactic:
exact fun n => (hfn (s n)).indicator ht

Premises used: MeasureTheory.AEStronglyMeasurable.indicator
-- 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 : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
h :
  ∀ (a : α) (ha : Tendsto (fun (n : κ) ↦ fn (s n) a) u (𝓝 (f a))),
    Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto.{u_4, u_2} (β := β) (fun (x_1 : κ) ↦ t.indicator (fn (s x_1)) x) u
      (𝓝
        (t.indicator
          ((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 ⋯))
          x))

Tactic:
filter_upwards [hs] with a ha
-- 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 : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun (n : κ) ↦ fn (s n) a) u (𝓝 (f a))
pos : ∀ (memt : a ∈ t), Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
neg : ∀ (memt : a ∉ t), Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
⊢ Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))

Tactic:
by_cases memt : a ∈ t
-- 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 : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun (n : κ) ↦ fn (s n) a) u (𝓝 (f a))
memt : a ∈ t
⊢ Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))

Tactic:
simpa [memt]
-- 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 : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun (n : κ) ↦ fn (s n) a) u (𝓝 (f a))
memt : a ∉ t
⊢ Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))

Tactic:
simp [memt]
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : MeasurableSpace α
⊢ @UniformIntegrable _ _ _ _ inst_1 f p 0

Tactic:
⟨fun _ => aestronglyMeasurable_zero_measure _, unifIntegrable_zero_meas, 0,
    fun _ => eLpNorm_measure_zero.le⟩

Premises used: MeasureTheory.unifIntegrable_zero_meas, MeasureTheory.aestronglyMeasurable_zero_measure, MeasureTheory.UniformIntegrable, Eq.le, And.intro, Exists.intro, OfNat.ofNat, MeasureTheory.eLpNorm_measure_zero
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hf : UniformIntegrable f p μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
obtain :
  ∀ (hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ) (hunif : UnifIntegrable f p μ) (C : ℝ≥0)
    (hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)), UniformIntegrable g p μ
⊢ UniformIntegrable g p μ

Tactic:
obtain ⟨hfm, hunif, C, hC⟩ := hf
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ UniformIntegrable g p μ

Tactic:
⟨fun i => (hfm i).congr (hfg i), (unifIntegrable_congr_ae hfg).1 hunif, C, fun i => ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.UniformIntegrable, And.intro, Exists.intro, Iff.mp, MeasureTheory.unifIntegrable_congr_ae
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
refine : ∀ (i : ι), eLpNorm (g i) p μ ≤ (↑C : ℝ≥0∞)
⊢ UniformIntegrable g p μ

Tactic:
refine ⟨fun i => (hfm i).congr (hfg i), (unifIntegrable_congr_ae hfg).1 hunif, C, fun i => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
i : ι
rw : eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ eLpNorm (g i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
rw [← eLpNorm_congr_ae (hfg i)]

Premises used: MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
i : ι
⊢ eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
hC i
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
i : ι
⊢ eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
exact hC i
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
⊢ UniformIntegrable f p μ ↔ UniformIntegrable g p μ

Tactic:
⟨fun h => h.ae_eq hfg, fun h => h.ae_eq fun i => (hfg i).symm⟩

Premises used: MeasureTheory.UniformIntegrable.ae_eq, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
intro : ∀ (val : Fintype ι), UniformIntegrable f p μ
⊢ UniformIntegrable f p μ

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
⊢ UniformIntegrable f p μ

Tactic:
⟨fun n => (hf n).1, unifIntegrable_finite hp_one hp_top hf, ?_⟩

Premises used: MeasureTheory.UniformIntegrable, And.left, And.intro, MeasureTheory.unifIntegrable_finite
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
intro : ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ UniformIntegrable f p μ

Tactic:
refine ⟨fun n => (hf n).1, unifIntegrable_finite hp_one hp_top hf, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
pos : ∀ (hι : Nonempty ι), ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
neg : ∀ (hι : ¬Nonempty ι), ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
by_cases hι : Nonempty ι

Premises used: Nonempty
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
hι : Nonempty ι
⊢ ∀ (i : ι), AEStronglyMeasurable (f i) μ

Tactic:
choose _ hf using hf
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ ∀ (i : ι), eLpNorm (f i) p μ < ∞

Tactic:
choose _ hf using hf
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
⟨C.toNNReal, fun i => ?_⟩

Premises used: ENNReal.toNNReal, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
pos : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C.toNNReal : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
refine ⟨C.toNNReal, fun i => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
pos : eLpNorm (f i) p μ ≤ C
pos₁ : C ≠ ∞
⊢ eLpNorm (f i) p μ ≤ (↑C.toNNReal : ℝ≥0∞)

Tactic:
rw [ENNReal.coe_toNNReal]

Premises used: ENNReal.coe_toNNReal
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
⊢ eLpNorm (f i) p μ ≤ C

Tactic:
Finset.le_max' (α := ℝ≥0∞) _ _ (Finset.mem_image.2 ⟨i, Finset.mem_univ _, rfl⟩)

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, Finset.le_max', And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
⊢ eLpNorm (f i) p μ ≤ C

Tactic:
exact Finset.le_max' (α := ℝ≥0∞) _ _ (Finset.mem_image.2 ⟨i, Finset.mem_univ _, rfl⟩)

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, Finset.le_max', And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
⊢ C ≠ ∞

Tactic:
ne_of_lt ((Finset.max'_lt_iff _ _).2 fun y hy => ?_)

Premises used: Iff.mpr, ne_of_lt, Finset.max'_lt_iff
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
pos :
  ∀ (y : ℝ≥0∞) (hy : Membership.mem (γ := Finset ℝ≥0∞) (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) y),
    y < ∞
⊢ C ≠ ∞

Tactic:
refine ne_of_lt ((Finset.max'_lt_iff _ _).2 fun y hy => ?_)

Premises used: Iff.mpr, ne_of_lt, Finset.max'_lt_iff
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
y : ℝ≥0∞
hy : Membership.mem (γ := Finset ℝ≥0∞) (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) y
⊢ ∃ (a : ι), Membership.mem (γ := Finset ι) Finset.univ a ∧ eLpNorm (f a) p μ = y

Tactic:
rw [Finset.mem_image] at hy

Premises used: Finset.mem_image
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
y : ℝ≥0∞
hy : ∃ (a : ι), Membership.mem (γ := Finset ι) Finset.univ a ∧ eLpNorm (f a) p μ = y
pos : ∀ (i : ι), eLpNorm (f i) p μ < ∞
⊢ y < ∞

Tactic:
obtain ⟨i, -, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i_1 i : ι
⊢ eLpNorm (f i) p μ < ∞

Tactic:
hf i
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i_1 i : ι
⊢ eLpNorm (f i) p μ < ∞

Tactic:
exact hf i