awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
i : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := (fun (a : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal) i) ((fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦ (0 : ENNReal)) i)
    ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
        ((volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2) : ENNReal))
      i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
E : ℕ × (ℕ → ℝ × ℝ)
hfh :
  ∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2) ≤
    ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
⊢ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2) ≤
    ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)

Tactic:
grw [measure_biUnion_finset_le]

Premises used: MeasureTheory.measure_biUnion_finset_le
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
E : ℕ × (ℕ → ℝ × ℝ)
hfh :
  LE.le (α := ENNReal) (∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2))
    (∑ i ∈ Finset.range E.1, ENNReal.ofReal (dist (E.2 i).1 (E.2 i).2))
⊢ ∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2) ≤
    ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)

Tactic:
rw [ENNReal.ofReal_sum_of_nonneg (fun _ _ ↦ dist_nonneg)]

Premises used: ENNReal.ofReal_sum_of_nonneg, dist_nonneg
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
E : ℕ × (ℕ → ℝ × ℝ)
hfh :
  Eq (α := ENNReal) (∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2))
    (∑ i ∈ Finset.range E.1, ENNReal.ofReal (dist (E.2 i).1 (E.2 i).2))
⊢ LE.le (α := ENNReal) (∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2))
    (∑ i ∈ Finset.range E.1, ENNReal.ofReal (dist (E.2 i).1 (E.2 i).2))

Tactic:
apply Eq.le

Premises used: Eq.le
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
E : ℕ × (ℕ → ℝ × ℝ)
hfh :
  ∀ x ∈ Finset.range E.1,
    (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 x).1 (E.2 x).2) = ENNReal.ofReal (dist (E.2 x).1 (E.2 x).2)
⊢ Eq (α := ENNReal) (∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2))
    (∑ i ∈ Finset.range E.1, ENNReal.ofReal (dist (E.2 i).1 (E.2 i).2))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
E : ℕ × (ℕ → ℝ × ℝ)
⊢ ∀ x ∈ Finset.range E.1,
    (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 x).1 (E.2 x).2) = ENNReal.ofReal (dist (E.2 x).1 (E.2 x).2)

Tactic:
simp [uIoc, Real.dist_eq, max_sub_min_eq_abs']

Premises used: max_sub_min_eq_abs', Set.uIoc, Real.dist_eq
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
hh :
  Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hgf :
  LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal) (fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦ 0) fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
    (Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
hfh :
  LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
      (Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
      (Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (h := fun E : ℕ × (ℕ → ℝ × ℝ) ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
hh : totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤ totalLengthFilter
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
apply tendsto_volume_totalLengthFilter_nhds_zero.mono_left

Premises used: AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero, Filter.Tendsto.mono_left
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
⊢ totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤ totalLengthFilter

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
i : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := (fun (a : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal) i) ((fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦ (0 : ENNReal)) i)
    ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
        ((Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal)
            (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2) :
          ENNReal))
      i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
E : ℕ × (ℕ → ℝ × ℝ)
hfh :
  LE.le (α := ENNReal)
    ((Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal)
        (⋃ (i : ℕ), ⋃ (_ : i < E.1), uIoc (E.2 i).1 (E.2 i).2) :
      ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) (⋃ (i : ℕ), ⋃ (_ : i < E.1), uIoc (E.2 i).1 (E.2 i).2) : ENNReal)
⊢ LE.le (α := (fun (a : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal) E)
    ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
        ((Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal)
            (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2) :
          ENNReal))
      E)
    ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
        ((volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2) : ENNReal))
      E)

Tactic:
simp only [Finset.mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
E : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := ENNReal)
    ((Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal)
        (⋃ (i : ℕ), ⋃ (_ : i < E.1), uIoc (E.2 i).1 (E.2 i).2) :
      ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) (⋃ (i : ℕ), ⋃ (_ : i < E.1), uIoc (E.2 i).1 (E.2 i).2) : ENNReal)

Tactic:
apply Measure.restrict_le_self

Premises used: MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
a b : ℝ
⊢ AbsolutelyContinuousOnInterval f 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:
simp [AbsolutelyContinuousOnInterval, Metric.tendsto_nhds,
    Filter.HasBasis.eventually_iff (hasBasis_totalLengthFilter.inf_principal _),
    imp.swap, abs_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ dist_nonneg))]

Premises used: Metric.tendsto_nhds, dist_nonneg, Finset.sum_nonneg, AbsolutelyContinuousOnInterval, Filter.HasBasis.eventually_iff, abs_of_nonneg, Filter.HasBasis.inf_principal, imp.swap, AbsolutelyContinuousOnInterval.hasBasis_totalLengthFilter
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval f b a

Tactic:
simp_all [AbsolutelyContinuousOnInterval, disjWithin_comm]

Premises used: AbsolutelyContinuousOnInterval.disjWithin_comm, AbsolutelyContinuousOnInterval
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
a b c d : ℝ
hf :
  LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)))
    (𝓝 0)
habcd : uIcc c d ⊆ uIcc a b
⊢ LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin c d)))
    (𝓝 0)

