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 : 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 : ℕ → ℝ)
⊢ ∀ (i : ℕ), (↑p.2 : ℕ → ℝ) i ∈ Icc x y

Tactic:
obtain ⟨hp₁, hp₂⟩ := p.2.property

Premises used: Prod.snd, Subtype.property
-- 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.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))) ∈ disjWithin a b
a₂ :
  ∑ 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 <
    δ
⊢ LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1

Tactic:
apply hδ₂ (p.1, (fun i ↦ (p.2.val i, p.2.val (i + 1))))

Premises used: Prod.mk, Prod.fst, HAdd.hAdd, OfNat.ofNat, Subtype.val, Prod.snd
-- 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₁ :
  ∀ i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1,
    ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1 ∈ uIcc a b ∧
      ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 ∈ uIcc a b
a₂ :
  (↑(Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1) : Set ℕ).PairwiseDisjoint (α :=
    Set ℝ) fun (i : ℕ) ↦
    uIoc ((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.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))) ∈ disjWithin a b

Tactic:
constructor
-- 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
rw : Icc x y ⊆ Icc a b
⊢ Icc x y ⊆ uIcc a b

Tactic:
rw [uIcc_of_le hab₀]

Premises used: Set.uIcc_of_le
-- 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
⊢ Icc x y ⊆ Icc a b

Tactic:
gcongr
-- 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
⊢ Icc x y ⊆ uIcc a b

Tactic:
have : Icc x y ⊆ uIcc a b := by rw [uIcc_of_le hab₀]; gcongr
-- 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 : Icc x y ⊆ uIcc a b
i : ℕ
hi : i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1
a₁ : ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1 ∈ uIcc a b
a₂ : ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 ∈ uIcc a b
⊢ ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1 ∈ uIcc a b ∧
    ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 ∈ uIcc a b

Tactic:
constructor
-- 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 : Icc x y ⊆ uIcc a b
i : ℕ
hi : i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1
⊢ ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1 ∈ uIcc a b

Tactic:
this (hp₂ _)
-- 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 : Icc x y ⊆ uIcc a b
i : ℕ
hi : i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1
⊢ ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1 ∈ uIcc a b

Tactic:
exact this (hp₂ _)
-- 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 : Icc x y ⊆ uIcc a b
i : ℕ
hi : i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1
⊢ ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 ∈ uIcc a b

Tactic:
this (hp₂ _)
-- 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 : Icc x y ⊆ uIcc a b
i : ℕ
hi : i ∈ Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1
⊢ ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 ∈ uIcc a b

Tactic:
exact this (hp₂ _)
-- 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
⊢ (↑(Finset.range p.1) : Set ℕ).Pairwise
    (onFun (β := Set ℝ) Disjoint fun (n : ℕ) ↦ Ioc ((↑p.2 : ℕ → ℝ) n) ((↑p.2 : ℕ → ℝ) (Order.succ n)))

Tactic:
hp₁.pairwise_disjoint_on_Ioc_succ.set_pairwise (Finset.range p.1)

Premises used: Prod.fst, Finset.range, SetLike.coe, Monotone.pairwise_disjoint_on_Ioc_succ, Pairwise.set_pairwise
-- 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
h :
  ∀ (x_1 : ℕ),
    uIoc ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 x_1).1
        ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 x_1).2 =
      Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) (Order.succ x_1))
⊢ (↑(Finset.range (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).1) : Set ℕ).Pairwise
    (onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦
      uIoc ((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:
convert! hp₁.pairwise_disjoint_on_Ioc_succ.set_pairwise (Finset.range p.1) using 3

Premises used: Prod.fst, Finset.range, SetLike.coe, Monotone.pairwise_disjoint_on_Ioc_succ, Pairwise.set_pairwise
-- 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
x_1 : ℕ
⊢ x_1 ≤ x_1 + 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_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
x_1 : ℕ
h : Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) (x_1 + 1)) = Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) (Order.succ x_1))
h₁ h₂ : Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) (x_1 + 1)) = Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) x_1.succ)
⊢ uIoc ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 x_1).1
      ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 x_1).2 =
    Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) (Order.succ x_1))

Tactic:
rw [uIoc_of_le (hp₁ (by lia)), Nat.succ_eq_succ]

Premises used: Nat.succ_eq_succ, Set.uIoc_of_le
-- 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 < δ
⊢ (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ

Tactic:
this
-- 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 ∈ 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
⊢ ∑ 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:
convert! this