Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
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
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ : Tendsto (fun s ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2)) (SummationFilter.unconditional ↑u).filter (𝓝 y)
sum_tendsto :
  Tendsto
    (fun x ↦ ∑ 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 (f d) (f b) ≤ y

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]

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
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
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ : Tendsto (fun s ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2)) (SummationFilter.unconditional ↑u).filter (𝓝 y)
sum_tendsto :
  Tendsto
    (fun x ↦ ∑ 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),
    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)
⊢ dist (f d) (f b) ≤ y