awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
⊢ ∑ x ∈ Finset.range (n, I).1,
      dist (α := ℝ) (∫ (v : ℝ) in c..((n, I).2 x).1, f v) (∫ (v : ℝ) in c..((n, I).2 x).2, f v) ≤
    (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range (n, I).1, uIoc ((n, I).2 i).1 ((n, I).2 i).2,
        ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
have hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
Tactic: obtain ⟨hnI1, hnI2⟩ := mem_setOf_eq ▸ hnI
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
⊢ ∑ x ∈ Finset.range (n, I).1,
      dist (α := ℝ) (∫ (v : ℝ) in c..((n, I).2 x).1, f v) (∫ (v : ℝ) in c..((n, I).2 x).2, f v) ≤
    (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range (n, I).1, uIoc ((n, I).2 i).1 ((n, I).2 i).2,
        ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
have hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
Tactic: obtain ⟨hnI1, hnI2⟩ := mem_setOf_eq ▸ hnI
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
⊢ ∑ x ∈ Finset.range (n, I).1,
      dist (α := ℝ) (∫ (v : ℝ) in c..((n, I).2 x).1, f v) (∫ (v : ℝ) in c..((n, I).2 x).2, f v) ≤
    (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range (n, I).1, uIoc ((n, I).2 i).1 ((n, I).2 i).2,
        ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
have h₁ : ∑ x ∈ Finset.range n, dist (α := ℝ) (∫ (v : ℝ) in c..(I x).1, f v) (∫ (v : ℝ) in c..(I x).2, f v) ≤
  (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range n, uIoc (I i).1 (I i).2, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
Tactic: simp only
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
⊢ ∑ x ∈ Finset.range n, dist (α := ℝ) (∫ (v : ℝ) in c..(I x).1, f v) (∫ (v : ℝ) in c..(I x).2, f v) ≤
    (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range n, uIoc (I i).1 (I i).2, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
have h₁ : LE.le (α := ℝ) (∑ x ∈ Finset.range n, dist (α := ℝ) (∫ (v : ℝ) in c..(I x).1, f v) (∫ (v : ℝ) in c..(I x).2, f v))
  (∑ i ∈ Finset.range (n, I).1,
    @integral _ _ _ _ Real.measurableSpace
      (Measure.restrict (Measure.restrict volume (uIoc a b)) (uIoc ((n, I).2 i).1 ((n, I).2 i).2)) fun (x : ℝ) ↦ ‖f x‖)
Tactic: rw [← integral_norm_eq_lintegral_enorm (h.aestronglyMeasurable_restrict_uIoc.restrict),
      integral_biUnion_finset _ (by simp +contextual [uIoc]) hnI2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
h₁ :
  LE.le (α := ℝ) (∑ x ∈ Finset.range n, dist (α := ℝ) (∫ (v : ℝ) in c..(I x).1, f v) (∫ (v : ℝ) in c..(I x).2, f v))
    (∑ i ∈ Finset.range (n, I).1,
      @integral _ _ _ _ Real.measurableSpace
        (Measure.restrict (Measure.restrict volume (uIoc a b)) (uIoc ((n, I).2 i).1 ((n, I).2 i).2)) fun (x : ℝ) ↦
        ‖f x‖)
⊢ ∑ x ∈ Finset.range n, dist (α := ℝ) (∫ (v : ℝ) in c..(I x).1, f v) (∫ (v : ℝ) in c..(I x).2, f v) ≤
    (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range n, uIoc (I i).1 (I i).2, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
have h₂ : ∀ i ∈ Finset.range (n, I).1,
  IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ ‖f x‖) (uIoc ((n, I).2 i).1 ((n, I).2 i).2)
    (Measure.restrict volume (uIoc a b))
Tactic: rw [← integral_norm_eq_lintegral_enorm (h.aestronglyMeasurable_restrict_uIoc.restrict),
      integral_biUnion_finset _ (by simp +contextual [uIoc]) hnI2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.range n, dist (α := ℝ) (∫ (v : ℝ) in c..(I x).1, f v) (∫ (v : ℝ) in c..(I x).2, f v))
    (∑ i ∈ Finset.range (n, I).1,
      @integral _ _ _ _ Real.measurableSpace
        (Measure.restrict (Measure.restrict volume (uIoc a b)) (uIoc ((n, I).2 i).1 ((n, I).2 i).2)) fun (x : ℝ) ↦
        ‖f x‖)
have h₁ : ∀ (i : ℕ) (hi : i ∈ Finset.range n),
  dist (α := ℝ) (∫ (v : ℝ) in c..(I i).1, f v) (∫ (v : ℝ) in c..(I i).2, f v) ≤
    @integral _ _ _ _ Real.measurableSpace
      (Measure.restrict (Measure.restrict volume (uIoc a b)) (uIoc ((n, I).2 i).1 ((n, I).2 i).2)) fun (x : ℝ) ↦ ‖f x‖
Tactic: refine Finset.sum_le_sum (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ IntervalIntegrable f volume c (I i).1
have apply : uIoc c (I i).1 ⊆ uIoc a b
Tactic: apply IntervalIntegrable.mono_set' h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ IntervalIntegrable f volume c (I i).2
have apply : uIoc c (I i).2 ⊆ uIoc a b
Tactic: apply IntervalIntegrable.mono_set' h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (α := ℝ) (∫ (v : ℝ) in c..(I i).1, f v) (∫ (v : ℝ) in c..(I i).2, f v) ≤
    @integral _ _ _ _ Real.measurableSpace
      (Measure.restrict (Measure.restrict volume (uIoc a b)) (uIoc ((n, I).2 i).1 ((n, I).2 i).2)) fun (x : ℝ) ↦ ‖f x‖
have h₁ : LE.le (α := ℝ)
  |@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (uIoc (I i).1 (I i).2)) fun (x : ℝ) ↦ f x|
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (uIoc (I i).1 (I i).2)) fun (x : ℝ) ↦ ‖f x‖)
Tactic: rw [Real.dist_eq,
        intervalIntegral.integral_interval_sub_left
          (by apply IntervalIntegrable.mono_set' h; grind [uIoc, uIcc])
          (by apply IntervalIntegrable.mono_set' h; grind [uIoc, uIcc]),
        Measure.restrict_restrict_of_subset
          (uIoc_subset_of_mem_disjWithin hnI (Finset.mem_range.mp hi)),
        intervalIntegral.integral_symm, abs_neg,
        intervalIntegral.abs_intervalIntegral_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range (n, I).1
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ ‖f x‖)
    (Measure.restrict (Measure.restrict volume (uIoc a b)) (uIoc ((n, I).2 i).1 ((n, I).2 i).2))
have h_subset : uIoc (I i).1 (I i).2 ⊆ uIoc a b
Tactic: have h_subset := uIoc_subset_of_mem_disjWithin hnI (Finset.mem_range.mp hi)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
hnI1 : ∀ i ∈ Finset.range (n, I).1, ((n, I).2 i).1 ∈ uIcc a b ∧ ((n, I).2 i).2 ∈ uIcc a b
hnI2 : (↑(Finset.range (n, I).1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc ((n, I).2 i).1 ((n, I).2 i).2
i : ℕ
hi : i ∈ Finset.range (n, I).1
h_subset : uIoc (I i).1 (I i).2 ⊆ uIoc a b
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ ‖f x‖)
    (Measure.restrict (Measure.restrict volume (uIoc a b)) (uIoc ((n, I).2 i).1 ((n, I).2 i).2))
have h₁ : @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ ‖f x‖) (Measure.restrict volume (uIoc (I i).1 (I i).2))
Tactic: rw [Measure.restrict_restrict_of_subset h_subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
⊢ Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
have rw : Membership.mem (γ := Set ↥(Lp F p μ))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (lpMeasSubgroup F m p μ)))) f ↔
  AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
Tactic: rw [← AddSubgroup.mem_carrier, lpMeasSubgroup, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
rw :
  Membership.mem (γ := Set ↥(Lp F p μ))
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (lpMeasSubgroup F m p μ))))
      f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
have rw₁ : Membership.mem (γ := Set ↥(Lp F p μ))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (AddSubgroup.toAddSubmonoid
          { carrier := {f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ}, add_mem' := sorry,
            zero_mem' := sorry, neg_mem' := sorry : AddSubgroup ↥(Lp F p μ) })))
    f ↔
  AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
