∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {F : Type u_3}
  [inst_2 : PseudoEMetricSpace F] {f : E → F} {C : NNReal} {t : Set E},
  LipschitzOnWith C f t → ∀ {g : α → E} {s : Set α}, Set.MapsTo g s t → eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s