awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) {a : α | ¬Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)} :
      ENNReal)
    (0 : ENNReal)
have h_ss : aeSeqSet hf p ⊆ {a : α | Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)}
Tactic: have h_ss : aeSeqSet hf p ⊆ { a : α | ⨆ i : ι, aeSeq hf p i a = ⨆ i : ι, f i a } := by
    intro x hx
    congr
    exact funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
⊢ HasBasis.{u_1, 1} (α := ℕ × (ℕ → X × X)) totalLengthFilter (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦
    {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε}
have h : Eq.{u_1 + 1} (α := ℝ → Set (ℕ × (ℕ → X × X)))
  (fun (ε : ℝ) ↦ {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε}) fun (i : ℝ) ↦
  (fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ⁻¹' Ioo (0 - i) (0 + i)
Tactic: convert! Filter.HasBasis.comap (α := ℝ) _ (nhds_basis_Ioo_pos _) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
⊢ Eq.{u_1 + 1} (α := ℝ → Set (ℕ × (ℕ → X × X)))
    (fun (ε : ℝ) ↦ {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε}) fun (i : ℝ) ↦
    (fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ⁻¹' Ioo (0 - i) (0 + i)
have h : ∀ (ε : ℝ) (E : ℕ × (ℕ → X × X)),
  Membership.mem (γ := Set (ℕ × (ℕ → X × X)))
      {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε} E ↔
    Membership.mem (γ := Set (ℕ × (ℕ → X × X)))
      ((fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ⁻¹' Ioo (0 - ε) (0 + ε)) E
Tactic: ext ε E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ
E : ℕ × (ℕ → X × X)
⊢ Membership.mem (γ := Set (ℕ × (ℕ → X × X)))
      {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε} E ↔
    Membership.mem (γ := Set (ℕ × (ℕ → X × X)))
      ((fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ⁻¹' Ioo (0 - ε) (0 + ε)) E
have h : ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε → -ε < ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2
Tactic: simp only [mem_setOf_eq, zero_sub, zero_add, mem_preimage, mem_Ioo, iff_and_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ
E : ℕ × (ℕ → X × X)
⊢ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε → -ε < ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2
have h : LE.le (α := ℝ) 0 (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
Tactic: suffices 0 ≤ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
⊢ disjWithin a b = disjWithin b a
have rw : {E : ℕ × (ℕ → ℝ × ℝ) |
    (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc a b ∧ (E.2 i).2 ∈ uIcc a b) ∧
      (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2} =
  disjWithin b a
Tactic: rw [disjWithin, disjWithin, uIcc_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
rw :
  {E : ℕ × (ℕ → ℝ × ℝ) |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc a b ∧ (E.2 i).2 ∈ uIcc a b) ∧
        (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2} =
    disjWithin b a
⊢ disjWithin a b = disjWithin b a
have rw₁ : Eq (α := Set (ℕ × (ℕ → ℝ × ℝ)))
  {E : ℕ × (ℕ → ℝ × ℝ) |
    (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc a b ∧ (E.2 i).2 ∈ uIcc a b) ∧
      (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
  {E : ℕ × (ℕ → ℝ × ℝ) |
    (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc b a ∧ (E.2 i).2 ∈ uIcc b a) ∧
      (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
Tactic: rw [disjWithin, disjWithin, uIcc_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
rw :
  {E : ℕ × (ℕ → ℝ × ℝ) |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc a b ∧ (E.2 i).2 ∈ uIcc a b) ∧
        (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2} =
    disjWithin b a
rw₁ :
  Eq (α := Set (ℕ × (ℕ → ℝ × ℝ)))
    {E : ℕ × (ℕ → ℝ × ℝ) |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc a b ∧ (E.2 i).2 ∈ uIcc a b) ∧
        (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
    {E : ℕ × (ℕ → ℝ × ℝ) |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc b a ∧ (E.2 i).2 ∈ uIcc b a) ∧
        (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
⊢ disjWithin a b = disjWithin b a
have rw₂ : Eq (α := Set (ℕ × (ℕ → ℝ × ℝ)))
  {E : ℕ × (ℕ → ℝ × ℝ) |
    (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc b a ∧ (E.2 i).2 ∈ uIcc b a) ∧
      (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
  {E : ℕ × (ℕ → ℝ × ℝ) |
    (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc b a ∧ (E.2 i).2 ∈ uIcc b a) ∧
      (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
Tactic: rw [disjWithin, disjWithin, uIcc_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
a b : ℝ
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
i : ℕ
hi : i < n
⊢ uIoc (I i).1 (I i).2 ⊆ uIoc a b
have hnI₁ : (∀ i < n, (min a b ≤ (I i).1 ∧ (I i).1 ≤ max a b) ∧ min a b ≤ (I i).2 ∧ (I i).2 ≤ max a b) ∧
  (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
Tactic: simp only [disjWithin, Finset.mem_range, mem_setOf_eq, uIcc, mem_Icc] at hnI
Cleared hypotheses: hnI
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
⊢ ⋃ i ∈ Finset.range n, uIoc (I i).1 (I i).2 ⊆ uIoc a b
have simp : ∀ (i : ℕ) (i_1 : i < n), uIoc (I i).1 (I i).2 ⊆ uIoc a b
Tactic: simp only [iUnion_subset_iff, Finset.mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    totalLengthFilter (𝓝 0)
have hh : Tendsto (β := ENNReal) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2))
  totalLengthFilter (𝓝 0)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (h := fun E ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, (dist (E.2 i).1 (E.2 i).2)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
hh :
  Tendsto (β := ENNReal) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2))
    totalLengthFilter (𝓝 0)
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    totalLengthFilter (𝓝 0)
have hgf : LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal) (fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦ 0) fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
  (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (h := fun E ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, (dist (E.2 i).1 (E.2 i).2)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
hh :
  Tendsto (β := ENNReal) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2))
    totalLengthFilter (𝓝 0)
hgf :
  LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal) (fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦ 0) fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
    (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    totalLengthFilter (𝓝 0)
have hfh : LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal)
  (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
  fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (h := fun E ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, (dist (E.2 i).1 (E.2 i).2)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
⊢ Tendsto (β := ENNReal) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2))
    totalLengthFilter (𝓝 0)
have h : 0 = ENNReal.ofReal 0
Tactic: convert! ENNReal.tendsto_ofReal (Filter.tendsto_comap)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
E : ℕ × (ℕ → ℝ × ℝ)
⊢ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2) ≤
    ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
have hfh : ∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2) ≤
  ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
Tactic: grw [measure_biUnion_finset_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
E : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2) ≤
    ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
have hfh : LE.le (α := ENNReal) (∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2))
  (∑ i ∈ Finset.range E.1, ENNReal.ofReal (dist (E.2 i).1 (E.2 i).2))
Tactic: rw [ENNReal.ofReal_sum_of_nonneg (fun _ _ ↦ dist_nonneg)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
E : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := ENNReal) (∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2))
    (∑ i ∈ Finset.range E.1, ENNReal.ofReal (dist (E.2 i).1 (E.2 i).2))
have hfh : Eq (α := ENNReal) (∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2))
  (∑ i ∈ Finset.range E.1, ENNReal.ofReal (dist (E.2 i).1 (E.2 i).2))
Tactic: apply Eq.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
E : ℕ × (ℕ → ℝ × ℝ)
⊢ Eq (α := ENNReal) (∑ i ∈ Finset.range E.1, (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 i).1 (E.2 i).2))
    (∑ i ∈ Finset.range E.1, ENNReal.ofReal (dist (E.2 i).1 (E.2 i).2))
have hfh : ∀ x ∈ Finset.range E.1,
  (volume : (a : Set ℝ) → ENNReal) (uIoc (E.2 x).1 (E.2 x).2) = ENNReal.ofReal (dist (E.2 x).1 (E.2 x).2)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
      (Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
have hh : Tendsto (β := ENNReal)
  (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
  (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (h := fun E : ℕ × (ℕ → ℝ × ℝ) ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
hh :
  Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
      (Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
have hgf : LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal) (fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦ 0) fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
  (Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (h := fun E : ℕ × (ℕ → ℝ × ℝ) ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
hh :
  Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hgf :
  LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal) (fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦ 0) fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
    (Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
      (Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
have hfh : LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal)
  (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
    (Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
  fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (h := fun E : ℕ × (ℕ → ℝ × ℝ) ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
have hh : totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤ totalLengthFilter
Tactic: apply tendsto_volume_totalLengthFilter_nhds_zero.mono_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
a b : ℝ
E : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := (fun (a : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal) E)
    ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
        ((Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal)
            (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2) :
          ENNReal))
      E)
    ((fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
        ((volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2) : ENNReal))
      E)
have hfh : LE.le (α := ENNReal)
  ((Measure.restrict volume (uIoc a b) : (a : Set ℝ) → ENNReal) (⋃ (i : ℕ), ⋃ (_ : i < E.1), uIoc (E.2 i).1 (E.2 i).2) :
    ENNReal)
  ((volume : (a : Set ℝ) → ENNReal) (⋃ (i : ℕ), ⋃ (_ : i < E.1), uIoc (E.2 i).1 (E.2 i).2) : ENNReal)
Tactic: simp only [Finset.mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
a b c d : ℝ
hf :
  LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)))
    (𝓝 0)
habcd : uIcc c d ⊆ uIcc a b
⊢ LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin c d)))
    (𝓝 0)
have refine : totalLengthFilter ⊓ 𝓟 (disjWithin c d) ≤ totalLengthFilter ⊓ 𝓟 (disjWithin a b)
Tactic: refine le_trans (Filter.map_mono ?_) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
f : ℝ → X
a b c d : ℝ
hf :
  LE.le (α := Filter ℝ)
    (map (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (totalLengthFilter ⊓ 𝓟 (disjWithin a b)))
    (𝓝 0)
habcd : uIcc c d ⊆ uIcc a b
⊢ totalLengthFilter ⊓ 𝓟 (disjWithin c d) ≤ totalLengthFilter ⊓ 𝓟 (disjWithin a b)
have h₂ : disjWithin c d ⊆ disjWithin a b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ AbsolutelyContinuousOnInterval (f + g) a b
have apply : ∀ (t : ℕ × (ℕ → ℝ × ℝ)), LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2))
Tactic: apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using Tendsto.add hf hg)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
apply : ∀ (t : ℕ × (ℕ → ℝ × ℝ)), LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2))
⊢ AbsolutelyContinuousOnInterval (f + g) a b
have apply₁ : ∀ (t : ℕ × (ℕ → ℝ × ℝ)),
  ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤
    HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2))
      (∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2))
Tactic: apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using Tendsto.add hf hg)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤
    HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2))
      (∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2))
have rw : LE.le (α := ℝ) (∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2))
  (∑ x ∈ Finset.range t.1, (dist (f (t.2 x).1) (f (t.2 x).2) + dist (g (t.2 x).1) (g (t.2 x).2)))
Tactic: rw [← Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2))
    (∑ x ∈ Finset.range t.1, (dist (f (t.2 x).1) (f (t.2 x).2) + dist (g (t.2 x).1) (g (t.2 x).2)))
have h : ∀ i ∈ Finset.range t.1,
  dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤ dist (f (t.2 i).1) (f (t.2 i).2) + dist (g (t.2 i).1) (g (t.2 i).2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval (-f) a b
have apply : ∀ (t : ℕ × (ℕ → ℝ × ℝ)), LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2))
Tactic: apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
apply : ∀ (t : ℕ × (ℕ → ℝ × ℝ)), LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2))
⊢ AbsolutelyContinuousOnInterval (-f) a b
have apply₁ : ∀ (t : ℕ × (ℕ → ℝ × ℝ)),
  LE.le (α := ℝ) (∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2))
    (∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2))
