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∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
hι : ¬Nonempty ι
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
⟨0, fun i => False.elim <| hι <| Nonempty.intro i⟩

Premises used: False.elim, Nonempty.intro, Exists.intro, OfNat.ofNat
-- 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 ι
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
exact ⟨0, fun i => False.elim <| hι <| Nonempty.intro 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 : Subsingleton ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
⊢ UniformIntegrable f p μ

Tactic:
uniformIntegrable_finite hp_one hp_top hf

Premises used: MeasureTheory.uniformIntegrable_finite
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
⊢ UniformIntegrable.{u_1, u_2, u_3} (β := β) (fun (x : ι) ↦ g) p μ

Tactic:
⟨fun _ => hg.1, unifIntegrable_const hp hp_ne_top hg,
    ⟨(eLpNorm g p μ).toNNReal, fun _ => le_of_eq (ENNReal.coe_toNNReal hg.2.ne).symm⟩⟩

Premises used: ENNReal.coe_toNNReal, MeasureTheory.UniformIntegrable, ENNReal.toNNReal, And.right, And.left, And.intro, Exists.intro, MeasureTheory.unifIntegrable_const, le_of_eq, Eq.symm, LT.lt.ne, MeasureTheory.eLpNorm
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ UniformIntegrable f p μ

Tactic:
⟨fun i => (hf i).aestronglyMeasurable,
    unifIntegrable_of hp hp' (fun i => (hf i).aestronglyMeasurable) h, ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.UniformIntegrable, And.intro, MeasureTheory.unifIntegrable_of
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
refine : ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ UniformIntegrable f p μ

Tactic:
refine ⟨fun i => (hf i).aestronglyMeasurable,
    unifIntegrable_of hp hp' (fun i => (hf i).aestronglyMeasurable) h, ?_⟩
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
obtain :
  ∀ (C : ℝ≥0) (hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
obtain ⟨C, hC⟩ := h 1 one_pos

Premises used: OfNat.ofNat, one_pos
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
⟨((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1).toNNReal, fun i => ?_⟩

Premises used: ENNReal.ofNNReal, HMul.hMul, Set.univ, ENNReal.toNNReal, ENNReal.toReal, Inv.inv, HPow.hPow, HAdd.hAdd, Exists.intro, OfNat.ofNat, DFunLike.coe
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
refine :
  ∀ (i : ι),
    eLpNorm (f i) p μ ≤
      (↑((↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1).toNNReal : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
refine ⟨((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1).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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ eLpNorm (f i) p μ ≤
    eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ + eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ

Tactic:
le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.StronglyMeasurable.measurableSet_lt, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasureTheory.StronglyMeasurable.indicator, MeasureTheory.eLpNorm_mono_enorm, MeasureTheory.StronglyMeasurable.nnnorm, MeasureTheory.eLpNorm_add_le, le_trans
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
refine : ∀ (x : α), ‖f i x‖ₑ ≤ ‖(indicator {x : α | ‖f i x‖₊ < C} (f i) + indicator {x : α | C ≤ ‖f i x‖₊} (f i)) x‖ₑ
⊢ eLpNorm (f i) p μ ≤
    eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ + eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ

Tactic:
refine le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.StronglyMeasurable.measurableSet_lt, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasureTheory.StronglyMeasurable.indicator, MeasureTheory.eLpNorm_mono_enorm, MeasureTheory.StronglyMeasurable.nnnorm, MeasureTheory.eLpNorm_add_le, le_trans
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
rw :
  ‖f i x‖ₑ ≤
    ‖(if Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x then f i x else 0) +
        indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
⊢ ‖f i x‖ₑ ≤ ‖(indicator {x : α | ‖f i x‖₊ < C} (f i) + indicator {x : α | C ≤ ‖f i x‖₊} (f i)) x‖ₑ

Tactic:
rw [Pi.add_apply, Set.indicator_apply]

Premises used: Set.indicator_apply, Pi.add_apply
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
pos :
  ∀ (hx : Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x),
    ‖f i x‖ₑ ≤ ‖f i x + indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
neg : ∀ (hx : x ∉ {x : α | ‖f i x‖₊ < C}), ‖f i x‖ₑ ≤ ‖0 + indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
⊢ ‖f i x‖ₑ ≤
    ‖(if Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x then f i x else 0) +
        indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ

Tactic:
split_ifs with hx
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x
pos : x ∉ {x : α | C ≤ ‖f i x‖₊}
⊢ ‖f i x‖ₑ ≤ ‖f i x + indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ

Tactic:
rw [Set.indicator_of_notMem, add_zero]

Premises used: Set.indicator_of_notMem, add_zero
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x
⊢ x ∉ {x : α | C ≤ ‖f i x‖₊}

Tactic:
simpa using hx
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : x ∉ {x : α | ‖f i x‖₊ < C}
neg : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
⊢ ‖f i x‖ₑ ≤ ‖0 + indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ

Tactic:
rw [Set.indicator_of_mem, zero_add]

Premises used: zero_add, Set.indicator_of_mem
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : x ∉ {x : α | ‖f i x‖₊ < C}
⊢ Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x

Tactic:
simpa using hx
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
h₁ : ∀ (a : α), ‖indicator {x : α | ‖f i x‖₊ < C} (f i) a‖₊ ≤ C
⊢ ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C

Tactic:
filter_upwards
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
h₁ : ∀ (a : α), indicator {x : α | ‖f i x‖₊ < C} (fun (a : α) ↦ ‖f i a‖₊) a ≤ C
⊢ ∀ (a : α), ‖indicator {x : α | ‖f i x‖₊ < C} (f i) a‖₊ ≤ C

Tactic:
simp_rw [nnnorm_indicator_eq_indicator_nnnorm]

Premises used: nnnorm_indicator_eq_indicator_nnnorm
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ ∀ (a : α), indicator {x : α | ‖f i x‖₊ < C} (fun (a : α) ↦ ‖f i a‖₊) a ≤ C

Tactic:
Set.indicator_le fun x (hx : _ < _) => hx.le

Premises used: LT.lt.le, Set.indicator_le
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ ∀ (a : α), indicator {x : α | ‖f i x‖₊ < C} (fun (a : α) ↦ ‖f i a‖₊) a ≤ C

Tactic:
exact Set.indicator_le fun x (hx : _ < _) => hx.le

Premises used: LT.lt.le, Set.indicator_le
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C

Tactic:
have : ∀ᵐ x ∂μ, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖₊ ≤ C := by
        filter_upwards
        simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
        exact Set.indicator_le fun x (hx : _ < _) => hx.le
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C
⊢ eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ + eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1

Tactic:
add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)

Premises used: add_le_add, Eq.rec, ENNReal.ofReal_one, MeasureTheory.eLpNorm_le_of_ae_bound, le_trans
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C
refine :
  HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal (↑C : ℝ) ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ + eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1

Tactic:
refine add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)

Premises used: add_le_add, MeasureTheory.eLpNorm_le_of_ae_bound, le_trans
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C
simp_rw :
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal (↑C : ℝ) ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
simp_rw [NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm]

Premises used: NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C
⊢ (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
le_rfl

Premises used: le_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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C
⊢ (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
exact le_rfl

Premises used: le_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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1 ≠ ∞

Tactic:
finiteness
-- 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 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
rw rw₁ :
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1 =
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1
⊢ (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1 =
    (↑((↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1).toNNReal : ℝ≥0∞)

Tactic:
rw [ENNReal.coe_toNNReal (by finiteness)]

Premises used: ENNReal.coe_toNNReal