awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖
⊢ 0 ≤ ‖f x‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- 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‖
⊢ 0 ≤ ‖f x‖

Tactic:
exact norm_nonneg _

Premises used: norm_nonneg
-- 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‖
⊢ x ∉ {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊}

Tactic:
assumption
-- 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:
have : Tendsto (fun n : ℕ ↦ ∫⁻ a, ENNReal.ofReal ‖{ x | n ≤ ‖f x‖₊ }.indicator f a - 0‖ ∂μ)
      atTop (𝓝 0) := by
    refine tendsto_lintegral_norm_of_dominated_convergence hmeas hbound ?_ htendsto
    refine fun n => univ_mem' (id fun x => ?_)
    by_cases hx : (n : ℝ) ≤ ‖f x‖
    · dsimp
      rwa [Set.indicator_of_mem]
    · dsimp
      rw [Set.indicator_of_notMem, norm_zero]
      · exact norm_nonneg _
      · assumption
-- 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‖) μ
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ) atTop (𝓝 0)
⊢ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε

Tactic:
rw [ENNReal.tendsto_atTop_zero] at this

Premises used: ENNReal.tendsto_atTop_zero
-- 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‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
obtain :
  ∀ (M : ℕ)
    (hM :
      ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ENNReal.ofReal ε),
    ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨M, hM⟩ := this (ENNReal.ofReal ε) (ENNReal.ofReal_pos.2 hε)

Premises used: Iff.mpr, ENNReal.ofReal, ENNReal.ofReal_pos
-- 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‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ENNReal.ofReal ε
⊢ ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε

Tactic:
simp only [sub_zero] at hM

Premises used: sub_zero
-- 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‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε

Tactic:
⟨M, ?_⟩

Premises used: Nat.cast, Exists.intro
-- 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‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
refine : ∫⁻ (x : α), (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨M, ?_⟩
-- 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‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑M : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε

Tactic:
hM M le_rfl

Premises used: le_rfl
-- 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‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
h :
  ∀ (x : α),
    (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) =
      ENNReal.ofReal ‖Set.indicator {x : α | (↑M : ℝ≥0) ≤ ‖f x‖₊} f x‖
⊢ ∫⁻ (x : α), (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε

Tactic:
convert! hM M le_rfl

Premises used: le_rfl
-- 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‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
x : α
h :
  (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ ‖f x‖} f x‖₊ : ℝ≥0∞) =
    (↑(NNReal.mk ‖Set.indicator {x : α | (↑M : ℝ≥0) ≤ ‖f x‖₊} f x‖ ⋯) : ℝ≥0∞)
⊢ (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) =
    ENNReal.ofReal ‖Set.indicator {x : α | (↑M : ℝ≥0) ≤ ‖f x‖₊} f x‖

Tactic:
simp only [coe_nnnorm, ENNReal.ofReal_eq_coe_nnreal (norm_nonneg _)]

Premises used: coe_nnnorm, ENNReal.ofReal_eq_coe_nnreal, norm_nonneg
-- 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‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
x : α
⊢ (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ ‖f x‖} f x‖₊ : ℝ≥0∞) =
    (↑(NNReal.mk ‖Set.indicator {x : α | (↑M : ℝ≥0) ≤ ‖f x‖₊} f x‖ ⋯) : ℝ≥0∞)

Tactic:
rfl
-- 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 < ε
M : ℝ
hM : ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
⊢ ∫⁻ (x : α), ‖Set.indicator {x : α | max M 0 ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ ≤ ENNReal.ofReal ε

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
⊢ MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ

Tactic:
have hf_mk : MemLp (hf.1.mk f) 1 μ := (memLp_congr_ae hf.1.ae_eq_mk).mp hf
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
obtain :
  ∀ (M : ℝ) (hM_pos : 0 ≤ M)
    (hfM :
      ∫⁻ (x : α),
          ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
        ENNReal.ofReal ε),
    ∃ (M : ℝ), 0 ≤ M ∧ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), 0 ≤ M ∧ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨M, hM_pos, hfM⟩ :=
    hf_mk.integral_indicator_norm_ge_nonneg_le_of_meas hf.1.stronglyMeasurable_mk hε

Premises used: MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le_of_meas, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, And.left
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
M : ℝ
hM_pos : 0 ≤ M
hfM :
  ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
    ENNReal.ofReal ε
⊢ ∃ (M : ℝ), 0 ≤ M ∧ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ ≤ ENNReal.ofReal ε

