awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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 ε
⊢ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε
have rw₁ : ENNReal.ofReal ε ≤ ENNReal.ofReal ε
Tactic: rw [← ENNReal.ofReal_add (half_pos hε).le (half_pos hε).le, add_halves]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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 μ
have hp₁ : ∀ (ε : ℝ) (hε : 0 < ε),
  ∃ (C : ℝ≥0),
    0 < C ∧
      ∀ (i : ι),
        eLpNorm
            (indicator {x : α | C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖₊}
              (Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry))
            p μ ≤
          ENNReal.ofReal ε
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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),
    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 ε
have 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) sorry x‖₊}
              (Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry))
            p μ ≤
          ENNReal.ofReal ε
Tactic: obtain ⟨C, hC⟩ := h ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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 ε
have refine : indicator {x : α | C ≤ ‖g i x‖₊} (g i) =ᶠ[ae μ] indicator {x : α | C ≤ ‖f i x‖₊} (f i)
Tactic: refine le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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 : ι
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) =ᶠ[ae μ] indicator {x : α | C ≤ ‖f i x‖₊} (f i)
have h₁ : ∀ (x : α) (hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x),
  indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
Tactic: filter_upwards [(Exists.choose_spec <| hf i).2] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
have 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
Tactic: by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
have 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
Tactic: by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
have pos : Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
Tactic: rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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
⊢ Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
have pos : ∀ (hfx : C ≤ ‖f i x‖₊), Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
Tactic: rwa [Set.mem_setOf, hx] at hfx
Cleared hypotheses: hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
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
⊢ Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
have pos₁ : ∀ (hfx : C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖₊),
  Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
Tactic: rwa [Set.mem_setOf, hx] at hfx
Cleared hypotheses: hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
have neg : x ∉ {x : α | C ≤ ‖g i x‖₊}
Tactic: rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
⊢ x ∉ {x : α | C ≤ ‖g i x‖₊}
have neg : ∀ (hfx : ¬C ≤ ‖f i x‖₊), x ∉ {x : α | C ≤ ‖g i x‖₊}
Tactic: rwa [Set.mem_setOf, hx] at hfx
Cleared hypotheses: hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
neg : ∀ (hfx : ¬C ≤ ‖f i x‖₊), x ∉ {x : α | C ≤ ‖g i x‖₊}
⊢ x ∉ {x : α | C ≤ ‖g i x‖₊}
have neg₁ : ∀ (hfx : ¬C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖₊),
  x ∉ {x : α | C ≤ ‖g i x‖₊}
Tactic: rwa [Set.mem_setOf, hx] at hfx
Cleared hypotheses: hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
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 ε
⊢ ∃ (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 ε
have hCg : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
Tactic: have hCg : ∀ i, eLpNorm ({ x | C ≤ ‖g i x‖₊ }.indicator (g i)) p μ ≤ ENNReal.ofReal ε := by
    intro i
    refine le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)
    filter_upwards [(Exists.choose_spec <| hf i).2] with x hx
    by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
    · rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
      rwa [Set.mem_setOf, hx] at hfx
    · rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]
      rwa [Set.mem_setOf, hx] at hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0),
    0 < C ∧
      ∀ (i : ι),
        eLpNorm
            (indicator {x : α | C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
              (Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯))
            p μ ≤
          ENNReal.ofReal ε
have refine : ∀ (i : ι) (x : α),
  ‖indicator {x : α | max C 1 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖₊}
        (Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry) x‖ ≤
    ‖indicator {x : α | C ≤ ‖g i x‖₊} (g i) x‖
Tactic: refine ⟨max C 1, lt_max_of_lt_right one_pos, fun i => le_trans (eLpNorm_mono fun x => ?_) (hCg i)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ ‖indicator {x : α | max C 1 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
        (Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯) x‖ ≤
    ‖indicator {x : α | C ≤ ‖g i x‖₊} (g i) x‖
have rw : LE.le (α := ℝ)
  (indicator {x : α | max C 1 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖₊}
    (fun (a : α) ↦ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry a‖) x)
  (indicator {x : α | C ≤ ‖g i x‖₊} (fun (a : α) ↦ ‖g i a‖) x)
Tactic: rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ LE.le (α := ℝ)
    (indicator {x : α | max C 1 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
      (fun (a : α) ↦ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ a‖) x)
    (indicator {x : α | C ≤ ‖g i x‖₊} (fun (a : α) ↦ ‖g i a‖) x)
have h₁ : 0 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖
Tactic: grw [← le_max_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
h₁ : 0 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖
⊢ LE.le (α := ℝ)
    (indicator {x : α | max C 1 ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊}
      (fun (a : α) ↦ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ a‖) x)
    (indicator {x : α | C ≤ ‖g i x‖₊} (fun (a : α) ↦ ‖g i a‖) x)
have grw : LE.le (α := ℝ)
  (indicator {x : α | C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖₊}
    (fun (a : α) ↦ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry a‖) x)
  (indicator {x : α | C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖₊}
    (fun (a : α) ↦ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry a‖) x)
Tactic: grw [← le_max_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε
have obtain : ∀ (δ : ℝ) (hδ : 0 < δ)
  (hδ' :
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδ, hδ'⟩ := hUI hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε
have refine : ∀ (x : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (t : Set α)
  (ht : MeasurableSet t) (ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ) (f : α → β) (s : κ → ι)
  (hs : TendstoInMeasure μ (fn ∘ s) u f),
  eLpNorm.{u_1, u_2} (ε := β)
      (t.indicator
        ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
            (↑f : α → β))
          (Subtype.mk (p := fun (x : α → β) ↦
            Membership.mem (γ := Set (α → β)) {g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} x) f sorry)))
      p μ ≤
    ENNReal.ofReal ε
Tactic: refine ⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