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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
neg : x ∉ {x : α | C ≤ ‖g i x‖₊}
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x

Tactic:
rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]

Premises used: Set.indicator_of_notMem
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
neg : ∀ (hfx : ¬C ≤ ‖f i x‖₊), x ∉ {x : α | C ≤ ‖g i x‖₊}
neg₁ neg₂ neg₃ neg₄ :
  ∀ (hfx : ¬C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊),
    x ∉ {x : α | C ≤ ‖g i x‖₊}
⊢ x ∉ {x : α | C ≤ ‖g i x‖₊}

Tactic:
rwa [Set.mem_setOf, hx] at hfx

Premises used: Set.mem_setOf
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε

Tactic:
have hCg : ∀ i, eLpNorm ({ x | C ≤ ‖g i x‖₊ }.indicator (g i)) p μ ≤ ENNReal.ofReal ε := by
    intro i
    refine le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)
    filter_upwards [(Exists.choose_spec <| hf i).2] with x hx
    by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
    · rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
      rwa [Set.mem_setOf, hx] at hfx
    · rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]
      rwa [Set.mem_setOf, hx] at hfx
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0),
    0 < C ∧
      ∀ (i : ι),
        eLpNorm
            (indicator {x : α | C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
              (Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯))
            p μ ≤
          ENNReal.ofReal ε

Tactic:
⟨max C 1, lt_max_of_lt_right one_pos, fun i => le_trans (eLpNorm_mono fun x => ?_) (hCg i)⟩

Premises used: lt_max_of_lt_right, Max.max, MeasureTheory.eLpNorm_mono, And.intro, Exists.intro, OfNat.ofNat, one_pos, le_trans
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
refine :
  ∀ (i : ι) (x : α),
    ‖indicator {x : α | max C 1 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
          (Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯) x‖ ≤
      ‖indicator {x : α | C ≤ ‖g i x‖₊} (g i) x‖
⊢ ∃ (C : ℝ≥0),
    0 < C ∧
      ∀ (i : ι),
        eLpNorm
            (indicator {x : α | C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
              (Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯))
            p μ ≤
          ENNReal.ofReal ε

Tactic:
refine ⟨max C 1, lt_max_of_lt_right one_pos, fun i => le_trans (eLpNorm_mono fun x => ?_) (hCg i)⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
rw :
  LE.le (α := ℝ)
    (indicator {x : α | max C 1 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
      (fun (a : α) ↦ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ a‖) x)
    (indicator {x : α | C ≤ ‖g i x‖₊} (fun (a : α) ↦ ‖g i a‖) x)
⊢ ‖indicator {x : α | max C 1 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
        (Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯) x‖ ≤
    ‖indicator {x : α | C ≤ ‖g i x‖₊} (g i) x‖

Tactic:
rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]

Premises used: norm_indicator_eq_indicator_norm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
h₁ : 0 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖
grw grw₁ :
  LE.le (α := ℝ)
    (indicator {x : α | C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
      (fun (a : α) ↦ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ a‖) x)
    (indicator {x : α | C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
      (fun (a : α) ↦ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ a‖) x)
⊢ LE.le (α := ℝ)
    (indicator {x : α | max C 1 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
      (fun (a : α) ↦ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ a‖) x)
    (indicator {x : α | C ≤ ‖g i x‖₊} (fun (a : α) ↦ ‖g i a‖) x)

Tactic:
grw [← le_max_left]

Premises used: le_max_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 : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
obtain :
  ∀ (δ : ℝ) (hδ : 0 < δ)
    (hδ' :
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
            eLpNorm.{u_1, u_2} (ε := β)
                (s.indicator
                  ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
                      (↑f : α → β))
                    i))
                p μ ≤
              ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδ, hδ'⟩ := hUI hε
-- 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 ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε

Tactic:
⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩

Premises used: ENNReal.ofReal, Set.indicator, LE.le, _private.0.MeasureTheory.UnifIntegrable.unifIntegrable_of_tendstoInMeasure.match_1, 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 : 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 ε
refine :
  ∀ (x : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (t : Set α)
    (ht : MeasurableSet t) (ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ) (f : α → β) (s : κ → ι)
    (hs : TendstoInMeasure μ (fn ∘ s) u f),
    eLpNorm.{u_1, u_2} (ε := β)
        (t.indicator
          ((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 ⋯)))
        p μ ≤
      ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε

Tactic:
refine ⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩
-- 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 : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : TendstoInMeasure μ (fn ∘ s) u f
⊢ eLpNorm.{u_1, u_2} (ε := β)
      (t.indicator
        ((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 ⋯)))
      p μ ≤
    ENNReal.ofReal ε

Tactic:
eLpNorm_le_of_tendstoInMeasure
    (Eventually.of_forall fun n => hδ' (s n) t ht ht') (hs.indicator t) ?_

Premises used: MeasureTheory.TendstoInMeasure.indicator, Filter.Eventually.of_forall, MeasureTheory.eLpNorm_le_of_tendstoInMeasure
-- 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 : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : TendstoInMeasure μ (fn ∘ s) u f
refine : ∀ (i : κ), AEStronglyMeasurable (t.indicator (fn (s i))) μ
⊢ eLpNorm.{u_1, u_2} (ε := β)
      (t.indicator
        ((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 ⋯)))
      p μ ≤
    ENNReal.ofReal ε

Tactic:
refine eLpNorm_le_of_tendstoInMeasure
    (Eventually.of_forall fun n => hδ' (s n) t ht ht') (hs.indicator t) ?_

Premises used: MeasureTheory.TendstoInMeasure.indicator, Filter.Eventually.of_forall, MeasureTheory.eLpNorm_le_of_tendstoInMeasure
-- 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 : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : TendstoInMeasure μ (fn ∘ s) u f
⊢ ∀ (i : κ), AEStronglyMeasurable (t.indicator (fn (s i))) μ

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 : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : TendstoInMeasure μ (fn ∘ s) u f
⊢ ∀ (i : κ), AEStronglyMeasurable (t.indicator (fn (s i))) μ

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

Tactic:
obtain ⟨δ, hδ, hδ'⟩ := hUI hε
-- 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 ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2)))
      (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun
                      (f :
                        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                          Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε

Tactic:
⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩

Premises used: ENNReal.ofReal, Set.indicator, LE.le, Exists.intro, _private.0.MeasureTheory.UnifIntegrable.unifIntegrable_of_ae_tendsto.match_1, 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 : 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 ε
refine :
  ∀
    (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 ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2)))
      (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun
                      (f :
                        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                          Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε

Tactic:
refine ⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