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 * δ'))
x y : ℝ
h_1 : a ≤ x
h_2 : x ≤ y
h_3 : y < x + δ
h_4 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
this : (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ
h :
  Eq (α := ℝ)
    (∑ i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1,
      dist (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1
        ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2)
    (∑ i ∈ Finset.range p.1, ((↑p.2 : ℕ → ℝ) (i + 1) - (↑p.2 : ℕ → ℝ) i))
⊢ ∑ i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1,
      dist (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1
        ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 =
    (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0

Tactic:
rw [← Finset.sum_range_sub]

Premises used: Finset.sum_range_sub
-- 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 * δ'))
x y : ℝ
h_1 : a ≤ x
h_2 : x ≤ y
h_3 : y < x + δ
h_4 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
this : (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ
h :
  Eq (α := ℕ → ℝ)
    (fun (i : ℕ) ↦
      dist (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1
        ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2)
    fun (i : ℕ) ↦ (↑p.2 : ℕ → ℝ) (i + 1) - (↑p.2 : ℕ → ℝ) i
⊢ Eq (α := ℝ)
    (∑ i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1,
      dist (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1
        ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2)
    (∑ i ∈ Finset.range p.1, ((↑p.2 : ℕ → ℝ) (i + 1) - (↑p.2 : ℕ → ℝ) i))

Tactic:
congr
-- 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 * δ'))
x y : ℝ
h_1 : a ≤ x
h_2 : x ≤ y
h_3 : y < x + δ
h_4 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
this : (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ
h :
  ∀ (i : ℕ),
    dist (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1
        ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 =
      (↑p.2 : ℕ → ℝ) (i + 1) - (↑p.2 : ℕ → ℝ) i
⊢ Eq (α := ℕ → ℝ)
    (fun (i : ℕ) ↦
      dist (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1
        ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2)
    fun (i : ℕ) ↦ (↑p.2 : ℕ → ℝ) (i + 1) - (↑p.2 : ℕ → ℝ) i

Tactic:
ext i
-- 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 * δ'))
x y : ℝ
h_1 : a ≤ x
h_2 : x ≤ y
h_3 : y < x + δ
h_4 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
this : (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ
i : ℕ
h :
  0 ≤
    HSub.hSub (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2
      ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1
⊢ dist (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1
      ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 =
    (↑p.2 : ℕ → ℝ) (i + 1) - (↑p.2 : ℕ → ℝ) i

Tactic:
rw [dist_comm, Real.dist_eq, abs_eq_self.mpr]

Premises used: Iff.mpr, dist_comm, Real.dist_eq, abs_eq_self
-- 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
this : (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ
i : ℕ
⊢ i ≤ i + 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
this : (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ
i : ℕ
linarith :
  HSub.hSub (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2
        ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1 <
      0 →
    HSub.hSub (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2
            ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1 -
          0 +
        ((↑p.2 : ℕ → ℝ) i - (↑p.2 : ℕ → ℝ) (i + 1)) =
      0
⊢ 0 ≤
    HSub.hSub (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2
      ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1

Tactic:
linarith [@hp₁ 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
a₁ : (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ
⊢ ∑ i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1,
      dist (α := ℝ) ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1
        ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 <
    δ

Tactic:
suffices p.2.val p.1 - p.2.val 0 < δ by
          convert! this
          rw [← Finset.sum_range_sub]
          congr; ext i
          rw [dist_comm, Real.dist_eq, abs_eq_self.mpr]
          linarith [@hp₁ 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
linarith :
  δ ≤ (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 →
    y - (x + δ) + (δ - ((↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0)) + ((↑p.2 : ℕ → ℝ) p.1 - y) + (x - (↑p.2 : ℕ → ℝ) 0) = 0
⊢ (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ

Tactic:
linarith [mem_Icc.mp (hp₂ p.1), mem_Icc.mp (hp₂ 0)]

Premises used: Prod.fst, Iff.mp, Set.mem_Icc, OfNat.ofNat
-- 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
⊢ LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1

Tactic:
have vf : ∑ i ∈ Finset.range p.1, dist (f (p.2.val i)) (f (p.2.val (i + 1))) < 1 := by
      apply hδ₂ (p.1, (fun i ↦ (p.2.val i, p.2.val (i + 1))))
      · constructor
        · have : Icc x y ⊆ uIcc a b := by rw [uIcc_of_le hab₀]; gcongr
          intro i hi
          constructor <;> exact this (hp₂ _)
        · rw [PairwiseDisjoint]
          convert! hp₁.pairwise_disjoint_on_Ioc_succ.set_pairwise (Finset.range p.1) using 3
          rw [uIoc_of_le (hp₁ (by lia)), Nat.succ_eq_succ]
      · suffices p.2.val p.1 - p.2.val 0 < δ by
          convert! this
          rw [← Finset.sum_range_sub]
          congr; ext i
          rw [dist_comm, Real.dist_eq, abs_eq_self.mpr]
          linarith [@hp₁ i (i + 1) (by lia)]
        linarith [mem_Icc.mp (hp₂ p.1), mem_Icc.mp (hp₂ 0)]
-- 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
⊢ ∀ a ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (a + 1))) (f ((↑p.2 : ℕ → ℝ) a)) ≠ ⊤

Tactic:
simp [edist_ne_top]

Premises used: edist_ne_top
-- 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
rw :
  Eq (α := ℝ) (∑ a ∈ Finset.range p.1, (edist (f ((↑p.2 : ℕ → ℝ) (a + 1))) (f ((↑p.2 : ℕ → ℝ) a))).toReal)
    (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1))))
⊢ ENNReal.toReal (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i))) =
    ∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))

Tactic:
rw [ENNReal.toReal_sum (by simp [edist_ne_top])]

Premises used: ENNReal.toReal_sum
-- 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
simp_rw :
  Eq (α := ℝ) (∑ x_1 ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) (x_1 + 1))) (f ((↑p.2 : ℕ → ℝ) x_1)))
    (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1))))
⊢ Eq (α := ℝ) (∑ a ∈ Finset.range p.1, (edist (f ((↑p.2 : ℕ → ℝ) (a + 1))) (f ((↑p.2 : ℕ → ℝ) a))).toReal)
    (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1))))

Tactic:
simp_rw [← dist_edist]

Premises used: dist_edist
-- 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
e_f :
  Eq (α := ℕ → ℝ) (fun (x_1 : ℕ) ↦ dist (f ((↑p.2 : ℕ → ℝ) (x_1 + 1))) (f ((↑p.2 : ℕ → ℝ) x_1))) fun (i : ℕ) ↦
    dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))
⊢ Eq (α := ℝ) (∑ x_1 ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) (x_1 + 1))) (f ((↑p.2 : ℕ → ℝ) x_1)))
    (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1))))

Tactic:
congr
-- 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
e_f :
  ∀ (i : ℕ),
    dist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i)) = dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))
⊢ Eq (α := ℕ → ℝ) (fun (x_1 : ℕ) ↦ dist (f ((↑p.2 : ℕ → ℝ) (x_1 + 1))) (f ((↑p.2 : ℕ → ℝ) x_1))) fun (i : ℕ) ↦
    dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))

Tactic:
ext i
-- 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 * δ'))
x y : ℝ
h : a ≤ x
h_1 : x ≤ y
h_2 : y < x + δ
h_3 : y ≤ b
p : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone (↑p.2 : ℕ → ℝ)
hp₂ : ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
i : ℕ
e_f e_f₁ :
  dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1))) = dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))
⊢ dist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i)) = dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))

Tactic:
nth_rw 1 [dist_comm]

Premises used: dist_comm