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 : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (a : α), indicator {x : α | ‖f i x‖₊ < C} (fun (a : α) ↦ ‖f i a‖) a ≤ (↑C : ℝ)

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

Premises used: LT.lt.le, NNReal.coe_nonneg, 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖ ≤ (↑C : ℝ)

Tactic:
have : ∀ᵐ x ∂μ.restrict s, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖ ≤ C := by
        filter_upwards
        simp_rw [norm_indicator_eq_indicator_norm]
        exact Set.indicator_le' (fun x (hx : _ < _) => hx.le) fun _ _ => NNReal.coe_nonneg _
-- 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 : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ.restrict s, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖ ≤ (↑C : ℝ)
⊢ eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p (μ.restrict s) ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
le_trans (eLpNorm_le_of_ae_bound this) ?_

Premises used: 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ.restrict s, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖ ≤ (↑C : ℝ)
refine :
  HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal (↑C : ℝ) ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p (μ.restrict s) ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
refine le_trans (eLpNorm_le_of_ae_bound this) ?_

Premises used: 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ.restrict s, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖ ≤ (↑C : ℝ)
rw :
  ENNReal.ofReal (↑C : ℝ) * HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
rw₁ :
  ENNReal.ofReal (↑C : ℝ) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ s) : ℝ≥0∞) p.toReal⁻¹ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
rw₂ :
  ENNReal.ofReal (↑C : ℝ) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) p.toReal⁻¹ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