Tactic:
le_trans (Filter.map_mono ?_) hf

Premises used: Filter.map_mono, le_trans
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
a b c d : ℝ
hf :
  LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)))
    (𝓝 0)
habcd : uIcc c d ⊆ uIcc a b
refine : totalLengthFilter ⊓ 𝓟 (disjWithin c d) ≤ totalLengthFilter ⊓ 𝓟 (disjWithin a b)
⊢ LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin c d)))
    (𝓝 0)

Tactic:
refine le_trans (Filter.map_mono ?_) hf

Premises used: Filter.map_mono, le_trans
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
a b c d : ℝ
hf :
  LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)))
    (𝓝 0)
habcd : uIcc c d ⊆ uIcc a b
h₂ : disjWithin c d ⊆ disjWithin a b
⊢ totalLengthFilter ⊓ 𝓟 (disjWithin c d) ≤ totalLengthFilter ⊓ 𝓟 (disjWithin a b)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
a b c d : ℝ
hf :
  LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)))
    (𝓝 0)
habcd : uIcc c d ⊆ uIcc a b
⊢ disjWithin c d ⊆ disjWithin a b

Tactic:
disjWithin_mono habcd

Premises used: AbsolutelyContinuousOnInterval.disjWithin_mono
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
a b c d : ℝ
hf :
  LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)))
    (𝓝 0)
habcd : uIcc c d ⊆ uIcc a b
⊢ disjWithin c d ⊆ disjWithin a b

Tactic:
exact disjWithin_mono habcd

Premises used: AbsolutelyContinuousOnInterval.disjWithin_mono
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ Tendsto (β := ℝ)
    (fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range x.1, dist (f (x.2 i).1) (f (x.2 i).2))
        (∑ i ∈ Finset.range x.1, dist (g (x.2 i).1) (g (x.2 i).2)))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
simpa using Tendsto.add hf hg

Premises used: Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
apply : ∀ (t : ℕ × (ℕ → ℝ × ℝ)), LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2))
apply₁ :
  ∀ (t : ℕ × (ℕ → ℝ × ℝ)),
    ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2))
        (∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2))
⊢ AbsolutelyContinuousOnInterval (f + g) a b

Tactic:
apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using Tendsto.add hf hg)

Premises used: squeeze_zero
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
i : ℕ
hi : i ∈ Finset.range t.1
⊢ 0 ≤ dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2))

Tactic:
exact Finset.sum_nonneg (fun i hi ↦ by positivity)

Premises used: Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
rw :
  LE.le (α := ℝ) (∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2))
    (∑ x ∈ Finset.range t.1, (dist (f (t.2 x).1) (f (t.2 x).2) + dist (g (t.2 x).1) (g (t.2 x).2)))
⊢ ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤
    HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2))
      (∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2))

Tactic:
rw [← Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
h :
  ∀ i ∈ Finset.range t.1,
    dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤ dist (f (t.2 i).1) (f (t.2 i).2) + dist (g (t.2 i).1) (g (t.2 i).2)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2))
    (∑ x ∈ Finset.range t.1, (dist (f (t.2 x).1) (f (t.2 x).2) + dist (g (t.2 x).1) (g (t.2 x).2)))

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
i : ℕ
h : i ∈ Finset.range t.1
⊢ dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤ dist (f (t.2 i).1) (f (t.2 i).2) + dist (g (t.2 i).1) (g (t.2 i).2)

Tactic:
dist_add_add_le _ _ _ _

Premises used: dist_add_add_le
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
i : ℕ
h : i ∈ Finset.range t.1
⊢ dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤ dist (f (t.2 i).1) (f (t.2 i).2) + dist (g (t.2 i).1) (g (t.2 i).2)

Tactic:
exact dist_add_add_le _ _ _ _

Premises used: dist_add_add_le
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
simpa using hf
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
apply : ∀ (t : ℕ × (ℕ → ℝ × ℝ)), LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2))
apply₁ :
  ∀ (t : ℕ × (ℕ → ℝ × ℝ)),
    LE.le (α := ℝ) (∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2))
      (∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2))
⊢ AbsolutelyContinuousOnInterval (-f) a b

Tactic:
apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf)

Premises used: squeeze_zero
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
i : ℕ
hi : i ∈ Finset.range t.1
⊢ 0 ≤ dist ((-f) (t.2 i).1) ((-f) (t.2 i).2)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2))

Tactic:
exact Finset.sum_nonneg (fun i hi ↦ by positivity)

