awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
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)
⊢ 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 h : comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) =
  comap (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
Tactic: convert! Filter.comap_mono hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
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)
h :
  comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) =
    comap (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) (totalLengthFilter ⊓ 𝓟 (disjWithin 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 h₁ : Eq (α := Filter (ℝ × ℝ))
  (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))
  (comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x))
    (comap (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)))
Tactic: convert! Filter.comap_mono hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
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)
h :
  comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) =
    comap (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
h₁ :
  Eq (α := Filter (ℝ × ℝ))
    (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))
    (comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x))
      (comap (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)))
⊢ 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 convert_2 : ℝ × ℝ → ℕ × (ℕ → ℝ × ℝ)
Tactic: convert! Filter.comap_mono hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
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)
⊢ comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) =
    comap (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
have h : comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) =
  comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓
    𝓟 ((fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b)
Tactic: simp only [comap_inf, comap_principal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
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)
⊢ comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) =
    comap (β := ℕ × (ℕ → ℝ × ℝ)) (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) totalLengthFilter ⊓
      𝓟 ((fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b)
have h : uIcc a b ×ˢ uIcc a b = (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
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)
⊢ uIcc a b ×ˢ uIcc a b = (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b
have h : ∀ (p : ℝ × ℝ),
  p ∈ uIcc a b ×ˢ uIcc a b ↔
    Membership.mem (γ := Set (ℝ × ℝ)) ((fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
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)
p : ℝ × ℝ
⊢ p ∈ uIcc a b ×ˢ uIcc a b ↔
    Membership.mem (γ := Set (ℝ × ℝ)) ((fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b) p
have h : p.1 ∈ uIcc a b ∧ p.2 ∈ uIcc a b ↔
  (p.1 ∈ uIcc a b ∧ p.2 ∈ uIcc a b) ∧
    (↑(Finset.range 1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc p.1 p.2
Tactic: simp only [disjWithin, Finset.mem_range, preimage_setOf_eq, Nat.lt_one_iff,
      forall_eq, mem_setOf_eq, mem_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ AbsolutelyContinuousOnInterval (f • g) a b
have obtain : ∀ (C : ℝ) (hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C), AbsolutelyContinuousOnInterval (f • g) a b
Tactic: obtain ⟨C, hC⟩ := hf.exists_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
⊢ AbsolutelyContinuousOnInterval (f • g) a b
have obtain : ∀ (D : ℝ) (hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D), AbsolutelyContinuousOnInterval (f • g) a b
Tactic: obtain ⟨D, hD⟩ := hg.exists_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ AbsolutelyContinuousOnInterval (f • g) a b
have apply : ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
  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' ?_ ?_
    (by simpa using (hg.const_mul C).add (hf.const_mul D))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
apply :
  ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    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 : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
  ∑ i ∈ Finset.range t.1, dist ((f • g) (t.2 i).1) ((f • g) (t.2 i).2) ≤
    C * ∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2) +
      D * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)
Tactic: apply squeeze_zero' ?_ ?_
    (by simpa using (hg.const_mul C).add (hf.const_mul D))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ i ∈ Finset.range t.1, dist ((f • g) (t.2 i).1) ((f • g) (t.2 i).2) ≤
      C * ∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2) +
        D * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)
have rw : ∀ᶠ (x : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter,
  x ∈ disjWithin a b →
    ∑ i ∈ Finset.range x.1, dist ((f • g) (x.2 i).1) ((f • g) (x.2 i).2) ≤
      C * ∑ i ∈ Finset.range x.1, dist (g (x.2 i).1) (g (x.2 i).2) +
        D * ∑ i ∈ Finset.range x.1, dist (f (x.2 i).1) (f (x.2 i).2)
Tactic: rw [eventually_inf_principal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ ∀ᶠ (x : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter,
    x ∈ disjWithin a b →
      ∑ i ∈ Finset.range x.1, dist ((f • g) (x.2 i).1) ((f • g) (x.2 i).2) ≤
        C * ∑ i ∈ Finset.range x.1, dist (g (x.2 i).1) (g (x.2 i).2) +
          D * ∑ i ∈ Finset.range x.1, dist (f (x.2 i).1) (f (x.2 i).2)
have h : ∀ (n : ℕ) (I : ℕ → ℝ × ℝ) (hnI : (n, I) ∈ disjWithin a b),
  ∑ i ∈ Finset.range (n, I).1, dist ((f • g) ((n, I).2 i).1) ((f • g) ((n, I).2 i).2) ≤
    C * ∑ i ∈ Finset.range (n, I).1, dist (g ((n, I).2 i).1) (g ((n, I).2 i).2) +
      D * ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2)
Tactic: filter_upwards with (n, I) hnI
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
⊢ ∑ i ∈ Finset.range (n, I).1, dist ((f • g) ((n, I).2 i).1) ((f • g) ((n, I).2 i).2) ≤
    C * ∑ i ∈ Finset.range (n, I).1, dist (g ((n, I).2 i).1) (g ((n, I).2 i).2) +
      D * ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2)
have h : LE.le (α := ℝ) (∑ x ∈ Finset.range n, dist ((f • g) (I x).1) ((f • g) (I x).2))
  (∑ x ∈ Finset.range n, (C * dist (g (I x).1) (g (I x).2) + D * dist (f (I x).1) (f (I x).2)))
Tactic: simp only [Finset.mul_sum, ← Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.range n, dist ((f • g) (I x).1) ((f • g) (I x).2))
    (∑ x ∈ Finset.range n, (C * dist (g (I x).1) (g (I x).2) + D * dist (f (I x).1) (f (I x).2)))
have h : ∀ (i : ℕ) (hi : i ∈ Finset.range n),
  dist ((f • g) (I i).1) ((f • g) (I i).2) ≤ C * dist (g (I i).1) (g (I i).2) + D * dist (f (I i).1) (f (I i).2)
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
i : ℕ
hi : i ∈ Finset.range n
⊢ dist ((f • g) (I i).1) ((f • g) (I i).2) ≤ C * dist (g (I i).1) (g (I i).2) + D * dist (f (I i).1) (f (I i).2)
have trans : dist ((f • g) (I i).1) ((f • g) (I i).2) ≤
  dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) + dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2)
Tactic: trans dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) +
    dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
i : ℕ
hi : i ∈ Finset.range n
trans :
  dist ((f • g) (I i).1) ((f • g) (I i).2) ≤
    dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) + dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2)
