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 β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
obtain :
  ∀ (δ : ℝ) (hδ_pos : 0 < δ)
    (hδε :
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
            eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε

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

Tactic:
⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
refine :
  ∀ (i : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
    eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε

Tactic:
refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ

Tactic:
rw [μ.restrict_apply hs, ← measure_toMeasurable] at hμs

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
rw : eLpNorm (f i) p ((μ.restrict E).restrict s) = eLpNorm (f i) p (μ.restrict (s ∩ E))
rw₁ rw₂ : eLpNorm (f i) p (μ.restrict (s ∩ E)) = eLpNorm (f i) p (μ.restrict (s ∩ E))
⊢ eLpNorm (s.indicator (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E))

Tactic:
rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, μ.restrict_restrict hs]

Premises used: MeasureTheory.Measure.restrict_restrict, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
⊢ eLpNorm (f i) p (μ.restrict (s ∩ E)) ≤ eLpNorm (f i) p (μ.restrict (toMeasurable μ (s ∩ E)))

Tactic:
eLpNorm_mono_measure _ <| Measure.restrict_mono (subset_toMeasurable _ _) le_rfl

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono, MeasureTheory.subset_toMeasurable, MeasureTheory.eLpNorm_mono_measure
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
⊢ eLpNorm (f i) p (μ.restrict (toMeasurable μ (s ∩ E))) = eLpNorm ((toMeasurable μ (s ∩ E)).indicator (f i)) p μ

Tactic:
(eLpNorm_indicator_eq_eLpNorm_restrict (measurableSet_toMeasurable _ _)).symm

Premises used: MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, MeasureTheory.measurableSet_toMeasurable, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
⊢ eLpNorm ((toMeasurable μ (s ∩ E)).indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
hδε i _ (measurableSet_toMeasurable _ _) hμs

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
eLpNorm :
  MeasureTheory.eLpNorm (s.indicator (f i)) p (μ.restrict E) = MeasureTheory.eLpNorm (f i) p (μ.restrict (s ∩ E))
⊢ MeasureTheory.eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε

Tactic:
calc
    eLpNorm (indicator s (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E)) := by
      rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, μ.restrict_restrict hs]
    _ ≤ eLpNorm (f i) p (μ.restrict (toMeasurable μ (s ∩ E))) :=
      eLpNorm_mono_measure _ <| Measure.restrict_mono (subset_toMeasurable _ _) le_rfl
    _ = eLpNorm (indicator (toMeasurable μ (s ∩ E)) (f i)) p μ :=
      (eLpNorm_indicator_eq_eLpNorm_restrict (measurableSet_toMeasurable _ _)).symm
    _ ≤ ENNReal.ofReal ε := hδε i _ (measurableSet_toMeasurable _ _) hμs

Premises used: le_rfl, ENNReal.ofReal, Set.indicator, MeasureTheory.Measure.restrict_mono, MeasureTheory.Measure.restrict, MeasureTheory.subset_toMeasurable, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, Inter.inter, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.eLpNorm_mono_measure, MeasureTheory.toMeasurable, Eq.symm, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedAddCommGroup β
inst_1 : MeasurableSpace α
p : ℝ≥0∞
f : ι → α → β
ε : ℝ
h : 0 < ε
i : ι
s : Set α
h_1 : MeasurableSet s
h_2 : ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal 1
⊢ @eLpNorm _ _ _ inst_1 (s.indicator (f i)) p 0 ≤ ENNReal.ofReal ε

Tactic:
simp
-- 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
⊢ UnifIntegrable f p μ ↔ UnifIntegrable g p μ

Tactic:
⟨fun hf => hf.ae_eq hfg, fun hg => hg.ae_eq fun n => (hfg n).symm⟩

Premises used: MeasureTheory.UnifIntegrable.ae_eq, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
⊢ Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)

Tactic:
tendsto_atTop_of_eventually_const (i₀ := Nat.ceil (‖f x‖₊ : ℝ) + 1) fun n hn => ?_

