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 b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1) (f (I i).2) * dist (g (I i).2) 0 ≤ dist (f (I i).1) (f (I i).2) * D
have h₂ : dist (g (I i).2) 0 ≤ D
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (g (I i).2) 0 ≤ D
have h₂ : ‖g (I i).2‖ ≤ D
Tactic: rw [dist_zero_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
⊢ AbsolutelyContinuousOnInterval f a b
have rw : ∀ ε > 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) < ε
Tactic: rw [absolutelyContinuousOnInterval_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 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) < ε
have refine : ∀ (x : ℕ × (ℕ → ℝ × ℝ)) (n : ℕ) (I : ℕ → ℝ × ℝ) (hnI₁ : (n, I) ∈ disjWithin a b)
  (hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)),
  ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) < ε
Tactic: refine ⟨ε / (K + 1), by positivity, fun (n, I) hnI₁ hnI₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2))
    (∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2)
have h : ∀ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
Tactic: apply Finset.sum_le_sum
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
i : ℕ
hi : i ∈ Finset.range (n, I).1
⊢ dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
have this : edist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ENNReal) * edist ((n, I).2 i).1 ((n, I).2 i).2
Tactic: have := hfK (hnI₁.left i hi).left (hnI₁.left i hi).right
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
i : ℕ
hi : i ∈ Finset.range (n, I).1
this : edist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ENNReal) * edist ((n, I).2 i).1 ((n, I).2 i).2
⊢ dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
have this₁ : (edist (f ((n, I).2 i).1) (f ((n, I).2 i).2)).toReal ≤ ((↑K : ENNReal) * edist ((n, I).2 i).1 ((n, I).2 i).2).toReal
Tactic: apply ENNReal.toReal_mono (Ne.symm (not_eq_of_beq_eq_false rfl)) at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
i : ℕ
hi : i ∈ Finset.range (n, I).1
this :
  (edist (f ((n, I).2 i).1) (f ((n, I).2 i).2)).toReal ≤ ((↑K : ENNReal) * edist ((n, I).2 i).1 ((n, I).2 i).2).toReal
⊢ dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
have h : ∀
  (this :
    (edist (f ((n, I).2 i).1) (f ((n, I).2 i).2)).toReal ≤
      (↑K : ENNReal).toReal * (edist ((n, I).2 i).1 ((n, I).2 i).2).toReal),
  dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
Tactic: rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
i : ℕ
hi : i ∈ Finset.range (n, I).1
this :
  (edist (f ((n, I).2 i).1) (f ((n, I).2 i).2)).toReal ≤ ((↑K : ENNReal) * edist ((n, I).2 i).1 ((n, I).2 i).2).toReal
h :
  ∀
    (this :
      (edist (f ((n, I).2 i).1) (f ((n, I).2 i).2)).toReal ≤
        (↑K : ENNReal).toReal * (edist ((n, I).2 i).1 ((n, I).2 i).2).toReal),
    dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
⊢ dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
have h₁ : ∀
  (this :
    dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ENNReal).toReal * (edist ((n, I).2 i).1 ((n, I).2 i).2).toReal),
  dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
Tactic: rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
i : ℕ
hi : i ∈ Finset.range (n, I).1
this :
  (edist (f ((n, I).2 i).1) (f ((n, I).2 i).2)).toReal ≤ ((↑K : ENNReal) * edist ((n, I).2 i).1 ((n, I).2 i).2).toReal
h :
  ∀
    (this :
      (edist (f ((n, I).2 i).1) (f ((n, I).2 i).2)).toReal ≤
        (↑K : ENNReal).toReal * (edist ((n, I).2 i).1 ((n, I).2 i).2).toReal),
    dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
h₁ :
  ∀
    (this :
      dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤
        (↑K : ENNReal).toReal * (edist ((n, I).2 i).1 ((n, I).2 i).2).toReal),
    dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
⊢ dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
have h₂ : ∀ (this : dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ENNReal).toReal * dist ((n, I).2 i).1 ((n, I).2 i).2),
  dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ (↑K : ℝ) * dist (I i).1 (I i).2