⊢ dist ((f • g) (I i).1) ((f • g) (I i).2) ≤ C * dist (g (I i).1) (g (I i).2) + D * dist (f (I i).1) (f (I i).2)
have trans₁ : dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) + dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤
  C * dist (g (I i).1) (g (I i).2) + D * dist (f (I i).1) (f (I i).2)
Tactic: trans dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) +
    dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) + dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤
    C * dist (g (I i).1) (g (I i).2) + D * dist (f (I i).1) (f (I i).2)
have h₁ : dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) ≤ C * dist (g (I i).1) (g (I i).2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
h₁ : dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) ≤ C * dist (g (I i).1) (g (I i).2)
⊢ dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) + dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤
    C * dist (g (I i).1) (g (I i).2) + D * dist (f (I i).1) (f (I i).2)
have h₂ : dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ D * dist (f (I i).1) (f (I i).2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) ≤ C * dist (g (I i).1) (g (I i).2)
have h₁ : ‖f (I i).1‖ * dist (g (I i).1) (g (I i).2) ≤ C * dist (g (I i).1) (g (I i).2)
Tactic: rw [dist_smul₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ ‖f (I i).1‖ * dist (g (I i).1) (g (I i).2) ≤ C * dist (g (I i).1) (g (I i).2)
have h₁ : ‖f (I i).1‖ ≤ C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ D * dist (f (I i).1) (f (I i).2)
have h₂ : dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ dist (f (I i).1) (f (I i).2) * D
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AbsolutelyContinuous (goal)
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst_1 : SeminormedRing M
inst_2 : Module M F
inst_3 : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
hg :
  Tendsto (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ dist (f (I i).1) (f (I i).2) * D
have h₂ : dist (f (I i).1) (f (I i).2) * dist (g (I i).2) 0 ≤ dist (f (I i).1) (f (I i).2) * D
Tactic: grw [dist_pair_smul]