awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
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 (T s).1, (((T s).2 i).2 - ((T s).2 i).1) = b - d - ∑ x ∈ s, ((↑x : ℝ × ℝ).2 - (↑x : ℝ × ℝ).1)
have h : Eq (α := ℝ) (∑ x ∈ s, ((↑x : ℝ × ℝ).2 - (↑x : ℝ × ℝ).1)) (∑ z ∈ u_coe s, (id z.2 - id z.1))
Tactic: convert! (u_coe s).sum_intervalGapsWithin_eq_sub_sub_sum rfl id
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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)
⊢ dist (f d) (f b) ≤ y
have hu₅ : 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
Cleared hypotheses: hu₃
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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))
⊢ dist (f d) (f b) ≤ y
have hu₅ : 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₄
Cleared hypotheses: hu₄, u_coe, hu₁, hu₂, T, hT₁, hT₂, hT₃, hT₄, hT, u_coe_sum, hu₃
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
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))
⊢ dist (f d) (f b) ≤ y
have hu₅ : 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₄
Cleared hypotheses: hu₄
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
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)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
⊢ dist (f d) (f b) ≤ y
have sum_tendsto : Tendsto
  (fun (x : Finset (↑u : Type)) ↦
    HAdd.hAdd (α := ℝ) (((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) ∘ T) x)
      (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
  atTop (𝓝 (0 + y))
Tactic: have sum_tendsto := hf.comp hu₃ |>.add hu₄
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
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)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
sum_tendsto :
  Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ)
        (((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) ∘ T) x)
        (∑ z ∈ u_coe x, dist (f z.1) (f z.2)))
    atTop (𝓝 (0 + y))
⊢ dist (f d) (f b) ≤ y
have sum_tendsto₁ : Tendsto
  (fun (x : Finset (↑u : Type)) ↦
    HAdd.hAdd (α := ℝ) (∑ 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)
Tactic: simp only [comp_apply, zero_add] at sum_tendsto
Cleared hypotheses: sum_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
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)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
sum_tendsto :
  Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ) (∑ 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)
s : Finset (↑u : Type)
⊢ dist (f d) (f b) ≤
    HAdd.hAdd (α := ℝ) (∑ 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))
have rw : dist (f d) (f b) ≤
  ∑ x ∈ Finset.range (u_coe s).card,
      (dist (f ((T s).2 x).1) (f ((T s).2 x).2) +
        dist (f ((u_coe s).intervalGapsWithin sorry d b (↑x : Fin ((u_coe s).card + 1))).2)
          (f ((u_coe s).intervalGapsWithin sorry d b (↑x.succ : Fin ((u_coe s).card + 1))).1)) +
    dist (f ((T s).2 (u_coe s).card).1) (f ((T s).2 (u_coe s).card).2)
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
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)) ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2))
    (SummationFilter.filter (SummationFilter.unconditional (↑u : Type))) (𝓝 y)
sum_tendsto :
  Tendsto
    (fun (x : Finset (↑u : Type)) ↦
      HAdd.hAdd (α := ℝ) (∑ 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
have dist_le_sum : ∀ (s : Finset (↑u : Type)),
  dist (f d) (f b) ≤
    HAdd.hAdd (α := ℝ) (∑ 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))
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
⊢ ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
have inr : ∀
  (this :
    ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ}
      (hf : AbsolutelyContinuousOnInterval f a b) (hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x) (hab : a ≤ b),
      ∃ (C : F), ∀ x ∈ uIcc a b, f x = C)
  (hab : ¬a ≤ b), ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
Tactic: wlog hab : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
inr :
  ∀
    (this :
      ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ}
        (hf : AbsolutelyContinuousOnInterval f a b) (hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x) (hab : a ≤ b),
        ∃ (C : F), ∀ x ∈ uIcc a b, f x = C)
    (hab : ¬a ≤ b), ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
⊢ ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
have wlog : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ}
  (hf : AbsolutelyContinuousOnInterval f a b) (hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x) (hab : a ≤ b),
  ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
Tactic: wlog hab : a ≤ b
Cleared hypotheses: f, a, b, hf, hf₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
this :
  ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ}
    (hf : AbsolutelyContinuousOnInterval f a b) (hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x) (hab : a ≤ b),
    ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
hab : ¬a ≤ b
⊢ b ≤ a
have linarith : a < b → b - a + (a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
hab : a ≤ b
this : ∀ x ∈ uIcc a b, f x = f b
⊢ ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
have w : F
Tactic: use f b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
hab : a ≤ b
⊢ ∃ (C : F), ∀ x ∈ uIcc a b, f x = C
have suffices : ∀ x ∈ uIcc a b, f x = f b
Tactic: suffices ∀ x ∈ uIcc a b, f x = f b by use f b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
hab : a ≤ b
⊢ ∀ x ∈ uIcc a b, f x = f b
have rw : ∀ (hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x) (hab : a ≤ b), ∀ x ∈ Icc a b, f x = f b
Tactic: rw [uIcc_of_le hab] at hf₀ ⊢
Cleared hypotheses: hf₀, hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
this : ∀ r > 0, dist (f d) (f b) ≤ r
⊢ f d = f b
have contrapose! : ∀ (this : f d ≠ f b), ∃ r > 0, r < dist (f d) (f b)
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
⊢ f d = f b
have suffices : ∀ r > 0, dist (f d) (f b) ≤ r
Tactic: suffices ∀ r > 0, dist (f d) (f b) ≤ r by
    contrapose! this
    exact exists_between (dist_pos.mpr this)