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)
⊢ ∀ (s : Finset (↑u : Type)) (g : ℝ → ℝ → ℝ),
    Eq (α := ℝ) (∑ b ∈ s, g (↑b : ℝ × ℝ).1 (↑b : ℝ × ℝ).2) (∑ z ∈ u_coe s, g z.1 z.2)

Tactic:
have u_coe_sum (s : Finset u) (g : ℝ → ℝ → ℝ) :
      ∑ b ∈ s, (g b.val.1 b.val.2) = ∑ z ∈ u_coe s, (g z.1 z.2) :=
    Finset.sum_nbij Subtype.val (by simp [u_coe]) (by simp)
      (by simp only [Finset.coe_image, u_coe]; tauto) (by 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 (ℝ × ℝ)
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)
⊢ LE.le (α := Filter (Finset (↑u : Type))) atTop (𝓟 univ)

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 (ℝ × ℝ)
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)
refine : Tendsto T atTop totalLengthFilter
⊢ Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))

Tactic:
refine tendsto_inf.mpr ⟨?_, hT.tendsto.mono_left (by simp)⟩

Premises used: Iff.mpr, Set.MapsTo.tendsto, Filter.tendsto_inf, And.intro, Filter.Tendsto.mono_left
-- 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)
simp : Tendsto (β := ℝ) ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ∘ T) atTop (𝓝 0)
⊢ Tendsto T atTop totalLengthFilter

Tactic:
simp only [totalLengthFilter, tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, AbsolutelyContinuousOnInterval.totalLengthFilter
-- 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 (fun (x : Finset (↑u : Type)) ↦ b - d - ∑ b ∈ x, (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) b)
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 (b - d - (b - d)))

Tactic:
hu₃.const_sub (b - d)

Premises used: HSub.hSub, Filter.Tendsto.const_sub
-- 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)
h :
  ∀ (s : Finset (↑u : Type)),
    ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ∘ T) s =
      b - d - ∑ b ∈ s, (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) b
h₁ : 0 = b - d - (b - d)
⊢ Tendsto (β := ℝ) ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ∘ T) atTop (𝓝 0)

Tactic:
convert! hu₃.const_sub (b - d) with s

Premises used: HSub.hSub, Filter.Tendsto.const_sub
-- 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 : ∑ i ∈ Finset.range (T s).1, dist ((T s).2 i).1 ((T s).2 i).2 = b - d - ∑ x ∈ s, ((↑x : ℝ × ℝ).2 - (↑x : ℝ × ℝ).1)
⊢ ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ∘ T) s =
    b - d - ∑ b ∈ s, (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) b

Tactic:
simp only [comp_apply]

Premises used: 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 (ℝ × ℝ)
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)
i : ℕ
hi : i ∈ Finset.range (T s).1
⊢ 0 ≤ ((T s).2 i).2 - ((T s).2 i).1

Tactic:
grind
-- 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)
i : ℕ
hi : i ∈ Finset.range (T s).1
rw : dist ((T s).2 i).2 ((T s).2 i).1 = (fun (i : ℕ) ↦ ((T s).2 i).2 - ((T s).2 i).1) i
rw₁ : |((T s).2 i).2 - ((T s).2 i).1| = (fun (i : ℕ) ↦ ((T s).2 i).2 - ((T s).2 i).1) i
rw₂ rw₃ : ((T s).2 i).2 - ((T s).2 i).1 = (fun (i : ℕ) ↦ ((T s).2 i).2 - ((T s).2 i).1) i
⊢ dist ((T s).2 i).1 ((T s).2 i).2 = (fun (i : ℕ) ↦ ((T s).2 i).2 - ((T s).2 i).1) i

Tactic:
rw [dist_comm, Real.dist_eq, abs_of_nonneg (by grind)]

Premises used: dist_comm, Real.dist_eq, abs_of_nonneg
-- 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 : ∑ i ∈ Finset.range (T s).1, (((T s).2 i).2 - ((T s).2 i).1) = b - d - ∑ x ∈ s, ((↑x : ℝ × ℝ).2 - (↑x : ℝ × ℝ).1)
⊢ ∑ i ∈ Finset.range (T s).1, dist ((T s).2 i).1 ((T s).2 i).2 = b - d - ∑ x ∈ s, ((↑x : ℝ × ℝ).2 - (↑x : ℝ × ℝ).1)

Tactic:
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)])]

Premises used: Finset.sum_congr, 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)
⊢ ∑ i ∈ Finset.range ((u_coe s).card + 1),
      (id ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).2 -
        id ((u_coe s).intervalGapsWithin ⋯ d b (↑i : Fin ((u_coe s).card + 1))).1) =
    id b - id d - ∑ z ∈ u_coe s, (id z.2 - id z.1)

Tactic:
(u_coe s).sum_intervalGapsWithin_eq_sub_sub_sum rfl id

Premises used: id, Finset.sum_intervalGapsWithin_eq_sub_sub_sum, rfl