awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ BoundedVariationOn f (Icc a b)

Tactic:
obtain ⟨δ, hδ₁, hδ₂⟩ := hf 1 (by linarith)

Premises used: OfNat.ofNat
-- 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
δ : ℝ
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
linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
⊢ 0 < b - a

Tactic:
linarith
-- 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
δ : ℝ
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

Tactic:
have hab₁ : 0 < b - a := by linarith
-- 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
δ : ℝ
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
inr : ∀ (n : ℕ) (hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ / (b - a)), BoundedVariationOn f (Icc a b)
⊢ BoundedVariationOn f (Icc a b)

Tactic:
obtain ⟨n, hn⟩ := exists_nat_one_div_lt (div_pos hδ₁ hab₁)

Premises used: exists_nat_one_div_lt, div_pos
-- 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
δ : ℝ
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
dsimp : (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ
⊢ δ' < δ

Tactic:
dsimp only [δ']
-- 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
δ : ℝ
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
⊢ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (b - a) < δ / (b - a) * (b - a)

Tactic:
mul_lt_mul_of_pos_right hn hab₁

Premises used: mul_lt_mul_of_pos_right
-- 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
δ : ℝ
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 : (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (b - a)
h₁ : δ = δ / (b - a) * (b - a)
⊢ (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < δ

Tactic:
convert! mul_lt_mul_of_pos_right hn hab₁ using 1

Premises used: mul_lt_mul_of_pos_right
-- 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
δ : ℝ
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
⊢ (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (b - a)

Tactic:
field
-- 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
δ : ℝ
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
⊢ δ = δ / (b - a) * (b - a)

Tactic:
field
-- 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
δ : ℝ
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
⊢ δ' < δ

Tactic:
have hδ₃ : δ' < δ := by
    dsimp only [δ']
    convert! mul_lt_mul_of_pos_right hn hab₁ using 1 <;> field
-- 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
δ : ℝ
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δ₃ : δ' < δ
hf₁ : Monotone (β := ℝ) fun (x : ℕ) ↦ (↑x : ℝ) * δ'
⊢ Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'

Tactic:
apply Monotone.const_add

Premises used: Monotone.const_add
-- 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
δ : ℝ
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δ₃ : δ' < δ
hf₁ : 0 ≤ δ'
⊢ Monotone (β := ℝ) fun (x : ℕ) ↦ (↑x : ℝ) * δ'

Tactic:
apply Monotone.mul_const Nat.mono_cast

Premises used: Monotone.mul_const, Nat.mono_cast
-- 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
δ : ℝ
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δ₃ : δ' < δ
hf₁ : 0 ≤ (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ 0 ≤ δ'

Tactic:
simp only [δ']
-- 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
δ : ℝ
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δ₃ : δ' < δ
⊢ 0 ≤ (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
div_nonneg ?_ ?_

Premises used: div_nonneg
-- 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
δ : ℝ
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δ₃ : δ' < δ
hf₁ : 0 ≤ b - a
hf₂ : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ 0 ≤ (b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
refine div_nonneg ?_ ?_

Premises used: div_nonneg
-- 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
δ : ℝ
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δ₃ : δ' < δ
linarith : b - a < 0 → a - b + (b - a - 0) = 0
⊢ 0 ≤ b - a

Tactic:
linarith
-- 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
δ : ℝ
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δ₃ : δ' < δ
linarith :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < 0 → -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 0) = 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
linarith
-- 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
δ : ℝ
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δ₃ : δ' < δ
⊢ Monotone (β := ℝ) fun (i : ℕ) ↦ a + (↑i : ℝ) * δ'

Tactic:
have h_mono : Monotone fun (i : ℕ) ↦ a + ↑i * δ' := by
    apply Monotone.const_add
    apply Monotone.mul_const Nat.mono_cast
    simp only [δ']
    refine div_nonneg ?_ ?_ <;> linarith
-- 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
δ : ℝ
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 : ℝ) * δ'
⊢ eVariationOn f (Icc (a + (↑0 : ℝ) * δ') (a + (↑(n + 1) : ℝ) * δ')) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + (↑(i + 1) : ℝ) * δ'))

Tactic:
eVariationOn.sum' f (I := fun i ↦ a + i * δ') h_mono |>.symm

Premises used: eVariationOn.sum', Eq.symm
-- 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
δ : ℝ
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 : ℝ) * δ'
h : a = a + (↑0 : ℝ) * δ'
h₁ : b = a + (↑(n + 1) : ℝ) * δ'
h₂ : ∀ x ∈ Finset.range (n + 1), HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 = (↑(x + 1) : ℝ)
⊢ eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))

Tactic:
convert! eVariationOn.sum' f (I := fun i ↦ a + i * δ') h_mono |>.symm

Premises used: eVariationOn.sum', Eq.symm
-- 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
δ : ℝ
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 : ℝ) * δ'
⊢ a = a + (↑0 : ℝ) * δ'

Tactic:
simp
-- 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
δ : ℝ
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 : ℝ) * δ'
h : b = a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ((b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ b = a + (↑(n + 1) : ℝ) * δ'

Tactic:
simp only [Nat.cast_add, Nat.cast_one, δ']

Premises used: Nat.cast_add, Nat.cast_one
-- 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
δ : ℝ
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 : ℝ) * δ'
⊢ b = a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ((b - a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
field
-- 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
δ : ℝ
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 : ℝ) * δ'
x : ℕ
h_1 : x ∈ Finset.range (n + 1)
h h₁ h₂ h₃ : x + 1 = x + 1
⊢ HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 = (↑(x + 1) : ℝ)

Tactic:
norm_cast
-- 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
δ : ℝ
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 : ℝ) * δ'
⊢ eVariationOn f (Icc a b) =
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + (↑i : ℝ) * δ') (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * δ'))

Tactic:
have v_sum : eVariationOn f (Icc a b) =
      ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + i * δ') (a + (i + 1) * δ')) := by
    convert! eVariationOn.sum' f (I := fun i ↦ a + i * δ') h_mono |>.symm
    · simp
    · simp only [Nat.cast_add, Nat.cast_one, δ']; field
    · norm_cast
-- 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
δ : ℝ
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
simp :
  ∀ (i : ℕ × { u : ℕ → ℝ // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }),
    LE.le (α := ENNReal) (∑ i_1 ∈ Finset.range i.1, edist (f ((↑i.2 : ℕ → ℝ) (i_1 + 1))) (f ((↑i.2 : ℕ → ℝ) i_1))) 1
⊢ eVariationOn f (Icc x y) ≤ 1

Tactic:
simp only [eVariationOn, iSup_le_iff]

Premises used: eVariationOn, iSup_le_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
δ : ℝ
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 }
⊢ Monotone (↑p.2 : ℕ → ℝ)

Tactic:
obtain ⟨hp₁, hp₂⟩ := p.2.property

Premises used: Prod.snd, Subtype.property