awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
hu₁ : ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
T : (s : Finset (↑u : Type)) → ℕ × ((i : ℕ) → ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦
    ((u_coe s).card + 1, fun (i : ℕ) ↦ (u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1)))
hT₁ : ∀ (s : Finset (↑u : Type)) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1
hT₂ :
  ∀ (s : Finset (↑u : Type)) (i : ℕ),
    ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1 ≤
      ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2
hT₃ : ∀ (s : Finset (↑u : Type)) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2 ≤ b
hT₄ :
  ∀ (s : Finset (↑u : Type)),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint (α := Set ℝ) fun (j : ℕ) ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).1
        ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum :
  ∀ (s : Finset (↑u : Type)) (g : ℝ → ℝ → ℝ),
    Eq (α := ℝ) (∑ b ∈ s, g (↑b : ℝ × ℝ).1 (↑b : ℝ × ℝ).2) (∑ z ∈ u_coe s, g z.1 z.2)
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ :
  Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
⊢ Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ)
        (((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) ∘ T) x)
        (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
    atTop (𝓝 (0 + y))

Tactic:
have sum_tendsto := hf.comp hu₃ |>.add hu₄
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
hu₁ : ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
T : (s : Finset (↑u : Type)) → ℕ × ((i : ℕ) → ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦
    ((u_coe s).card + 1, fun (i : ℕ) ↦ (u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1)))
hT₁ : ∀ (s : Finset (↑u : Type)) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1
hT₂ :
  ∀ (s : Finset (↑u : Type)) (i : ℕ),
    ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1 ≤
      ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2
hT₃ : ∀ (s : Finset (↑u : Type)) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2 ≤ b
hT₄ :
  ∀ (s : Finset (↑u : Type)),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint (α := Set ℝ) fun (j : ℕ) ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).1
        ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum :
  ∀ (s : Finset (↑u : Type)) (g : ℝ → ℝ → ℝ),
    Eq (α := ℝ) (∑ b ∈ s, g (↑b : ℝ × ℝ).1 (↑b : ℝ × ℝ).2) (∑ z ∈ u_coe s, g z.1 z.2)
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ :
  Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
sum_tendsto :
  Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ)
        (((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) ∘ T) x)
        (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
    atTop (𝓝 (0 + y))
⊢ Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2))
        (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
    atTop (𝓝 y)

Tactic:
simp only [comp_apply, zero_add] at sum_tendsto

Premises used: zero_add, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
hu₁ : ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
T : (s : Finset (↑u : Type)) → ℕ × ((i : ℕ) → ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦
    ((u_coe s).card + 1, fun (i : ℕ) ↦ (u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1)))
hT₁ : ∀ (s : Finset (↑u : Type)) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1
hT₂ :
  ∀ (s : Finset (↑u : Type)) (i : ℕ),
    ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1 ≤
      ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2
hT₃ : ∀ (s : Finset (↑u : Type)) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2 ≤ b
hT₄ :
  ∀ (s : Finset (↑u : Type)),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint (α := Set ℝ) fun (j : ℕ) ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).1
        ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum :
  ∀ (s : Finset (↑u : Type)) (g : ℝ → ℝ → ℝ),
    Eq (α := ℝ) (∑ b ∈ s, g (↑b : ℝ × ℝ).1 (↑b : ℝ × ℝ).2) (∑ z ∈ u_coe s, g z.1 z.2)
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ :
  Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
sum_tendsto :
  Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2))
        (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
    atTop (𝓝 y)
s : Finset (↑u : Type)
rw :
  dist (f d) (f b) ≤
    ∑ x ∈ Finset.range (u_coe s).card,
        (dist (f ((T s).2 x).1) (f ((T s).2 x).2) +
          dist (f ((u_coe s).intervalGapsWithin ⋯ d b (↑x : Fin ((u_coe s).card + 1))).2)
            (f ((u_coe s).intervalGapsWithin ⋯ d b (↑x.succ : Fin ((u_coe s).card + 1))).1)) +
      dist (f ((T s).2 (u_coe s).card).1) (f ((T s).2 (u_coe s).card).2)
rw₁ rw₂ : ℝ
⊢ dist (f d) (f b) ≤
    HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T s).1, dist (f ((T s).2 i).1) (f ((T s).2 i).2))
      (∑ b ∈ u_coe s, dist (f b.1) (f b.2))

Tactic:
rw [Finset.sum_eq_sum_range_intervalGapsWithin _ rfl (fun x y ↦ dist (f x) (f y)),
        Finset.sum_range_succ, add_right_comm, ← Finset.sum_add_distrib]

Premises used: Finset.sum_eq_sum_range_intervalGapsWithin, Finset.sum_add_distrib, add_right_comm, Dist.dist, Finset.sum_range_succ, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
hu₁ : ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
T : (s : Finset (↑u : Type)) → ℕ × ((i : ℕ) → ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦
    ((u_coe s).card + 1, fun (i : ℕ) ↦ (u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1)))
