awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ ‖f (I i).1‖ ≤ C

Tactic:
hC _ (hnI.left i hi |>.left)

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ ‖f (I i).1‖ ≤ C

Tactic:
exact hC _ (hnI.left i hi |>.left)

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
h₂ : dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ dist (f (I i).1) (f (I i).2) * D
⊢ dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ D * dist (f (I i).1) (f (I i).2)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
h₂ : 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
⊢ dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ dist (f (I i).1) (f (I i).2) * D

Tactic:
grw [dist_pair_smul]

Premises used: dist_pair_smul
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
h₂ : dist (g (I i).2) 0 ≤ D
⊢ 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

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
h₂ : ‖g (I i).2‖ ≤ D
⊢ dist (g (I i).2) 0 ≤ D

Tactic:
rw [dist_zero_right]

Premises used: dist_zero_right
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ ‖g (I i).2‖ ≤ D

Tactic:
hD _ (hnI.left i hi |>.right)

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ ‖g (I i).2‖ ≤ D

Tactic:
exact hD _ (hnI.left i hi |>.right)

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
f g : ℝ → ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ AbsolutelyContinuousOnInterval (f * g) a b

Tactic:
hf.smul hg

Premises used: AbsolutelyContinuousOnInterval.smul
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
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) < ε
⊢ AbsolutelyContinuousOnInterval f a b

Tactic:
rw [absolutelyContinuousOnInterval_iff]

Premises used: absolutelyContinuousOnInterval_iff
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
⊢ ε / ((↑K : ℝ) + 1) > 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
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) < ε
⊢ ∃ δ > 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:
refine ⟨ε / (K + 1), by positivity, fun (n, I) hnI₁ hnI₂ ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
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
⊢ 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:
apply Finset.sum_le_sum

Premises used: Finset.sum_le_sum
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ (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

Premises used: Ne.symm, not_eq_of_beq_eq_false, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
h₂ h₃ h₄ 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
⊢ 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

Premises used: ENNReal.toReal_mul, dist_edist
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
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
⊢ ∑ 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:
symm
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 = ∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2

Tactic:
Finset.mul_sum _ _ _

Premises used: Finset.mul_sum
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 = ∑ i ∈ Finset.range n, (↑K : ℝ) * dist (I i).1 (I i).2

Tactic:
exact Finset.mul_sum _ _ _

Premises used: Finset.mul_sum
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
ha : 0 ≤ (↑K : ℝ)
⊢ (↑K : ℝ) * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 ≤ (↑K : ℝ) * (ε / ((↑K : ℝ) + 1))

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
hbc : (↑K : ℝ) < (↑K : ℝ) + 1
⊢ (↑K : ℝ) * (ε / ((↑K : ℝ) + 1)) < ((↑K : ℝ) + 1) * (ε / ((↑K : ℝ) + 1))

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
linarith : (↑K : ℝ) + 1 ≤ (↑K : ℝ) → -1 + ((↑K : ℝ) + 1 - (↑K : ℝ)) = 0
⊢ (↑K : ℝ) < (↑K : ℝ) + 1

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 : ℝ) + 1) * (ε / ((↑K : ℝ) + 1)) = ε

Tactic:
field
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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))
_₄ : ((↑K : ℝ) + 1) * (ε / ((↑K : ℝ) + 1)) = ε
⊢ ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 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

Premises used: HDiv.hDiv, Finset.range, HAdd.hAdd, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
hf : ContDiffOn ℝ 1 f (uIcc a b)
⊢ Ne (α := WithTop ℕ∞) 1 0

Tactic:
decide
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
hf : ContDiffOn ℝ 1 f (uIcc a b)
obtain : ∀ (K : ℝ≥0) (hK : LipschitzOnWith K f (uIcc a b)), AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval f a b

Tactic:
obtain ⟨K, hK⟩ := hf.exists_lipschitzOnWith (by decide) (convex_Icc _ _) isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, convex_Icc, ContDiffOn.exists_lipschitzOnWith
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
hf : ContDiffOn ℝ 1 f (uIcc a b)
K : ℝ≥0
hK : LipschitzOnWith K f (uIcc a b)
⊢ AbsolutelyContinuousOnInterval f a b

Tactic:
hK.absolutelyContinuousOnInterval

Premises used: LipschitzOnWith.absolutelyContinuousOnInterval
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
hf : ContDiffOn ℝ 1 f (uIcc a b)
K : ℝ≥0
hK : LipschitzOnWith K f (uIcc a b)
⊢ AbsolutelyContinuousOnInterval f a b

Tactic:
exact hK.absolutelyContinuousOnInterval

Premises used: LipschitzOnWith.absolutelyContinuousOnInterval
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
wlog : ∀ {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hab₀ : a ≤ b), BoundedVariationOn f (uIcc a b)
⊢ BoundedVariationOn f (uIcc a b)

Tactic:
wlog hab₀ : a ≤ b generalizing a b
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
linarith : a < b → b - a + (a - b) = 0
⊢ b ≤ a

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 b a)

Tactic:
specialize @this b a hf.symm (by linarith)

Premises used: AbsolutelyContinuousOnInterval.symm
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hab₀ : ¬a ≤ b
this inr inr₁ inr₂ inr₃ : BoundedVariationOn f (uIcc b a)
⊢ BoundedVariationOn f (uIcc a b)

Tactic:
rwa [uIcc_comm]

Premises used: Set.uIcc_comm
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab₀ : a ≤ b
rw : BoundedVariationOn f (Icc a b)
⊢ BoundedVariationOn f (uIcc a b)

Tactic:
rw [uIcc_of_le hab₀]

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab₀ : a ≤ b
inl : ∀ (hf : AbsolutelyContinuousOnInterval f a a) (hab₀ : a ≤ a), BoundedVariationOn f (Icc a a)
inr : ∀ (hab : a < b), BoundedVariationOn f (Icc a b)
⊢ BoundedVariationOn f (Icc a b)

Tactic:
rcases hab₀.eq_or_lt with rfl | hab

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b : ℝ
f : ℝ → F
a : ℝ
hf : AbsolutelyContinuousOnInterval f a a
hab₀ : a ≤ a
⊢ BoundedVariationOn f (Icc a a)

Tactic:
simp [BoundedVariationOn]

Premises used: BoundedVariationOn
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ ∀ ε > 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

Premises used: absolutelyContinuousOnInterval_iff
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
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) < ε
⊢ a ≤ b

Tactic:
rw [absolutelyContinuousOnInterval_iff] at hf

Premises used: absolutelyContinuousOnInterval_iff
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
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
⊢ a < b

Tactic:
rw [absolutelyContinuousOnInterval_iff] at hf

Premises used: absolutelyContinuousOnInterval_iff
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a_1 b_1 : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
linarith : LE.le (α := ℝ) 1 0 → -1 + HSub.hSub (α := ℝ) 1 0 = 0
⊢ GT.gt (α := ℝ) 1 0

Tactic:
linarith