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
⊢ ∑ 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 a₁ : (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ
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)]
-- 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
⊢ (↑p.2 : ℕ → ℝ) p.1 - (↑p.2 : ℕ → ℝ) 0 < δ
have 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
Tactic: linarith [mem_Icc.mp (hp₂ p.1), mem_Icc.mp (hp₂ 0)]
-- 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
⊢ LE.le (α := ENNReal) (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i))) 1
have vf : 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)]
-- 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
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 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)))
have 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))))
Tactic: rw [ENNReal.toReal_sum (by simp [edist_ne_top])]
-- 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
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 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))))
have 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))))
Tactic: simp_rw [← dist_edist]
-- 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
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 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))))
have 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)))
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
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 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)))
have e_f : ∀ (i : ℕ),
  dist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i)) = dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))
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
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
i : ℕ
⊢ dist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i)) = dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))
have e_f : dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1))) = dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))
Tactic: nth_rw 1 [dist_comm]
-- 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
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
⊢ LE.le (α := ENNReal) (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i))) 1
have veq : 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: have veq : (∑ i ∈ Finset.range p.1, edist (f (p.2.val (i + 1))) (f (p.2.val i))).toReal =
        ∑ i ∈ Finset.range p.1, dist (f (p.2.val i)) (f (p.2.val (i + 1))) := by
      rw [ENNReal.toReal_sum (by simp [edist_ne_top])]
      simp_rw [← dist_edist]; congr; ext i; nth_rw 1 [dist_comm]
-- 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
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
veq :
  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)))
⊢ LE.le (α := ENNReal) (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i))) 1
have not_top : Ne (α := ENNReal) (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i))) ⊤
Tactic: have not_top : ∑ i ∈ Finset.range p.1, edist (f (p.2.val (i + 1))) (f (p.2.val i)) ≠ ⊤ := by
      simp [edist_ne_top]
-- 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
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
veq :
  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)))
not_top : Ne (α := ENNReal) (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i))) ⊤
⊢ LE.le (α := ENNReal) (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i))) 1
have rw : ENNReal.ofReal (ENNReal.toReal (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i)))) ≤ 1
Tactic: rw [← ENNReal.ofReal_toReal not_top]
-- 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
vf : LT.lt (α := ℝ) (∑ i ∈ Finset.range p.1, dist (f ((↑p.2 : ℕ → ℝ) i)) (f ((↑p.2 : ℕ → ℝ) (i + 1)))) 1
veq :
  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)))
not_top : Ne (α := ENNReal) (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i))) ⊤
⊢ ENNReal.ofReal (ENNReal.toReal (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → ℝ) (i + 1))) (f ((↑p.2 : ℕ → ℝ) i)))) ≤
    1
have h : 1 = ENNReal.ofReal 1
Tactic: convert! ENNReal.ofReal_le_ofReal (veq.symm ▸ vf.le)
-- 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 * δ'))
⊢ BoundedVariationOn f (Icc a b)
have v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
Tactic: have v_each (x y : ℝ) (_ : a ≤ x) (_ : x ≤ y) (_ : y < x + δ) (_ : y ≤ b) :
      eVariationOn f (Icc x y) ≤ 1 := by
    simp only [eVariationOn, iSup_le_iff]
    intro p
    obtain ⟨hp₁, hp₂⟩ := p.2.property
    -- Focus on a partition `p` of `[x, y]` and show its variation with `f` is `≤ 1`.
    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)]
    -- Reduce edist in the goal to dist and clear up
    have veq : (∑ i ∈ Finset.range p.1, edist (f (p.2.val (i + 1))) (f (p.2.val i))).toReal =
        ∑ i ∈ Finset.range p.1, dist (f (p.2.val i)) (f (p.2.val (i + 1))) := by
      rw [ENNReal.toReal_sum (by simp [edist_ne_top])]
      simp_rw [← dist_edist]; congr; ext i; nth_rw 1 [dist_comm]
    have not_top : ∑ i ∈ Finset.range p.1, edist (f (p.2.val (i + 1))) (f (p.2.val i)) ≠ ⊤ := by
      simp [edist_ne_top]
    rw [← ENNReal.ofReal_toReal not_top]
    convert! ENNReal.ofReal_le_ofReal (veq.symm ▸ vf.le)
    simp
-- 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 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
⊢ BoundedVariationOn f (Icc a b)
have inr : ∀ x < n + 1, ¬eVariationOn f (Icc (a + (↑x : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * δ')) = ⊤
Tactic: simp only [BoundedVariationOn, v_sum, ne_eq, ENNReal.sum_eq_top, Finset.mem_range, not_exists,
    not_and]