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 (ℝ × ℝ)
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
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)
s : Finset (↑u : Type)
h : Eq (α := ℝ) (∑ x ∈ s, ((↑x : ℝ × ℝ).2 - (↑x : ℝ × ℝ).1)) (∑ z ∈ u_coe s, (id z.2 - id z.1))
⊢ ∑ i ∈ Finset.range (T s).1, (((T s).2 i).2 - ((T s).2 i).1) = b - d - ∑ x ∈ s, ((↑x : ℝ × ℝ).2 - (↑x : ℝ × ℝ).1)

Tactic:
convert! (u_coe s).sum_intervalGapsWithin_eq_sub_sub_sum rfl id

Premises used: id, Finset.sum_intervalGapsWithin_eq_sub_sub_sum, 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 (ℝ × ℝ)
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
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)
s : Finset (↑u : Type)
⊢ Eq (α := ℝ) (∑ x ∈ s, ((↑x : ℝ × ℝ).2 - (↑x : ℝ × ℝ).1)) (∑ z ∈ u_coe s, (id z.2 - id z.1))

Tactic:
u_coe_sum s fun x y ↦ y - x

Premises used: HSub.hSub
-- 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 (ℝ × ℝ)
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
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)
s : Finset (↑u : Type)
⊢ Eq (α := ℝ) (∑ x ∈ s, ((↑x : ℝ × ℝ).2 - (↑x : ℝ × ℝ).1)) (∑ z ∈ u_coe s, (id z.2 - id z.1))

Tactic:
exact u_coe_sum s fun x y ↦ y - x

Premises used: HSub.hSub
-- 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 (ℝ × ℝ)
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
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)
⊢ 0 = b - d - (b - d)

Tactic:
abel
-- 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 (ℝ × ℝ)
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
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)
⊢ Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))

Tactic:
replace hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b)) := by
    refine tendsto_inf.mpr ⟨?_, hT.tendsto.mono_left (by simp)⟩
    simp only [totalLengthFilter, tendsto_comap_iff]
    convert! hu₃.const_sub (b - d) with s
    · simp only [comp_apply]
      rw [Finset.sum_congr rfl (g := fun i ↦ ((T s).2 i).2 - ((T s).2 i).1)
            (fun i hi ↦ by rw [dist_comm, Real.dist_eq, abs_of_nonneg (by grind)])]
      convert! (u_coe s).sum_intervalGapsWithin_eq_sub_sub_sum rfl id
      exact u_coe_sum s fun x y ↦ y - x
    · abel
-- 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 (ℝ × ℝ)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
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))
⊢ Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ b ∈ s, dist (f (↑b : ℝ × ℝ).1) (f (↑b : ℝ × ℝ).2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)

Tactic:
rw [HasSum] at hu₄

Premises used: HasSum, SummationFilter.unconditional
-- 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 (ℝ × ℝ)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
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)) ↦ ∑ b ∈ s, dist (f (↑b : ℝ × ℝ).1) (f (↑b : ℝ × ℝ).2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
⊢ let u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) := fun (s : Finset (↑u : Type)) ↦
    Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s;
  ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b

Tactic:
rw [HasSum] at hu₄

Premises used: HasSum, SummationFilter.unconditional
-- 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 (ℝ × ℝ)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
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)) ↦ ∑ b ∈ s, dist (f (↑b : ℝ × ℝ).1) (f (↑b : ℝ × ℝ).2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
hu₆ :
  let u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) := fun (s : Finset (↑u : Type)) ↦
    Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s;
  ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ let u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) := fun (s : Finset (↑u : Type)) ↦
    Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s;
  ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2

Tactic:
rw [HasSum] at hu₄

Premises used: HasSum, SummationFilter.unconditional
-- 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 (ℝ × ℝ)
hu₄ : HasSum (fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)) y
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)) ↦ ∑ b ∈ s, dist (f (↑b : ℝ × ℝ).1) (f (↑b : ℝ × ℝ).2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
hu₆ :
  let u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) := fun (s : Finset (↑u : Type)) ↦
    Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s;
  ∀ (s : Finset (↑u : Type)) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₇ :
  let u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) := fun (s : Finset (↑u : Type)) ↦
    Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s;
  ∀ (s : Finset (↑u : Type)), (↑(u_coe s) : Set (ℝ × ℝ)).PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
⊢ let u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) := fun (s : Finset (↑u : Type)) ↦
    Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s;
  ∀ (s : Finset (↑u : Type)) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1

Tactic:
rw [HasSum] at hu₄

Premises used: HasSum, SummationFilter.unconditional
-- 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 (ℝ × ℝ)
hu₄ :
  Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ b ∈ s, dist (f (↑b : ℝ × ℝ).1) (f (↑b : ℝ × ℝ).2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
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))
⊢ Tendsto (fun (s : Finset (↑u : Type)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)

Tactic:
simp_rw [u_coe_sum _ fun x y ↦ dist (f x) (f y)] at hu₄

Premises used: Dist.dist