rw₃ :
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) p.toReal⁻¹ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
rw₄ rw₅ :
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) p.toReal⁻¹ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) p.toReal⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal (↑C : ℝ) ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
rw [mul_comm, Measure.restrict_apply' hs, Set.univ_inter, ENNReal.ofReal_coe_nnreal, one_div]

Premises used: Set.univ_inter, one_div, ENNReal.ofReal_coe_nnreal, mul_comm, MeasureTheory.Measure.restrict_apply'
-- 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 : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
grw :
  ENNReal.ofReal (ε / 2) + (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal (ε / 2) + (↑C : ℝ≥0∞) * ENNReal.ofReal (ε / (2 * (↑C : ℝ)))
⊢ eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ +
      (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal (ε / 2) + (↑C : ℝ≥0∞) * ENNReal.ofReal (ε / (2 * (↑C : ℝ)))

Tactic:
grw [hC 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 : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
bc : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ ENNReal.ofReal (ε / (2 * (↑C : ℝ)))
⊢ ENNReal.ofReal (ε / 2) + (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal (ε / 2) + (↑C : ℝ≥0∞) * ENNReal.ofReal (ε / (2 * (↑C : ℝ)))

Tactic:
gcongr
-- 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 : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
bc : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) p.toReal⁻¹ ≤ ENNReal.ofReal (ε / (2 * (↑C : ℝ)))
bc₁ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (ε / (2 * (↑C : ℝ))) ^ p.toReal
bc₂ bc₃ bc₄ bc₅ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
⊢ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ ENNReal.ofReal (ε / (2 * (↑C : ℝ)))

Tactic:
rwa [one_div, ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hpzero hp'),
        ENNReal.ofReal_rpow_of_pos (div_pos hε (mul_pos two_pos (NNReal.coe_pos.2 hCpos)))]

Premises used: ENNReal.ofReal_rpow_of_pos, Iff.mpr, ENNReal.rpow_inv_le_iff, two_pos, ENNReal.toReal_pos, mul_pos, one_div, NNReal.coe_pos, div_pos
-- 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 : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
bc : (↑C : ℝ≥0∞) * ENNReal.ofReal (ε / (2 * (↑C : ℝ))) ≤ ENNReal.ofReal (ε / 2)
⊢ ENNReal.ofReal (ε / 2) + (↑C : ℝ≥0∞) * ENNReal.ofReal (ε / (2 * (↑C : ℝ))) ≤
    ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)

Tactic:
gcongr
-- 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 : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
bc : ENNReal.ofReal (↑C : ℝ) * ENNReal.ofReal (ε / (2 * (↑C : ℝ))) ≤ ENNReal.ofReal (ε / 2)
bc₁ : ENNReal.ofReal ((↑C : ℝ) * (ε / (2 * (↑C : ℝ)))) ≤ ENNReal.ofReal (ε / 2)
bc₂ : ENNReal.ofReal ((↑C : ℝ) * (ε / 2 / (↑C : ℝ))) ≤ ENNReal.ofReal (ε / 2)
bc₃ bc₄ : ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal (ε / 2)
⊢ (↑C : ℝ≥0∞) * ENNReal.ofReal (ε / (2 * (↑C : ℝ))) ≤ ENNReal.ofReal (ε / 2)

Tactic:
rw [← ENNReal.ofReal_coe_nnreal, ← ENNReal.ofReal_mul (NNReal.coe_nonneg _), ← div_div,
        mul_div_cancel₀ _ (NNReal.coe_pos.2 hCpos).ne.symm]

Premises used: Iff.mpr, ENNReal.ofReal_mul, Ne.symm, mul_div_cancel₀, NNReal.coe_nonneg, ENNReal.ofReal_coe_nnreal, NNReal.coe_pos, div_div, LT.lt.ne
-- 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 : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : ENNReal.ofReal (ε / 2 + ε / 2) ≤ ENNReal.ofReal ε
rw₁ rw₂ : ENNReal.ofReal ε ≤ ENNReal.ofReal ε
⊢ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε

Tactic:
rw [← ENNReal.ofReal_add (half_pos hε).le (half_pos hε).le, add_halves]

Premises used: add_halves, half_pos, LT.lt.le, ENNReal.ofReal_add
-- 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) ⋯
⊢ UnifIntegrable f p μ

Tactic:
(unifIntegrable_of' hp hp' (fun i => (Exists.choose_spec <| hf i).1) fun ε hε => ?_).ae_eq
      fun i => (Exists.choose_spec <| hf i).2.symm

Premises used: Exists.choose_spec, MeasureTheory.UnifIntegrable.ae_eq, And.right, And.left, MeasureTheory.unifIntegrable_of', Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
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) ⋯
hp₁ :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ∃ (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 ε
⊢ UnifIntegrable f p μ

Tactic:
refine
    (unifIntegrable_of' hp hp' (fun i => (Exists.choose_spec <| hf i).1) fun ε hε => ?_).ae_eq
      fun i => (Exists.choose_spec <| hf i).2.symm

Premises used: Exists.choose_spec, MeasureTheory.UnifIntegrable.ae_eq, And.right, And.left, MeasureTheory.unifIntegrable_of', Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
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 < ε
obtain :
  ∀ (C : ℝ≥0) (hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f 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 ε
⊢ ∃ (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:
obtain ⟨C, hC⟩ := h ε hε
-- 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:
le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)

Premises used: le_of_eq, MeasureTheory.eLpNorm_congr_ae, 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 ε
i : ι
refine : indicator {x : α | C ≤ ‖g i x‖₊} (g i) =ᶠ[ae μ] indicator {x : α | C ≤ ‖f i x‖₊} (f i)
⊢ eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε

Tactic:
refine le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)

Premises used: le_of_eq, MeasureTheory.eLpNorm_congr_ae, 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 ε
i : ι
h₁ :
  ∀ (x : α) (hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x),
    indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) =ᶠ[ae μ] indicator {x : α | C ≤ ‖f i x‖₊} (f i)

Tactic:
filter_upwards [(Exists.choose_spec <| hf i).2] with x hx

Premises used: Exists.choose_spec, And.right
-- 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
pos :
  ∀ (hfx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x),
    indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
neg :
  ∀ (hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}),
    indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x

Tactic:
by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
-- 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 : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
pos : Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x

Tactic:
rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]

Premises used: 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∞
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 : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
pos : ∀ (hfx : C ≤ ‖f i x‖₊), Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
pos₁ pos₂ pos₃ pos₄ :
  ∀ (hfx : C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊),
    Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
⊢ Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x

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

Premises used: Set.mem_setOf