hT₁ : ∀ (s : Finset (↑u : Type)) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1
hT₂ :
  ∀ (s : Finset (↑u : Type)) (i : ℕ),
    ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1 ≤
      ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2
hT₃ : ∀ (s : Finset (↑u : Type)) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2 ≤ b
hT₄ :
  ∀ (s : Finset (↑u : Type)),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint (α := Set ℝ) fun (j : ℕ) ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).1
        ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum :
  ∀ (s : Finset (↑u : Type)) (g : ℝ → ℝ → ℝ),
    Eq (α := ℝ) (∑ b ∈ s, g (↑b : ℝ × ℝ).1 (↑b : ℝ × ℝ).2) (∑ z ∈ u_coe s, g z.1 z.2)
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ :
  Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
sum_tendsto :
  Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2))
        (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
    atTop (𝓝 y)
s : Finset (↑u : Type)
⊢ dist (f d) (f b) ≤ dist (f ((T s).2 0).1) (f ((T s).2 (u_coe s).card).2)

Tactic:
simp [T]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
hu₁ : ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
T : (s : Finset (↑u : Type)) → ℕ × ((i : ℕ) → ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦
    ((u_coe s).card + 1, fun (i : ℕ) ↦ (u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1)))
hT₁ : ∀ (s : Finset (↑u : Type)) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1
hT₂ :
  ∀ (s : Finset (↑u : Type)) (i : ℕ),
    ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1 ≤
      ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2
hT₃ : ∀ (s : Finset (↑u : Type)) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2 ≤ b
hT₄ :
  ∀ (s : Finset (↑u : Type)),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint (α := Set ℝ) fun (j : ℕ) ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).1
        ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum :
  ∀ (s : Finset (↑u : Type)) (g : ℝ → ℝ → ℝ),
    Eq (α := ℝ) (∑ b ∈ s, g (↑b : ℝ × ℝ).1 (↑b : ℝ × ℝ).2) (∑ z ∈ u_coe s, g z.1 z.2)
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ :
  Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
sum_tendsto :
  Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2))
        (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
    atTop (𝓝 y)
⊢ ∀ (s : Finset (↑u : Type)),
    dist (f d) (f b) ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T s).1, dist (f ((T s).2 i).1) (f ((T s).2 i).2))
        (∑ b ∈ u_coe s, dist (f b.1) (f b.2))

Tactic:
have dist_le_sum (s : Finset u) :
      dist (f d) (f b) ≤
      ∑ i ∈ Finset.range (T s).1, dist (f ((T s).2 i).1) (f ((T s).2 i).2) +
      (∑ b ∈ u_coe s, dist (f b.1) (f b.2)) := by
    rw [Finset.sum_eq_sum_range_intervalGapsWithin _ rfl (fun x y ↦ dist (f x) (f y)),
        Finset.sum_range_succ, add_right_comm, ← Finset.sum_add_distrib]
    grw [← Finset.sum_le_sum (fun _ _ ↦ dist_triangle _ _ _),
        ← dist_le_range_sum_dist,
        ← dist_triangle]
    simp [T]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
hu₁ : ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
T : (s : Finset (↑u : Type)) → ℕ × ((i : ℕ) → ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦
    ((u_coe s).card + 1, fun (i : ℕ) ↦ (u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1)))
hT₁ : ∀ (s : Finset (↑u : Type)) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1
hT₂ :
  ∀ (s : Finset (↑u : Type)) (i : ℕ),
    ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1 ≤
      ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2
hT₃ : ∀ (s : Finset (↑u : Type)) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2 ≤ b
hT₄ :
  ∀ (s : Finset (↑u : Type)),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint (α := Set ℝ) fun (j : ℕ) ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).1
        ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum :
  ∀ (s : Finset (↑u : Type)) (g : ℝ → ℝ → ℝ),
    Eq (α := ℝ) (∑ b ∈ s, g (↑b : ℝ × ℝ).1 (↑b : ℝ × ℝ).2) (∑ z ∈ u_coe s, g z.1 z.2)
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ :
  Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
sum_tendsto :
  Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2))
        (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
    atTop (𝓝 y)
dist_le_sum :
  ∀ (s : Finset (↑u : Type)),
    dist (f d) (f b) ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T s).1, dist (f ((T s).2 i).1) (f ((T s).2 i).2))
        (∑ b ∈ u_coe s, dist (f b.1) (f b.2))
⊢ Tendsto (fun (x : Finset (↑u : Type)) ↦ dist (f d) (f b)) atTop (𝓝 (dist (f d) (f b)))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦ Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s
hu₁ : ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
T : (s : Finset (↑u : Type)) → ℕ × ((i : ℕ) → ℝ × ℝ) :=
  fun (s : Finset (↑u : Type)) ↦
    ((u_coe s).card + 1, fun (i : ℕ) ↦ (u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1)))