Tactic: rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
⊢ ∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2 = (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2
have symm : (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 = ∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
⊢ (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 ≤ (↑K : ℝ) * (ε / ((↑K : ℝ) + 1))
have ha : 0 ≤ (↑K : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
⊢ (↑K : ℝ) * (ε / ((↑K : ℝ) + 1)) < ((↑K : ℝ) + 1) * (ε / ((↑K : ℝ) + 1))
have hbc : (↑K : ℝ) < (↑K : ℝ) + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
⊢ (↑K : ℝ) < (↑K : ℝ) + 1
have linarith : (↑K : ℝ) + 1 ≤ (↑K : ℝ) → -1 + ((↑K : ℝ) + 1 - (↑K : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
⊢ ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) < ε
have _ : LE.le (α := ℝ) (∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2))
  (∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2)
Tactic: calc
    _ ≤ ∑ i ∈ Finset.range n, K * dist (I i).1 (I i).2 := by
      apply Finset.sum_le_sum
      intro i hi
      have := hfK (hnI₁.left i hi).left (hnI₁.left i hi).right
      apply ENNReal.toReal_mono (Ne.symm (not_eq_of_beq_eq_false rfl)) at this
      rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
    _ = K * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 := by symm; exact Finset.mul_sum _ _ _
    _ ≤ K * (ε / (K + 1)) := by gcongr
    _ < (K + 1) * (ε / (K + 1)) := by gcongr; linarith
    _ = ε := by field
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
_ :
  LE.le (α := ℝ) (∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2))
    (∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2)
⊢ ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) < ε
have _₁ : ∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2 = (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2
Tactic: calc
    _ ≤ ∑ i ∈ Finset.range n, K * dist (I i).1 (I i).2 := by
      apply Finset.sum_le_sum
      intro i hi
      have := hfK (hnI₁.left i hi).left (hnI₁.left i hi).right
      apply ENNReal.toReal_mono (Ne.symm (not_eq_of_beq_eq_false rfl)) at this
      rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
    _ = K * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 := by symm; exact Finset.mul_sum _ _ _
    _ ≤ K * (ε / (K + 1)) := by gcongr
    _ < (K + 1) * (ε / (K + 1)) := by gcongr; linarith
    _ = ε := by field
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
_ :
  LE.le (α := ℝ) (∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2))
    (∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2)
_₁ : ∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2 = (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2
⊢ ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) < ε
have _₂ : (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 ≤ (↑K : ℝ) * (ε / ((↑K : ℝ) + 1))
Tactic: calc
    _ ≤ ∑ i ∈ Finset.range n, K * dist (I i).1 (I i).2 := by
      apply Finset.sum_le_sum
      intro i hi
      have := hfK (hnI₁.left i hi).left (hnI₁.left i hi).right
      apply ENNReal.toReal_mono (Ne.symm (not_eq_of_beq_eq_false rfl)) at this
      rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
    _ = K * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 := by symm; exact Finset.mul_sum _ _ _
    _ ≤ K * (ε / (K + 1)) := by gcongr
    _ < (K + 1) * (ε / (K + 1)) := by gcongr; linarith
    _ = ε := by field
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
_ :
  LE.le (α := ℝ) (∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2))
    (∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2)
_₁ : ∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2 = (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2
_₂ : (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 ≤ (↑K : ℝ) * (ε / ((↑K : ℝ) + 1))
⊢ ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) < ε
have _₃ : (↑K : ℝ) * (ε / ((↑K : ℝ) + 1)) < ((↑K : ℝ) + 1) * (ε / ((↑K : ℝ) + 1))
Tactic: calc
    _ ≤ ∑ i ∈ Finset.range n, K * dist (I i).1 (I i).2 := by
      apply Finset.sum_le_sum
      intro i hi
      have := hfK (hnI₁.left i hi).left (hnI₁.left i hi).right
      apply ENNReal.toReal_mono (Ne.symm (not_eq_of_beq_eq_false rfl)) at this
      rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
    _ = K * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 := by symm; exact Finset.mul_sum _ _ _
    _ ≤ K * (ε / (K + 1)) := by gcongr
    _ < (K + 1) * (ε / (K + 1)) := by gcongr; linarith
    _ = ε := by field
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / ((↑K : ℝ) + 1)
_ :
  LE.le (α := ℝ) (∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2))
    (∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2)
_₁ : ∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2 = (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2
_₂ : (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 ≤ (↑K : ℝ) * (ε / ((↑K : ℝ) + 1))
_₃ : (↑K : ℝ) * (ε / ((↑K : ℝ) + 1)) < ((↑K : ℝ) + 1) * (ε / ((↑K : ℝ) + 1))
⊢ ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) < ε
have _₄ : ((↑K : ℝ) + 1) * (ε / ((↑K : ℝ) + 1)) = ε
Tactic: calc
    _ ≤ ∑ i ∈ Finset.range n, K * dist (I i).1 (I i).2 := by
      apply Finset.sum_le_sum
      intro i hi
      have := hfK (hnI₁.left i hi).left (hnI₁.left i hi).right
      apply ENNReal.toReal_mono (Ne.symm (not_eq_of_beq_eq_false rfl)) at this
      rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
    _ = K * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 := by symm; exact Finset.mul_sum _ _ _
    _ ≤ K * (ε / (K + 1)) := by gcongr
    _ < (K + 1) * (ε / (K + 1)) := by gcongr; linarith
    _ = ε := by field
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
hf : ContDiffOn ℝ 1 f (uIcc a b)
⊢ AbsolutelyContinuousOnInterval f a b
have obtain : ∀ (K : ℝ≥0) (hK : LipschitzOnWith K f (uIcc a b)), AbsolutelyContinuousOnInterval f a b
Tactic: obtain ⟨K, hK⟩ := hf.exists_lipschitzOnWith (by decide) (convex_Icc _ _) isCompact_Icc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ BoundedVariationOn f (uIcc a b)
have inr : ∀ (this : ∀ {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hab₀ : a ≤ b), BoundedVariationOn f (uIcc a b))
  (hab₀ : ¬a ≤ b), BoundedVariationOn f (uIcc a b)
Tactic: wlog hab₀ : a ≤ b generalizing a b
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
inr :
  ∀ (this : ∀ {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hab₀ : a ≤ b), BoundedVariationOn f (uIcc a b))
    (hab₀ : ¬a ≤ b), BoundedVariationOn f (uIcc a b)
⊢ BoundedVariationOn f (uIcc a b)
have wlog : ∀ {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hab₀ : a ≤ b), BoundedVariationOn f (uIcc a b)
Tactic: wlog hab₀ : a ≤ b generalizing a b
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
this : ∀ {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hab₀ : a ≤ b), BoundedVariationOn f (uIcc a b)
hab₀ : ¬a ≤ b
⊢ b ≤ a
have linarith : a < b → b - a + (a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
this : ∀ {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hab₀ : a ≤ b), BoundedVariationOn f (uIcc a b)
hab₀ : ¬a ≤ b
⊢ BoundedVariationOn f (uIcc a b)
have this₁ : BoundedVariationOn f (uIcc b a)
Tactic: specialize @this b a hf.symm (by linarith)
Cleared hypotheses: 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 : AbsolutelyContinuousOnInterval f a b
hab₀ : a ≤ b
⊢ BoundedVariationOn f (uIcc a b)
have rw : BoundedVariationOn f (Icc a b)
Tactic: rw [uIcc_of_le hab₀]
-- 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 : AbsolutelyContinuousOnInterval f a b
hab₀ : a ≤ b
⊢ BoundedVariationOn f (Icc a b)
have inl : ∀ (hf : AbsolutelyContinuousOnInterval f a a) (hab₀ : a ≤ a), BoundedVariationOn f (Icc a a)
Tactic: rcases hab₀.eq_or_lt with rfl | hab
Cleared hypotheses: b, hf, hab₀
-- 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 : AbsolutelyContinuousOnInterval f a b
hab₀ : a ≤ b
inl : ∀ (hf : AbsolutelyContinuousOnInterval f a a) (hab₀ : a ≤ a), BoundedVariationOn f (Icc a a)
⊢ BoundedVariationOn f (Icc a b)
have inr : ∀ (hab : a < b), BoundedVariationOn f (Icc a b)
Tactic: rcases hab₀.eq_or_lt with rfl | 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 : AbsolutelyContinuousOnInterval f a b
hab₀ : a ≤ b
hab : a < b
⊢ BoundedVariationOn f (Icc a b)
have 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) < ε
Tactic: rw [absolutelyContinuousOnInterval_iff] at hf
Cleared hypotheses: hf, hab₀, hab
-- 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
⊢ GT.gt (α := ℝ) 1 0
have linarith : LE.le (α := ℝ) 1 0 → -1 + HSub.hSub (α := ℝ) 1 0 = 0
Tactic: linarith
-- 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
⊢ BoundedVariationOn f (Icc a b)
have inr : ∀ (δ : ℝ) (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),
  BoundedVariationOn f (Icc a b)
Tactic: obtain ⟨δ, hδ₁, hδ₂⟩ := hf 1 (by linarith)
-- 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
⊢ 0 < b - a
have linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
Tactic: linarith
-- 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
⊢ BoundedVariationOn f (Icc a b)
have hab₁ : 0 < b - a
Tactic: have hab₁ : 0 < b - a := by linarith