Premises used: tendsto_atTop_of_eventually_const
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
refine : ∀ (n : ℕ) (hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1), indicator {x : α | (↑n : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x = 0
⊢ Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)

Tactic:
refine tendsto_atTop_of_eventually_const (i₀ := Nat.ceil (‖f x‖₊ : ℝ) + 1) fun n hn => ?_

Premises used: tendsto_atTop_of_eventually_const
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
h : x ∉ {x : α | (↑n : ℝ) ≤ (↑‖f x‖₊ : ℝ)}
⊢ indicator {x : α | (↑n : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x = 0

Tactic:
rw [Set.indicator_of_notMem]

Premises used: Set.indicator_of_notMem
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
h : (↑‖f x‖₊ : ℝ) < (↑n : ℝ)
⊢ x ∉ {x : α | (↑n : ℝ) ≤ (↑‖f x‖₊ : ℝ)}

Tactic:
simp only [not_le, Set.mem_setOf_eq]

Premises used: not_le, Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
⊢ (↑‖f x‖₊ : ℝ) < (↑n : ℝ)

Tactic:
lt_of_le_of_lt (Nat.le_ceil _) ?_

Premises used: lt_of_le_of_lt, Nat.le_ceil
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
h : LT.lt (α := ℝ) (↑⌈(↑‖f x‖₊ : ℝ)⌉₊ : ℝ) (↑n : ℝ)
⊢ (↑‖f x‖₊ : ℝ) < (↑n : ℝ)

Tactic:
refine lt_of_le_of_lt (Nat.le_ceil _) ?_

Premises used: lt_of_le_of_lt, Nat.le_ceil
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
⊢ LT.lt (α := ℝ) (↑⌈(↑‖f x‖₊ : ℝ)⌉₊ : ℝ) (↑n : ℝ)

Tactic:
lt_of_lt_of_le (lt_add_one _) ?_

Premises used: lt_add_one, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
h : HAdd.hAdd (α := ℝ) (↑⌈(↑‖f x‖₊ : ℝ)⌉₊ : ℝ) 1 ≤ (↑n : ℝ)
⊢ LT.lt (α := ℝ) (↑⌈(↑‖f x‖₊ : ℝ)⌉₊ : ℝ) (↑n : ℝ)

Tactic:
refine lt_of_lt_of_le (lt_add_one _) ?_

Premises used: lt_add_one, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
h h₁ h₂ h₃ : ⌈‖f x‖⌉₊ + 1 ≤ n
⊢ HAdd.hAdd (α := ℝ) (↑⌈(↑‖f x‖₊ : ℝ)⌉₊ : ℝ) 1 ≤ (↑n : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)

Tactic:
have htendsto :
      ∀ᵐ x ∂μ, Tendsto (fun M : ℕ => { x | (M : ℝ) ≤ ‖f x‖₊ }.indicator f x) atTop (𝓝 0) :=
    univ_mem' (id fun x => tendsto_indicator_ge f x)
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
M : ℕ
apply : MeasurableSet.{u_1} (α := α) {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)}
⊢ AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ

Tactic:
apply hf.1.indicator

Premises used: And.left, MeasureTheory.AEStronglyMeasurable.indicator
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
M : ℕ
⊢ MeasurableSet.{u_1} (α := α) {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)}

Tactic:
apply StronglyMeasurable.measurableSet_le stronglyMeasurable_const
      hmeas.nnnorm.measurable.coe_nnreal_real.stronglyMeasurable

Premises used: MeasureTheory.stronglyMeasurable_const, Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.StronglyMeasurable.measurableSet_le, Measurable.coe_nnreal_real, MeasureTheory.StronglyMeasurable.nnnorm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
⊢ ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ

Tactic:
have hmeas : ∀ M : ℕ, AEStronglyMeasurable ({ x | (M : ℝ) ≤ ‖f x‖₊ }.indicator f) μ := by
    intro M
    apply hf.1.indicator
    apply StronglyMeasurable.measurableSet_le stronglyMeasurable_const
      hmeas.nnnorm.measurable.coe_nnreal_real.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
rw :
  ∀ (hf : Integrable f μ) (hmeas : StronglyMeasurable f) {ε : ℝ} (hε : 0 < ε)
    (htendsto :
      ∀ᵐ (x : α) ∂μ,
        Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0))
    (hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ),
    HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ

Tactic:
rw [memLp_one_iff_integrable] at hf

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ

Tactic:
hf.norm.2

Premises used: And.right, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ

Tactic:
exact hf.norm.2

Premises used: And.right, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ

Tactic:
have hbound : HasFiniteIntegral (fun x => ‖f x‖) μ := by
    rw [memLp_one_iff_integrable] at hf
    exact hf.norm.2
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ) atTop (𝓝 0)

Tactic:
tendsto_lintegral_norm_of_dominated_convergence hmeas hbound ?_ htendsto

Premises used: MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
refine : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ) atTop (𝓝 0)

Tactic:
refine tendsto_lintegral_norm_of_dominated_convergence hmeas hbound ?_ htendsto

Premises used: MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖

Tactic:
fun n => univ_mem' (id fun x => ?_)

Premises used: Filter.Eventually, id, Filter.univ_mem'
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
refine :
  ∀ (n : ℕ) (x : α),
    Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖

Tactic:
refine fun n => univ_mem' (id fun x => ?_)

Premises used: id, Filter.univ_mem'
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
n : ℕ
x : α
pos :
  ∀ (hx : (↑n : ℝ) ≤ ‖f x‖),
    Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x
neg :
  ∀ (hx : ¬(↑n : ℝ) ≤ ‖f x‖),
    Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x

Tactic:
by_cases hx : (n : ℝ) ≤ ‖f x‖

Premises used: Nat.cast
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
n : ℕ
x : α
hx : (↑n : ℝ) ≤ ‖f x‖
pos : ‖f x‖ ≤ ‖f x‖
pos₁ : Membership.mem (γ := Set α) {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} x
pos₂ : ‖f x‖ ≤ ‖f x‖
pos₃ pos₄ pos₅ : Membership.mem (γ := Set α) {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} x
⊢ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖

Tactic:
rwa [Set.indicator_of_mem]

Premises used: Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
n : ℕ
x : α
hx : ¬(↑n : ℝ) ≤ ‖f x‖
neg : 0 ≤ ‖f x‖
neg₁ : x ∉ {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊}
⊢ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖

Tactic:
rw [Set.indicator_of_notMem, norm_zero]

Premises used: norm_zero, Set.indicator_of_notMem