hT₁ : ∀ (s : Finset (↑u : Type)) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1
hT₂ :
  ∀ (s : Finset (↑u : Type)) (i : ℕ),
    ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1 ≤
      ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2
hT₃ : ∀ (s : Finset (↑u : Type)) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2 ≤ b
hT₄ :
  ∀ (s : Finset (↑u : Type)),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint (α := Set ℝ) fun (j : ℕ) ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).1
        ((u_coe s).intervalGapsWithin ⋯ d b (↑j : Fin ((u_coe s).card + 1))).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum :
  ∀ (s : Finset (↑u : Type)) (g : ℝ → ℝ → ℝ),
    Eq (α := ℝ) (∑ b ∈ s, g (↑b : ℝ × ℝ).1 (↑b : ℝ × ℝ).2) (∑ z ∈ u_coe s, g z.1 z.2)
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ :
  Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
sum_tendsto :
  Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2))
        (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
    atTop (𝓝 y)
dist_le_sum :
  ∀ (s : Finset (↑u : Type)),
    dist (f d) (f b) ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range (T s).1, dist (f ((T s).2 i).1) (f ((T s).2 i).2))
        (∑ b ∈ u_coe s, dist (f b.1) (f b.2))
⊢ dist (f d) (f b) ≤ y

Tactic:
exact le_of_tendsto_of_tendsto' (by simp) sum_tendsto dist_le_sum

Premises used: le_of_tendsto_of_tendsto'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
inr :
  ∀
    (this :
      ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ}
        (hf : AbsolutelyContinuousOnInterval f a b) (hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x) (hab : a ≤ b),
        ∃ (C : F), ∀ x ∈ uIcc a b, f x = C)
    (hab : ¬a ≤ b), ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
wlog :
  ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ}
    (hf : AbsolutelyContinuousOnInterval f a b) (hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x) (hab : a ≤ b),
    ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
⊢ ∃ (C : F), ∀ x ∈ uIcc a b, f x = C

Tactic:
wlog hab : a ≤ b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
this :
  ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ}
    (hf : AbsolutelyContinuousOnInterval f a b) (hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x) (hab : a ≤ b),
    ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
hab : ¬a ≤ b
linarith : a < b → b - a + (a - b) = 0
⊢ b ≤ a

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
this :
  ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ}
    (hf : AbsolutelyContinuousOnInterval f a b) (hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x) (hab : a ≤ b),
    ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
hab : ¬a ≤ b
⊢ ∃ (C : F), ∀ x ∈ uIcc a b, f x = C

Tactic:
exact uIcc_comm b a ▸ this (a := b) (b := a) hf.symm (uIcc_comm a b ▸ hf₀) (by linarith)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
hab : a ≤ b
this : ∀ x ∈ uIcc a b, f x = f b
w : F
h : ∀ x ∈ uIcc a b, f x = f b
⊢ ∃ (C : F), ∀ x ∈ uIcc a b, f x = C

Tactic:
use f b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
hab : a ≤ b
suffices : ∀ x ∈ uIcc a b, f x = f b
⊢ ∃ (C : F), ∀ x ∈ uIcc a b, f x = C

Tactic:
suffices ∀ x ∈ uIcc a b, f x = f b by use f b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
hab : a ≤ b
rw : ∀ (hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x) (hab : a ≤ b), ∀ x ∈ Icc a b, f x = f b
⊢ ∀ x ∈ uIcc a b, f x = f b

Tactic:
rw [uIcc_of_le hab] at hf₀ ⊢

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
this : ∀ r > 0, dist (f d) (f b) ≤ r
contrapose! : ∀ (this : f d ≠ f b), ∃ r > 0, r < dist (f d) (f b)
⊢ f d = f b

Tactic:
contrapose! this
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
this : f d ≠ f b
⊢ ∃ r > 0, r < dist (f d) (f b)

Tactic:
exists_between (dist_pos.mpr this)

Premises used: Iff.mpr, exists_between, dist_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
this : f d ≠ f b
⊢ ∃ r > 0, r < dist (f d) (f b)

Tactic:
exact exists_between (dist_pos.mpr this)

Premises used: Iff.mpr, exists_between, dist_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
suffices : ∀ r > 0, dist (f d) (f b) ≤ r
⊢ f d = f b

Tactic:
suffices ∀ r > 0, dist (f d) (f b) ≤ r by
    contrapose! this
    exact exists_between (dist_pos.mpr this)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
r : ℝ
hr : r > 0
rw : ∀ (hd : a ≤ d ∧ d ≤ b) (r : ℝ) (hr : r > 0), dist (f d) (f b) ≤ r
⊢ dist (f d) (f b) ≤ r

Tactic:
rw [mem_Icc] at hd

Premises used: Set.mem_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
linarith : d < a → a - d + (d - a) = 0
⊢ a ≤ d

Tactic:
linarith