awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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
⊢ (p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))) ∈ disjWithin a b
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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
have rw : Icc x y ⊆ Icc a b
Tactic: rw [uIcc_of_le hab₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
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
⊢ ∀ 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
have this : Icc x y ⊆ uIcc a b
Tactic: have : Icc x y ⊆ uIcc a b := by rw [uIcc_of_le hab₀]; gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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 ∧
    ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 ∈ uIcc a b
have a₁ : ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).1 ∈ uIcc a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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
⊢ ((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
have a₂ : ((p.1, fun (i : ℕ) ↦ ((↑p.2 : ℕ → ℝ) i, (↑p.2 : ℕ → ℝ) (i + 1))).2 i).2 ∈ uIcc a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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, 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)
have 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))
Tactic: convert! hp₁.pairwise_disjoint_on_Ioc_succ.set_pairwise (Finset.range p.1) using 3
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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 : ℕ
⊢ 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))
have h : Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) (x_1 + 1)) = Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) (Order.succ x_1))
Tactic: rw [uIoc_of_le (hp₁ (by lia)), Nat.succ_eq_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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))
⊢ 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))
have h₁ : Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) (x_1 + 1)) = Ioc ((↑p.2 : ℕ → ℝ) x_1) ((↑p.2 : ℕ → ℝ) x_1.succ)
Tactic: rw [uIoc_of_le (hp₁ (by lia)), Nat.succ_eq_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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 ∈ 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 <
    δ
have 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
Tactic: convert! this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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 ∈ 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
have 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))
Tactic: rw [← Finset.sum_range_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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 < δ
⊢ 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))
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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 < δ
⊢ 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
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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 : ℕ
⊢ 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
have 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
Tactic: rw [dist_comm, Real.dist_eq, abs_eq_self.mpr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
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 : ℕ
⊢ 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
have 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
Tactic: linarith [@hp₁ i (i + 1) (by lia)]