Tactic: rw [← AddSubgroup.mem_carrier, lpMeasSubgroup, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
rw :
  Membership.mem (γ := Set ↥(Lp F p μ))
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (lpMeasSubgroup F m p μ))))
      f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
rw₁ :
  Membership.mem (γ := Set ↥(Lp F p μ))
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (AddSubgroup.toAddSubmonoid
            { carrier := {f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ}, add_mem' := ⋯,
              zero_mem' := ⋯, neg_mem' := ⋯ : AddSubgroup ↥(Lp F p μ) })))
      f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
have rw₂ : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ ↔ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
Tactic: rw [← AddSubgroup.mem_carrier, lpMeasSubgroup, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
⊢ Membership.mem (γ := Submodule 𝕜 ↥(Lp F p μ)) (lpMeas F 𝕜 m p μ) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
have rw : f ∈ (↑(lpMeas F 𝕜 m p μ) : Set ↥(Lp F p μ)) ↔ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
Tactic: rw [← SetLike.mem_coe, ← Submodule.mem_carrier, lpMeas, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
rw : f ∈ (↑(lpMeas F 𝕜 m p μ) : Set ↥(Lp F p μ)) ↔ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ Membership.mem (γ := Submodule 𝕜 ↥(Lp F p μ)) (lpMeas F 𝕜 m p μ) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
have rw₁ : Membership.mem (γ := Set ↥(Lp F p μ))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (lpMeas F 𝕜 m p μ)))) f ↔
  AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
