Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case e'_3
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 ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
s : Finset ↑u
⊢ ((fun E ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ∘ T) s = b - d - ∑ b ∈ s, (fun z ↦ (↑z).2 - (↑z).1) b

pp: case e'_5
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 ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
⊢ 0 = b - d - (b - d)

Tactic:
· 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

Goal state after:
case e'_5
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 ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
⊢ 0 = b - d - (b - d)