-- 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
hT₅ :
  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
hT₆ :
  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 : ℕ),
    ((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₇ :
  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 : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2 ≤ b
hT₈ :
  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)),
    (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₉ :
  let u_coe : (s : Finset (↑u : Type)) → Finset (ℝ × ℝ) := fun (s : Finset (↑u : Type)) ↦
    Finset.image (Subtype.val (p := fun (x : ℝ × ℝ) ↦ x ∈ u)) s;
  let 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)));
  MapsTo T univ (disjWithin d 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)) (g : ℝ → ℝ → ℝ),
    Eq (α := ℝ) (∑ b ∈ s, g (↑b : ℝ × ℝ).1 (↑b : ℝ × ℝ).2) (∑ z ∈ u_coe s, g z.1 z.2)

Tactic:
rw [HasSum] at hu₄

Premises used: HasSum, SummationFilter.unconditional