Tactic: apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval.{u_2} (X := F) (fun (x : ℝ) ↦ α • f x) a b
have apply : ∀ (t : ℕ × (ℕ → ℝ × ℝ)),
  LE.le (α := ℝ) 0
    (∑ i ∈ Finset.range t.1,
      dist.{u_2} (α := F) ((fun (x : ℝ) ↦ α • f x) (t.2 i).1) ((fun (x : ℝ) ↦ α • f x) (t.2 i).2))
Tactic: apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf.const_mul ‖α‖)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
apply :
  ∀ (t : ℕ × (ℕ → ℝ × ℝ)),
    LE.le (α := ℝ) 0
      (∑ i ∈ Finset.range t.1,
        dist.{u_2} (α := F) ((fun (x : ℝ) ↦ α • f x) (t.2 i).1) ((fun (x : ℝ) ↦ α • f x) (t.2 i).2))
⊢ AbsolutelyContinuousOnInterval.{u_2} (X := F) (fun (x : ℝ) ↦ α • f x) a b
have apply₁ : ∀ (t : ℕ × (ℕ → ℝ × ℝ)),
  ∑ i ∈ Finset.range t.1, dist.{u_2} (α := F) ((fun (x : ℝ) ↦ α • f x) (t.2 i).1) ((fun (x : ℝ) ↦ α • f x) (t.2 i).2) ≤
    ‖α‖ * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)
