awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 ∈ Finset.range (n, I).1, MeasurableSet (uIoc ((n, I).2 i).1 ((n, I).2 i).2)

Tactic:
simp +contextual [uIoc]

Premises used: Set.uIoc
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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‖)
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))
⊢ ∑ 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:
rw [← integral_norm_eq_lintegral_enorm (h.aestronglyMeasurable_restrict_uIoc.restrict),
      integral_biUnion_finset _ (by simp +contextual [uIoc]) hnI2]

Premises used: MeasureTheory.integral_norm_eq_lintegral_enorm, MeasureTheory.integral_biUnion_finset, MeasureTheory.AEStronglyMeasurable.restrict, IntervalIntegrable.aestronglyMeasurable_restrict_uIoc
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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‖)

Tactic:
Finset.sum_le_sum (fun i hi ↦ ?_)

Premises used: Finset.sum_le_sum
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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₁ :
  ∀ (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‖
⊢ 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:
refine Finset.sum_le_sum (fun i hi ↦ ?_)

Premises used: Finset.sum_le_sum
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
apply : uIoc c (I i).1 ⊆ uIoc a b
⊢ IntervalIntegrable f volume c (I i).1

Tactic:
apply IntervalIntegrable.mono_set' h

Premises used: IntervalIntegrable.mono_set'
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ uIoc c (I i).1 ⊆ uIoc a b

Tactic:
grind [uIoc, uIcc]

Premises used: Set.uIoc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
apply : uIoc c (I i).2 ⊆ uIoc a b
⊢ IntervalIntegrable f volume c (I i).2

Tactic:
apply IntervalIntegrable.mono_set' h

Premises used: IntervalIntegrable.mono_set'
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ uIoc c (I i).2 ⊆ uIoc a b

Tactic:
grind [uIoc, uIcc]

Premises used: Set.uIoc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
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‖)
⊢ 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:
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]

Premises used: abs_neg, intervalIntegral.abs_intervalIntegral_eq, Finset.mem_range, intervalIntegral.integral_symm, MeasureTheory.Measure.restrict_restrict_of_subset, Real.dist_eq, Iff.mp, AbsolutelyContinuousOnInterval.uIoc_subset_of_mem_disjWithin, intervalIntegral.integral_interval_sub_left
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ 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:
abs_integral_le_integral_abs

Premises used: MeasureTheory.abs_integral_le_integral_abs
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ 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:
exact abs_integral_le_integral_abs

Premises used: MeasureTheory.abs_integral_le_integral_abs
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ 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)
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
h₁ : @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ ‖f x‖) (Measure.restrict volume (uIoc (I i).1 (I i).2))
⊢ @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))

Tactic:
rw [Measure.restrict_restrict_of_subset h_subset]

Premises used: MeasureTheory.Measure.restrict_restrict_of_subset
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 volume (uIoc (I i).1 (I i).2))

Tactic:
IntegrableOn.mono_set h.def'.norm h_subset |>.integrable

Premises used: MeasureTheory.IntegrableOn.mono_set, IntervalIntegrable.def', MeasureTheory.IntegrableOn.integrable, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 volume (uIoc (I i).1 (I i).2))

Tactic:
exact IntegrableOn.mono_set h.def'.norm h_subset |>.integrable

Premises used: MeasureTheory.IntegrableOn.mono_set, IntervalIntegrable.def', MeasureTheory.IntegrableOn.integrable, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
inst_1 : MetrizableSpace β
m m0 : MeasurableSpace α
μ : Measure α
f g : α → β
hm : m ≤ m0
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm ↔ f =ᶠ[ae μ] g

Tactic:
(hfm.stronglyMeasurable_mk.ae_eq_trim_iff hm hgm.stronglyMeasurable_mk).trans
    ⟨fun h => hfm.ae_eq_mk.trans (h.trans hgm.ae_eq_mk.symm), fun h =>
      hfm.ae_eq_mk.symm.trans (h.trans hgm.ae_eq_mk)⟩

Premises used: Filter.EventuallyEq.trans, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Iff.intro, Iff.trans, MeasureTheory.StronglyMeasurable.ae_eq_trim_iff, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
mα : MeasurableSpace α
x : MeasurableSpace γ
f : α → β
μ : Measure γ
g : γ → α
hf : AEStronglyMeasurable (m₀ := mα) f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable (f ∘ g) μ

Tactic:
⟨hf.mk f ∘ g, hf.stronglyMeasurable_mk.comp_measurable (measurable_iff_comap_le.mpr le_rfl),
    ae_eq_comp hg hf.ae_eq_mk⟩

Premises used: Iff.mpr, le_rfl, Function.comp, measurable_iff_comap_le, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.ae_eq_comp, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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) μ
rw₂ rw₃ : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ ↔ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ

Tactic:
rw [← AddSubgroup.mem_carrier, lpMeasSubgroup, Set.mem_setOf_eq]

Premises used: MeasureTheory.lpMeasSubgroup, Set.mem_setOf_eq, AddSubgroup.mem_carrier