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 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ ¬eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ')) = ⊤
have inr : eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ')) ≤ 1
Tactic: suffices eVariationOn f (Icc (a + i * δ') (a + (i + 1) * δ')) ≤ 1 from
    fun hC ↦ by simp [hC] at 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 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ')) ≤ 1
have inr : a ≤ a + (↑i : ℝ) * δ'
Tactic: apply v_each
-- 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
i : ℕ
hi : i < n + 1
inr : a ≤ a + (↑i : ℝ) * δ'
⊢ eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ')) ≤ 1
have inr₁ : a + (↑i : ℝ) * δ' ≤ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'
Tactic: apply v_each
-- 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
i : ℕ
hi : i < n + 1
inr : a ≤ a + (↑i : ℝ) * δ'
inr₁ : a + (↑i : ℝ) * δ' ≤ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'
⊢ eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ')) ≤ 1
have inr₂ : a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ' < a + (↑i : ℝ) * δ' + δ
Tactic: apply v_each
-- 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
i : ℕ
hi : i < n + 1
inr : a ≤ a + (↑i : ℝ) * δ'
inr₁ : a + (↑i : ℝ) * δ' ≤ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'
inr₂ : a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ' < a + (↑i : ℝ) * δ' + δ
⊢ eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ')) ≤ 1
have inr₃ : a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ' ≤ b
Tactic: apply v_each
-- 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
i : ℕ
hi : i < n + 1
⊢ a ≤ a + (↑i : ℝ) * δ'
have h : a = (fun (i : ℕ) ↦ a + (↑i : ℝ) * δ') 0
Tactic: convert! h_mono (show 0 ≤ i 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 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ a + (↑i : ℝ) * δ' ≤ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'
have h : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 = (↑(i + 1) : ℝ)
Tactic: convert! h_mono (show 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 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 = (↑(i + 1) : ℝ)
have h : i + 1 = i + 1
Tactic: norm_cast
-- 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
i : ℕ
hi : i < n + 1
⊢ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ' < a + (↑i : ℝ) * δ' + δ
have inr : a + (↑i : ℝ) * δ' + 1 * δ' < a + (↑i : ℝ) * δ' + δ
Tactic: rw [add_mul, ← add_assoc]
-- 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
i : ℕ
hi : i < n + 1
⊢ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ' ≤ b
have h : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 = (↑(i + 1) : ℝ)
Tactic: convert! h_mono (show i + 1 ≤ n + 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 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
h : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 = (↑(i + 1) : ℝ)
⊢ a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ' ≤ b
have h₁ : b = (fun (i : ℕ) ↦ a + (↑i : ℝ) * δ') (n + 1)
Tactic: convert! h_mono (show i + 1 ≤ n + 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 * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ b = (fun (i : ℕ) ↦ a + (↑i : ℝ) * δ') (n + 1)
have h : b = a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ((b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: simp only [Nat.cast_add, Nat.cast_one, δ']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in c..x, f v) a b
have this : Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
  (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
Tactic: have : Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0) :=
    tendsto_setLIntegral_zero
    (ne_of_lt <| intervalIntegrable_iff.mp h |>.hasFiniteIntegral)
    (tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in c..x, f v) a b
have this₁ : Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
  (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
Tactic: have := ENNReal.toReal_zero ▸ (ENNReal.continuousAt_toReal (by simp)).tendsto.comp this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in c..x, f v) a b
have refine_1 : ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
  LE.le (α := ℝ) 0
    (∑ i ∈ Finset.range t.1,
      dist (α := ℝ) ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).1)
        ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).2))
Tactic: refine squeeze_zero' ?_ ?_ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
refine_1 :
  ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    LE.le (α := ℝ) 0
      (∑ i ∈ Finset.range t.1,
        dist (α := ℝ) ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).1)
          ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).2))
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ ∫ (v : ℝ) in c..x, f v) a b
have refine_2 : ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
  ∑ i ∈ Finset.range t.1,
      dist (α := ℝ) ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).1)
        ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).2) ≤
    (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)) t
Tactic: refine squeeze_zero' ?_ ?_ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    LE.le (α := ℝ) 0
      (∑ i ∈ Finset.range t.1,
        dist (α := ℝ) ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).1)
          ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).2))
have refine_1 : ∀ (n : ℕ) (I : ℕ → ℝ × ℝ),
  LE.le (α := ℝ) 0
    (∑ i ∈ Finset.range (n, I).1,
      dist (α := ℝ) (∫ (v : ℝ) in c..((n, I).2 i).1, f v) (∫ (v : ℝ) in c..((n, I).2 i).2, f v))
Tactic: filter_upwards with (n, I)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ i ∈ Finset.range t.1,
        dist (α := ℝ) ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).1)
          ((fun (x : ℝ) ↦ (∫ (v : ℝ) in c..x, f v : ℝ)) (t.2 i).2) ≤
      (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)) t
have refine_2 : ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
  ∑ x ∈ Finset.range t.1, dist (α := ℝ) (∫ (v : ℝ) in c..(t.2 x).1, f v) (∫ (v : ℝ) in c..(t.2 x).2, f v) ≤
    (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range t.1, uIoc (t.2 i).1 (t.2 i).2, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
Tactic: simp only [comp_apply, s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ x ∈ Finset.range t.1, dist (α := ℝ) (∫ (v : ℝ) in c..(t.2 x).1, f v) (∫ (v : ℝ) in c..(t.2 x).2, f v) ≤
      (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range t.1, uIoc (t.2 i).1 (t.2 i).2,
          ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
have this₁ : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
Tactic: have : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
      E ∈ disjWithin a b :=
    eventually_inf_principal.mpr (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : (E : ℕ × (ℕ → ℝ × ℝ)) → Set ℝ := fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this_1 :
  Tendsto (β := ENNReal) (fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this_2 :
  Tendsto (ENNReal.toReal ∘ fun (i : ℕ × (ℕ → ℝ × ℝ)) ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ x ∈ Finset.range t.1, dist (α := ℝ) (∫ (v : ℝ) in c..(t.2 x).1, f v) (∫ (v : ℝ) in c..(t.2 x).2, f v) ≤
      (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range t.1, uIoc (t.2 i).1 (t.2 i).2,
          ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
have h₁ : ∀ (n : ℕ) (I : ℕ → ℝ × ℝ) (hnI : (n, I) ∈ disjWithin a b),
  ∑ x ∈ Finset.range (n, I).1,
      dist (α := ℝ) (∫ (v : ℝ) in c..((n, I).2 x).1, f v) (∫ (v : ℝ) in c..((n, I).2 x).2, f v) ≤
    (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range (n, I).1, uIoc ((n, I).2 i).1 ((n, I).2 i).2,
        ‖f x‖ₑ ∂Measure.restrict volume (uIoc a b)).toReal
Tactic: filter_upwards [this] with (n, I) hnI