Premises used: Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2))
    (∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ AbsolutelyContinuousOnInterval (f - g) a b

Tactic:
simpa [sub_eq_add_neg] using hf.add (hg.neg)

Premises used: AbsolutelyContinuousOnInterval.add, sub_eq_add_neg, AbsolutelyContinuousOnInterval.neg
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
⊢ Tendsto (β := ℝ) (fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦ ‖α‖ * ∑ i ∈ Finset.range x.1, dist (f (x.2 i).1) (f (x.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
simpa using hf.const_mul ‖α‖

Premises used: Norm.norm, Filter.Tendsto.const_mul
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
apply :
  ∀ (t : ℕ × (ℕ → ℝ × ℝ)),
    LE.le (α := ℝ) 0
      (∑ i ∈ Finset.range t.1,
        dist.{u_2} (α := F) ((fun (x : ℝ) ↦ α • f x) (t.2 i).1) ((fun (x : ℝ) ↦ α • f x) (t.2 i).2))
apply₁ :
  ∀ (t : ℕ × (ℕ → ℝ × ℝ)),
    ∑ i ∈ Finset.range t.1,
        dist.{u_2} (α := F) ((fun (x : ℝ) ↦ α • f x) (t.2 i).1) ((fun (x : ℝ) ↦ α • f x) (t.2 i).2) ≤
      ‖α‖ * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)
⊢ AbsolutelyContinuousOnInterval.{u_2} (X := F) (fun (x : ℝ) ↦ α • f x) a b

Tactic:
apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf.const_mul ‖α‖)

Premises used: squeeze_zero
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
i : ℕ
hi : i ∈ Finset.range t.1
⊢ 0 ≤ dist.{u_2} (α := F) ((fun (x : ℝ) ↦ α • f x) (t.2 i).1) ((fun (x : ℝ) ↦ α • f x) (t.2 i).2)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := ℝ) 0
    (∑ i ∈ Finset.range t.1,
      dist.{u_2} (α := F) ((fun (x : ℝ) ↦ α • f x) (t.2 i).1) ((fun (x : ℝ) ↦ α • f x) (t.2 i).2))

Tactic:
exact Finset.sum_nonneg (fun i hi ↦ by positivity)

Premises used: Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist.{u_2} (α := F) ((fun (x : ℝ) ↦ α • f x) (t.2 i).1) ((fun (x : ℝ) ↦ α • f x) (t.2 i).2) ≤
    ‖α‖ * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)

Tactic:
simp [Finset.mul_sum, dist_smul₀]

Premises used: Finset.mul_sum, dist_smul₀
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
f : ℝ → ℝ
α : ℝ
hf : AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (x : ℝ) ↦ α * f x) a b

Tactic:
hf.const_smul α

Premises used: AbsolutelyContinuousOnInterval.const_smul
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
⊢ uniformity X = comap (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter

Tactic:
Filter.HasBasis.eq_of_same_basis Metric.uniformity_basis_dist ?_

Premises used: Metric.uniformity_basis_dist, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
refine :
  HasBasis.{u_1, 1} (α := X × X)
    (comap (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter) (fun (ε : ℝ) ↦ 0 < ε)
    fun (ε : ℝ) ↦ {p : X × X | dist p.1 p.2 < ε}
⊢ uniformity X = comap (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter

Tactic:
refine Filter.HasBasis.eq_of_same_basis Metric.uniformity_basis_dist ?_

Premises used: Metric.uniformity_basis_dist, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
⊢ HasBasis.{u_1, 1} (α := X × X)
    (comap (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter) (fun (ε : ℝ) ↦ 0 < ε)
    fun (i : ℝ) ↦
    preimage (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x))
      {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < i}

Tactic:
hasBasis_totalLengthFilter.comap _

Premises used: Filter.HasBasis.comap, AbsolutelyContinuousOnInterval.hasBasis_totalLengthFilter
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
h :
  ∀ (x : ℝ),
    Eq.{u_1 + 1} (α := Set (X × X)) {p : X × X | dist p.1 p.2 < x}
      (preimage (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x))
        {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < x})
⊢ HasBasis.{u_1, 1} (α := X × X)
    (comap (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter) (fun (ε : ℝ) ↦ 0 < ε)
    fun (ε : ℝ) ↦ {p : X × X | dist p.1 p.2 < ε}

Tactic:
convert! hasBasis_totalLengthFilter.comap _

Premises used: Filter.HasBasis.comap, AbsolutelyContinuousOnInterval.hasBasis_totalLengthFilter
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
x : ℝ
⊢ Eq.{u_1 + 1} (α := Set (X × X)) {p : X × X | dist p.1 p.2 < x}
    (preimage (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x))
      {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < x})

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
simp :
  comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) ≤
    comap.{0, u_2} (β := F × F) (fun (x : ℝ × ℝ) ↦ (f x.1, f x.2))
      (comap (β := ℕ × (ℕ → F × F)) (fun (x : F × F) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter)
⊢ UniformContinuousOn f (uIcc a b)

Tactic:
simp only [UniformContinuousOn, Filter.tendsto_iff_comap, uniformity_eq_comap_totalLengthFilter]

Premises used: Filter.tendsto_iff_comap, UniformContinuousOn, AbsolutelyContinuousOnInterval.uniformity_eq_comap_totalLengthFilter
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
    comap (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)

Tactic:
simp only [AbsolutelyContinuousOnInterval, Filter.tendsto_iff_comap] at hf

Premises used: Filter.tendsto_iff_comap, AbsolutelyContinuousOnInterval