awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
⊢ LE.le (α := Filter (ℝ × ℝ))
    (comap (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)))
    (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:
Filter.comap_mono hf

Premises used: Filter.comap_mono
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)))
convert_2 : ℝ × ℝ → ℕ × (ℕ → ℝ × ℝ)
⊢ 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:
convert! Filter.comap_mono hf

Premises used: Filter.comap_mono
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 ⊓
      𝓟 ((fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b)
⊢ 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:
simp only [comap_inf, comap_principal]

Premises used: Filter.comap_inf, Filter.comap_principal
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 : uIcc a b ×ˢ uIcc a b = (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b
⊢ 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:
congr
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 :
  ∀ (p : ℝ × ℝ),
    p ∈ uIcc a b ×ˢ uIcc a b ↔
      Membership.mem (γ := Set (ℝ × ℝ)) ((fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b) p
⊢ uIcc a b ×ˢ uIcc a b = (fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b

Tactic:
ext p
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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 : ℝ × ℝ
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
⊢ p ∈ uIcc a b ×ˢ uIcc a b ↔
    Membership.mem (γ := Set (ℝ × ℝ)) ((fun (x : ℝ × ℝ) ↦ (1, fun (x_1 : ℕ) ↦ x)) ⁻¹' disjWithin a b) p

Tactic:
simp only [disjWithin, Finset.mem_range, preimage_setOf_eq, Nat.lt_one_iff,
      forall_eq, mem_setOf_eq, mem_prod]

Premises used: forall_eq, Set.mem_setOf_eq, Finset.mem_range, AbsolutelyContinuousOnInterval.disjWithin, Set.preimage_setOf_eq, Set.mem_prod, Nat.lt_one_iff
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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.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
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
⊢ 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:
simp [totalLengthFilter, comap_comap, Function.comp_def]

Premises used: Function.comp_def, Filter.comap_comap, AbsolutelyContinuousOnInterval.totalLengthFilter
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ ContinuousOn f (uIcc a b)

Tactic:
hf.uniformContinuousOn.continuousOn

Premises used: AbsolutelyContinuousOnInterval.uniformContinuousOn, UniformContinuousOn.continuousOn
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ ∃ (C : ℝ), ∀ x ∈ uIcc a b, ‖f x‖ ≤ C

Tactic:
isCompact_Icc.exists_bound_of_continuousOn (hf.continuousOn)

Premises used: Set.Mem, CompactIccSpace.isCompact_Icc, IsCompact.exists_bound_of_continuousOn, Set.uIcc, AbsolutelyContinuousOnInterval.continuousOn
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
obtain : ∀ (C : ℝ) (hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C), AbsolutelyContinuousOnInterval (f • g) a b
⊢ AbsolutelyContinuousOnInterval (f • g) a b

Tactic:
obtain ⟨C, hC⟩ := hf.exists_bound

Premises used: AbsolutelyContinuousOnInterval.exists_bound
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
obtain : ∀ (D : ℝ) (hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D), AbsolutelyContinuousOnInterval (f • g) a b
⊢ AbsolutelyContinuousOnInterval (f • g) a b

Tactic:
obtain ⟨D, hD⟩ := hg.exists_bound

Premises used: AbsolutelyContinuousOnInterval.exists_bound
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
⊢ Tendsto (β := ℝ)
    (fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦
      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))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
simpa using (hg.const_mul C).add (hf.const_mul D)

Premises used: Filter.Tendsto.const_mul, Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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))
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)
⊢ AbsolutelyContinuousOnInterval (f • g) a b

Tactic:
apply squeeze_zero' ?_ ?_
    (by simpa using (hg.const_mul C).add (hf.const_mul D))

Premises used: squeeze_zero'
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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),
    LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((f • g) (t.2 i).1) ((f • g) (t.2 i).2))

Tactic:
Filter.Eventually.of_forall <| fun _ ↦ Finset.sum_nonneg (fun i hi ↦ dist_nonneg)

Premises used: dist_nonneg, Filter.Eventually.of_forall, Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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),
    LE.le (α := ℝ) 0 (∑ i ∈ Finset.range t.1, dist ((f • g) (t.2 i).1) ((f • g) (t.2 i).2))

Tactic:
exact Filter.Eventually.of_forall <| fun _ ↦ Finset.sum_nonneg (fun i hi ↦ dist_nonneg)

Premises used: dist_nonneg, Filter.Eventually.of_forall, Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
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)
⊢ ∀ᶠ (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:
rw [eventually_inf_principal]

Premises used: Filter.eventually_inf_principal
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
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)
⊢ ∀ᶠ (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:
filter_upwards with (n, I) hnI
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
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)))
⊢ ∑ 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:
simp only [Finset.mul_sum, ← Finset.sum_add_distrib]

Premises used: Finset.mul_sum, Finset.sum_add_distrib
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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
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)
⊢ 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:
gcongr with i hi
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
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)
⊢ 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:
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)

Premises used: Prod.fst, HSMul.hSMul, Dist.dist, Prod.snd
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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) ≤
    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:
dist_triangle _ _ _

Premises used: dist_triangle
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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) ≤
    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:
exact dist_triangle _ _ _

Premises used: dist_triangle
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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)
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)
⊢ 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:
gcongr
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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₁ : ‖f (I i).1‖ * dist (g (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) ≤ C * dist (g (I i).1) (g (I i).2)

Tactic:
rw [dist_smul₀]

Premises used: dist_smul₀
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
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₁ : ‖f (I i).1‖ ≤ C
⊢ ‖f (I i).1‖ * dist (g (I i).1) (g (I i).2) ≤ C * dist (g (I i).1) (g (I i).2)

Tactic:
gcongr