awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
      LT.lt (α := ℝ) (∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ / (b - a)
δ' : ℝ := (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hδ₃ : δ' < δ
h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'
v_sum :
  eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
h : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 = (↑(i + 1) : ℝ)
⊢ a + (↑i : ℝ) * δ' ≤ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'

Tactic:
convert! h_mono (show i ≤ i + 1 by lia)
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
      LT.lt (α := ℝ) (∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ / (b - a)
δ' : ℝ := (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hδ₃ : δ' < δ
h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'
v_sum :
  eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
h h₁ h₂ h₃ : i + 1 = i + 1
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 = (↑(i + 1) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
      LT.lt (α := ℝ) (∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ / (b - a)
δ' : ℝ := (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hδ₃ : δ' < δ
h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'
v_sum :
  eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
inr : a + (↑i : ℝ) * δ' + 1 * δ' < a + (↑i : ℝ) * δ' + δ
⊢ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ' < a + (↑i : ℝ) * δ' + δ

Tactic:
rw [add_mul, ← add_assoc]

Premises used: add_mul, add_assoc
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
      LT.lt (α := ℝ) (∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ / (b - a)
δ' : ℝ := (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hδ₃ : δ' < δ
h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'
v_sum :
  eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ a + (↑i : ℝ) * δ' + 1 * δ' < a + (↑i : ℝ) * δ' + δ

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
      LT.lt (α := ℝ) (∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ / (b - a)
δ' : ℝ := (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hδ₃ : δ' < δ
h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'
v_sum :
  eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ i + 1 ≤ n + 1

Tactic:
lia
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
      LT.lt (α := ℝ) (∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ / (b - a)
δ' : ℝ := (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hδ₃ : δ' < δ
h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'
v_sum :
  eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
h : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 = (↑(i + 1) : ℝ)
h₁ : b = (fun (i : ℕ) ↦ a + (↑i : ℝ) * δ') (n + 1)
⊢ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ' ≤ b

Tactic:
convert! h_mono (show i + 1 ≤ n + 1 by lia)
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
      LT.lt (α := ℝ) (∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ / (b - a)
δ' : ℝ := (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hδ₃ : δ' < δ
h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'
v_sum :
  eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
h : b = a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ((b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ b = (fun (i : ℕ) ↦ a + (↑i : ℝ) * δ') (n + 1)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, δ']

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
      LT.lt (α := ℝ) (∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ / (b - a)
δ' : ℝ := (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hδ₃ : δ' < δ
h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'
v_sum :
  eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ b = a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ((b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
field
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → DifferentiableAt ℝ f x

Tactic:
hf.boundedVariationOn.ae_differentiableAt_of_mem_uIcc

Premises used: AbsolutelyContinuousOnInterval.boundedVariationOn, BoundedVariationOn.ae_differentiableAt_of_mem_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
⊢ Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
have : Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0) :=
    tendsto_setLIntegral_zero
    (ne_of_lt <| intervalIntegrable_iff.mp h |>.hasFiniteIntegral)
    (tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero _ _)
-- 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 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ Ne (α := ENNReal) 0 ⊤

Tactic:
simp
-- 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 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
have := ENNReal.toReal_zero ▸ (ENNReal.continuousAt_toReal (by simp)).tendsto.comp this
-- 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 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in c..x, f v) a b

Tactic:
squeeze_zero' ?_ ?_ this

Premises used: AbsolutelyContinuousOnInterval, squeeze_zero'
-- 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 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
refine_1 :
  ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    LE.le (α := ℝ) 0
      (∑ i ∈ Finset.range t.1,
        dist (α := ℝ) ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).1)
          ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).2))
refine_2 :
  ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ i ∈ Finset.range t.1,
        dist (α := ℝ) ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).1)
          ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).2) ≤
      (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)) t
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in c..x, f v) a b

Tactic:
refine squeeze_zero' ?_ ?_ this

Premises used: squeeze_zero'
-- 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 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
refine_1 :
  ∀ (n : ℕ) (I : ℕ → ℝ × ℝ),
    LE.le (α := ℝ) 0
      (∑ i ∈ Finset.range (n, I).1,
        dist (α := ℝ) (∫ (v : ℝ) in c..((n, I).2 i).1, f v) (∫ (v : ℝ) in c..((n, I).2 i).2, f v))
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    LE.le (α := ℝ) 0
      (∑ i ∈ Finset.range t.1,
        dist (α := ℝ) ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).1)
          ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).2))

Tactic:
filter_upwards with (n, I)
-- 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 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
n : ℕ
I : ℕ → ℝ × ℝ
⊢ LE.le (α := ℝ) 0
    (∑ i ∈ Finset.range (n, I).1,
      dist (α := ℝ) (∫ (v : ℝ) in c..((n, I).2 i).1, f v) (∫ (v : ℝ) in c..((n, I).2 i).2, f v))

Tactic:
Finset.sum_nonneg (fun _ _ ↦ dist_nonneg)

Premises used: dist_nonneg, Finset.sum_nonneg
-- 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 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
n : ℕ
I : ℕ → ℝ × ℝ
⊢ LE.le (α := ℝ) 0
    (∑ i ∈ Finset.range (n, I).1,
      dist (α := ℝ) (∫ (v : ℝ) in c..((n, I).2 i).1, f v) (∫ (v : ℝ) in c..((n, I).2 i).2, f v))

Tactic:
exact Finset.sum_nonneg (fun _ _ ↦ dist_nonneg)

Premises used: dist_nonneg, Finset.sum_nonneg
-- 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 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
refine_2 :
  ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ x ∈ Finset.range t.1, dist (α := ℝ) (∫ (v : ℝ) in c..(t.2 x).1, f v) (∫ (v : ℝ) in c..(t.2 x).2, f v) ≤
      (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range t.1, uIoc (t.2 i).1 (t.2 i).2,
          ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ i ∈ Finset.range t.1,
        dist (α := ℝ) ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).1)
          ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).2) ≤
      (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)) t

Tactic:
simp only [comp_apply, s]

Premises used: Function.comp_apply
-- 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 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ ∀ᶠ (x : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter, x ∈ disjWithin a b → x ∈ disjWithin a b

Tactic:
simp
-- 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 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b

Tactic:
have : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
      E ∈ disjWithin a b :=
    eventually_inf_principal.mpr (by simp)
-- 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
h₁ :
  ∀ (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
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ x ∈ Finset.range t.1, dist (α := ℝ) (∫ (v : ℝ) in c..(t.2 x).1, f v) (∫ (v : ℝ) in c..(t.2 x).2, f v) ≤
      (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range t.1, uIoc (t.2 i).1 (t.2 i).2,
          ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal

Tactic:
filter_upwards [this] with (n, I) hnI
-- 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
⊢ ∀ 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
-- 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
⊢ (↑(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
-- 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₁ :
  ∑ 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
⊢ ∑ 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

Tactic:
simp only