Tactic: apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf.const_mul ‖α‖)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
⊢ uniformity X = comap (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter
have refine : HasBasis.{u_1, 1} (α := X × X)
  (comap (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter) (fun (ε : ℝ) ↦ 0 < ε)
  fun (ε : ℝ) ↦ {p : X × X | dist p.1 p.2 < ε}
Tactic: refine Filter.HasBasis.eq_of_same_basis Metric.uniformity_basis_dist ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
⊢ HasBasis.{u_1, 1} (α := X × X)
    (comap (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter) (fun (ε : ℝ) ↦ 0 < ε)
    fun (ε : ℝ) ↦ {p : X × X | dist p.1 p.2 < ε}
have h : ∀ (x : ℝ),
  Eq.{u_1 + 1} (α := Set (X × X)) {p : X × X | dist p.1 p.2 < x}
    (preimage (β := ℕ × (ℕ → X × X)) (fun (x : X × X) ↦ (1, fun (x_1 : ℕ) ↦ x))
      {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < x})
Tactic: convert! hasBasis_totalLengthFilter.comap _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ UniformContinuousOn f (uIcc a b)
have simp : comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) ≤
  comap.{0, u_2} (β := F × F) (fun (x : ℝ × ℝ) ↦ (f x.1, f x.2))
    (comap (β := ℕ × (ℕ → F × F)) (fun (x : F × F) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter)
Tactic: simp only [UniformContinuousOn, Filter.tendsto_iff_comap, uniformity_eq_comap_totalLengthFilter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (hypothesis)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) ≤
    comap.{0, u_2} (β := F × F) (fun (x : ℝ × ℝ) ↦ (f x.1, f x.2))
      (comap (β := ℕ × (ℕ → F × F)) (fun (x : F × F) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter)
have hf₁ : totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
  comap (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)
Tactic: simp only [AbsolutelyContinuousOnInterval, Filter.tendsto_iff_comap] at hf
Cleared hypotheses: hf