Tactic: rw [← SetLike.mem_coe, ← Submodule.mem_carrier, lpMeas, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
rw : f ∈ (↑(lpMeas F 𝕜 m p μ) : Set ↥(Lp F p μ)) ↔ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
rw₁ :
  Membership.mem (γ := Set ↥(Lp F p μ))
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (lpMeas F 𝕜 m p μ)))) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ Membership.mem (γ := Submodule 𝕜 ↥(Lp F p μ)) (lpMeas F 𝕜 m p μ) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
have rw₂ : Membership.mem (γ := Set ↥(Lp F p μ))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid (R := 𝕜)
          { carrier := {f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ}, add_mem' := sorry,
            zero_mem' := sorry, smul_mem' := sorry })))
    f ↔
  AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
Tactic: rw [← SetLike.mem_coe, ← Submodule.mem_carrier, lpMeas, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
rw : f ∈ (↑(lpMeas F 𝕜 m p μ) : Set ↥(Lp F p μ)) ↔ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
rw₁ :
  Membership.mem (γ := Set ↥(Lp F p μ))
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (lpMeas F 𝕜 m p μ)))) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
rw₂ :
  Membership.mem (γ := Set ↥(Lp F p μ))
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid (R := 𝕜)
            { carrier := {f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ}, add_mem' := ⋯,
              zero_mem' := ⋯, smul_mem' := ⋯ })))
      f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ Membership.mem (γ := Submodule 𝕜 ↥(Lp F p μ)) (lpMeas F 𝕜 m p μ) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
have rw₃ : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ ↔ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
Tactic: rw [← SetLike.mem_coe, ← Submodule.mem_carrier, lpMeas, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f
⊢ MemLp (Exists.choose (p := fun (g : α → F) ↦ StronglyMeasurable g ∧ (↑(↑f : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] g) ⋯) p
    (μ.trim hm)
have hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
Tactic: have hf : AEStronglyMeasurable[m] f μ :=
    mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ MemLp (Exists.choose (p := fun (g : α → F) ↦ StronglyMeasurable g ∧ (↑(↑f : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] g) ⋯) p
    (μ.trim hm)
have change : MemLp (AEStronglyMeasurable.mk (↑(↑f : α →ₘ[μ] F) : α → F) hf) p (μ.trim hm)
Tactic: change MemLp (hf.mk f) p (μ.trim hm)