Tactic:
⟨M, hM_pos, (le_of_eq ?_).trans hfM⟩

Premises used: And.intro, Exists.intro, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
M : ℝ
hM_pos : 0 ≤ M
hfM :
  ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
    ENNReal.ofReal ε
refine :
  ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ =
    ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ
⊢ ∃ (M : ℝ), 0 ≤ M ∧ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨M, hM_pos, (le_of_eq ?_).trans hfM⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
M : ℝ
hM_pos : 0 ≤ M
hfM :
  ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
    ENNReal.ofReal ε
⊢ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ =
    ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
M : ℝ
hM_pos : 0 ≤ M
hfM :
  ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
    ENNReal.ofReal ε
refine :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ) fun (x : α) ↦
    ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ
⊢ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ =
    ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
M : ℝ
hM_pos : 0 ≤ M
hfM :
  ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
    ENNReal.ofReal ε
h :
  ∀ (x : α) (hx : f x = AEStronglyMeasurable.mk f ⋯ x),
    ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ =
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ) fun (x : α) ↦
    ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ

Tactic:
filter_upwards [hf.1.ae_eq_mk] with x hx

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
M : ℝ
hM_pos : 0 ≤ M
hfM :
  ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
    ENNReal.ofReal ε
x : α
hx : f x = AEStronglyMeasurable.mk f ⋯ x
⊢ ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ =
    ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ

Tactic:
simp only [Set.indicator_apply, coe_nnnorm, Set.mem_setOf_eq, hx.symm]

Premises used: Set.indicator_apply, Set.mem_setOf_eq, coe_nnnorm, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
⊢ eLpNormEssSup f μ < ∞

Tactic:
have hbdd : eLpNormEssSup f μ < ∞ := hf.eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ ∃ (M : ℝ), eLpNormEssSup (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0

Tactic:
⟨(eLpNorm f ∞ μ + 1).toReal, ?_⟩

Premises used: ENNReal.toReal, HAdd.hAdd, Exists.intro, Top.top, OfNat.ofNat, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
refine : eLpNormEssSup (Set.indicator {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0
⊢ ∃ (M : ℝ), eLpNormEssSup (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0

Tactic:
refine ⟨(eLpNorm f ∞ μ + 1).toReal, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
rw : eLpNormEssSup f (μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}) = 0
rw₁ : MeasurableSet.{u_1} (α := α) {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}
⊢ eLpNormEssSup (Set.indicator {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0

Tactic:
rw [eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict]

Premises used: MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} = 0

Tactic:
simp only [coe_nnnorm, eLpNorm_exponent_top, Measure.restrict_eq_zero]

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.Measure.restrict_eq_zero, coe_nnnorm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
rw : (eLpNormEssSup f μ).toReal < ‖f x‖
⊢ Membership.mem (γ := Set α) {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)} x

Tactic:
rw [Set.mem_setOf_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne,
          ENNReal.coe_toReal, coe_nnnorm]

Premises used: ENNReal.coe_toReal, Set.mem_setOf_eq, coe_nnnorm, ENNReal.toReal_lt_toReal, ENNReal.coe_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
⊢ (eLpNormEssSup f μ).toReal < ‖f x‖

Tactic:
lt_of_lt_of_le ?_ hx

Premises used: lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
refine : (eLpNormEssSup f μ).toReal < (eLpNormEssSup f μ + 1).toReal
⊢ (eLpNormEssSup f μ).toReal < ‖f x‖

Tactic:
refine lt_of_lt_of_le ?_ hx

Premises used: lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
rw : eLpNormEssSup f μ < eLpNormEssSup f μ + 1
rw₁ : eLpNormEssSup f μ + 1 ≠ ∞
⊢ (eLpNormEssSup f μ).toReal < (eLpNormEssSup f μ + 1).toReal

Tactic:
rw [ENNReal.toReal_lt_toReal hbdd.ne]

Premises used: ENNReal.toReal_lt_toReal, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
⊢ eLpNormEssSup f μ < eLpNormEssSup f μ + 1

Tactic:
ENNReal.lt_add_right hbdd.ne one_ne_zero

Premises used: ENNReal.lt_add_right, one_ne_zero, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
⊢ eLpNormEssSup f μ < eLpNormEssSup f μ + 1

Tactic:
exact ENNReal.lt_add_right hbdd.ne one_ne_zero

Premises used: ENNReal.lt_add_right, one_ne_zero, LT.lt.ne