awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ b ∈ s ∩ Icc b c

Tactic:
⟨bs, le_rfl, bc⟩

Premises used: le_rfl, Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ c ∈ s ∩ Icc b c

Tactic:
⟨cs, bc, le_rfl⟩

Premises used: le_rfl, Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ b ∈ s ∩ Icc b c

Tactic:
exacts [⟨bs, le_rfl, bc⟩, ⟨cs, bc, le_rfl⟩]
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
rw : variationOnFromTo f s b c = variationOnFromTo f s a b + variationOnFromTo f s b c - variationOnFromTo f s a b
rw₁ rw₂ : variationOnFromTo f s b c = variationOnFromTo f s b c
⊢ variationOnFromTo f s b c = variationOnFromTo f s a c - variationOnFromTo f s a b

Tactic:
rw [← variationOnFromTo.add hf as bs cs, add_sub_cancel_left]

Premises used: add_sub_cancel_left, variationOnFromTo.add
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
f₁ : |f c - f b| = dist (f b) (f c)
f₂ : dist (f b) (f c) ≤ variationOnFromTo f s b c
f₃ : variationOnFromTo f s b c = variationOnFromTo f s a c - variationOnFromTo f s a b
⊢ f c - f b ≤ variationOnFromTo f s a c - variationOnFromTo f s a b

Tactic:
calc
    f c - f b ≤ |f c - f b| := le_abs_self _
    _ = dist (f b) (f c) := by rw [dist_comm, Real.dist_eq]
    _ ≤ variationOnFromTo f s b c := by
      rw [variationOnFromTo.eq_of_le f s bc, dist_edist]
      apply ENNReal.toReal_mono (hf b c bs cs)
      apply eVariationOn.edist_le f
      exacts [⟨bs, le_rfl, bc⟩, ⟨cs, bc, le_rfl⟩]
    _ = variationOnFromTo f s a c - variationOnFromTo f s a b := by
      rw [← variationOnFromTo.add hf as bs cs, add_sub_cancel_left]

Premises used: le_abs_self, variationOnFromTo, Dist.dist
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
inl : ∀ (h : x ≤ y), variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
inr : ∀ (h : y ≤ x), variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
rcases le_total x y with (h | h)

Premises used: le_total
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
inl : (eVariationOn (f ∘ φ) (t ∩ Icc x y)).toReal = variationOnFromTo f (φ '' t) (φ x) (φ y)
inl₁ : (eVariationOn (f ∘ φ) (t ∩ Icc x y)).toReal = (eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))).toReal
inl₂ inl₃ : (eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))).toReal = (eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))).toReal
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
rw [variationOnFromTo.eq_of_le _ _ h, variationOnFromTo.eq_of_le _ _ (hφ hx hy h),
      eVariationOn.comp_inter_Icc_eq_of_monotoneOn f φ hφ hx hy]

Premises used: eVariationOn.comp_inter_Icc_eq_of_monotoneOn, variationOnFromTo.eq_of_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
inr : -(eVariationOn (f ∘ φ) (t ∩ Icc y x)).toReal = variationOnFromTo f (φ '' t) (φ x) (φ y)
inr₁ : -(eVariationOn (f ∘ φ) (t ∩ Icc y x)).toReal = -(eVariationOn f (φ '' t ∩ Icc (φ y) (φ x))).toReal
inr₂ inr₃ : -(eVariationOn f (φ '' t ∩ Icc (φ y) (φ x))).toReal = -(eVariationOn f (φ '' t ∩ Icc (φ y) (φ x))).toReal
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
rw [variationOnFromTo.eq_of_ge _ _ h, variationOnFromTo.eq_of_ge _ _ (hφ hy hx h),
      eVariationOn.comp_inter_Icc_eq_of_monotoneOn f φ hφ hy hx]

Premises used: variationOnFromTo.eq_of_ge, eVariationOn.comp_inter_Icc_eq_of_monotoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
h : ∀ (y : α), variationOnFromTo f univ a y = variationOnFromTo f univ a x + variationOnFromTo f univ x y
⊢ variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y

Tactic:
ext y
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
y : α
h h₁ : variationOnFromTo f univ a y = variationOnFromTo f univ a y
⊢ variationOnFromTo f univ a y = variationOnFromTo f univ a x + variationOnFromTo f univ x y

Tactic:
rw [variationOnFromTo.add hf.locallyBoundedVariationOn (mem_univ _) (mem_univ _) (mem_univ _)]

Premises used: BoundedVariationOn.locallyBoundedVariationOn, variationOnFromTo.add, Set.mem_univ
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
⊢ variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y

Tactic:
have : variationOnFromTo f univ a =
      fun y ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y := by
    ext y
    rw [variationOnFromTo.add hf.locallyBoundedVariationOn (mem_univ _) (mem_univ _) (mem_univ _)]
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
rw : ContinuousWithinAt (Y := ℝ) (fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y) (Ici x) x
⊢ ContinuousWithinAt (variationOnFromTo f univ a) (Ici x) x

Tactic:
rw [this]
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
apply : ContinuousWithinAt (variationOnFromTo f univ x) (Ici x) x
⊢ ContinuousWithinAt (Y := ℝ) (fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y) (Ici x) x

Tactic:
apply continuousWithinAt_const.add

Premises used: ContinuousWithinAt.add, continuousWithinAt_const
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
H : ContinuousWithinAt (Y := ℝ) (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (Ici x) x
y : α
hy : y ∈ Ici x
⊢ variationOnFromTo f univ x y = (eVariationOn f (univ ∩ Icc x y)).toReal

Tactic:
grind [variationOnFromTo]

Premises used: variationOnFromTo
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
suffices : ContinuousWithinAt (Y := ℝ) (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (Ici x) x
⊢ ContinuousWithinAt (variationOnFromTo f univ x) (Ici x) x

Tactic:
suffices H : ContinuousWithinAt (fun y ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (Ici x) x from
    H.congr_of_mem (fun y hy ↦ by grind [variationOnFromTo]) self_mem_Iic
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
simp :
  Tendsto (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (𝓝[≥] x) (𝓝 (eVariationOn f (univ ∩ {x})).toReal)
⊢ ContinuousWithinAt (Y := ℝ) (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (Ici x) x

Tactic:
simp only [ContinuousWithinAt, Icc_self]

Premises used: Set.Icc_self, ContinuousWithinAt
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
⊢ Set.Subsingleton (α := α) (univ ∩ {x})

Tactic:
grind [Set.Subsingleton]

Premises used: Set.Subsingleton
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
rw : Tendsto (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (𝓝[≥] x) (𝓝 (ENNReal.toReal 0))
⊢ Tendsto (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (𝓝[≥] x) (𝓝 (eVariationOn f (univ ∩ {x})).toReal)

Tactic:
rw [eVariationOn.subsingleton _ (by grind [Set.Subsingleton])]

Premises used: eVariationOn.subsingleton
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
apply : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (univ ∩ Icc x y)) (𝓝[≥] x) (𝓝 0)
⊢ Tendsto (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (𝓝[≥] x) (𝓝 (ENNReal.toReal 0))

Tactic:
apply (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp

Premises used: ENNReal.tendsto_toReal, ENNReal.zero_ne_top, Filter.Tendsto.comp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
apply : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (univ ∩ Icc x y)) (𝓝[univ] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (univ ∩ Icc x y)) (𝓝[≥] x) (𝓝 0)

Tactic:
apply Tendsto.mono_left _ (nhdsWithin_mono _ (subset_univ _))

Premises used: Set.subset_univ, Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
⊢ ContinuousWithinAt f (univ ∩ Ici x) x

Tactic:
simpa using hx
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (univ ∩ Icc x y)) (𝓝[univ] x) (𝓝 0)

Tactic:
exact hf.tendsto_eVariationOn_Icc_zero_right _ (by simpa using hx)

Premises used: BoundedVariationOn.tendsto_eVariationOn_Icc_zero_right
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space E
inst_5 : CompleteSpace E
hf : BoundedVariationOn f univ
a x : α
⊢ ContinuousWithinAt (variationOnFromTo (Function.rightLim f) univ a) (Ici x) x

Tactic:
hf.rightLim.continuousWithinAt_variationOnFromTo_Ici hf.continuousWithinAt_rightLim

Premises used: BoundedVariationOn.continuousWithinAt_variationOnFromTo_Ici, BoundedVariationOn.rightLim, BoundedVariationOn.continuousWithinAt_rightLim
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
inl : ∀ (h : LocallyBoundedVariationOn f ∅), ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p ∅ ∧ MonotoneOn q ∅ ∧ f = p - q
inr : ∀ (c : α) (cs : c ∈ s), ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q
⊢ ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨c, cs⟩)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
h : LocallyBoundedVariationOn f ∅
⊢ ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p ∅ ∧ MonotoneOn q ∅ ∧ f = p - q

Tactic:
⟨f, 0, subsingleton_empty.monotoneOn _, subsingleton_empty.monotoneOn _,
      (sub_zero f).symm⟩

Premises used: sub_zero, Set.Subsingleton.monotoneOn, Set.subsingleton_empty, And.intro, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
h : LocallyBoundedVariationOn f ∅
⊢ ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p ∅ ∧ MonotoneOn q ∅ ∧ f = p - q

Tactic:
exact ⟨f, 0, subsingleton_empty.monotoneOn _, subsingleton_empty.monotoneOn _,
      (sub_zero f).symm⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q

Tactic:
⟨_, _, variationOnFromTo.monotoneOn h cs, variationOnFromTo.sub_self_monotoneOn h cs,
      (sub_sub_cancel _ _).symm⟩

Premises used: sub_sub_cancel, variationOnFromTo.sub_self_monotoneOn, And.intro, variationOnFromTo.monotoneOn, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q

Tactic:
exact ⟨_, _, variationOnFromTo.monotoneOn h cs, variationOnFromTo.sub_self_monotoneOn h cs,
      (sub_sub_cancel _ _).symm⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : 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 : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
apply :
  ∀ (i : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    ∑ i_1 ∈ Finset.range i.1, edist ((f ∘ g) ((↑i.2 : ℕ → α) (i_1 + 1))) ((f ∘ g) ((↑i.2 : ℕ → α) i_1)) ≤
      (↑C : ℝ≥0∞) * eVariationOn g s
⊢ eVariationOn (f ∘ g) s ≤ (↑C : ℝ≥0∞) * eVariationOn g s

Tactic:
apply iSup_le _

Premises used: iSup_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : 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 : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (g (u (i + 1)))) (f (g (u i))))
    (∑ i ∈ Finset.range n, (↑C : ℝ≥0∞) * edist (g (u (i + 1))) (g (u i)))

Tactic:
Finset.sum_le_sum fun i _ => h (hg (us _)) (hg (us _))

Premises used: HAdd.hAdd, Finset.sum_le_sum, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : 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 : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
rw rw₁ :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, (↑C : ℝ≥0∞) * edist (g (u (i + 1))) (g (u i)))
    (∑ i ∈ Finset.range n, (↑C : ℝ≥0∞) * edist (g (u (i + 1))) (g (u i)))
⊢ ∑ i ∈ Finset.range n, (↑C : ℝ≥0∞) * edist (g (u (i + 1))) (g (u i)) =
    (↑C : ℝ≥0∞) * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i))

Tactic:
rw [Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : 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 : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
grw grw₁ : (↑C : ℝ≥0∞) * eVariationOn g s ≤ (↑C : ℝ≥0∞) * eVariationOn g s
⊢ (↑C : ℝ≥0∞) * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i)) ≤ (↑C : ℝ≥0∞) * eVariationOn g s

Tactic:
grw [eVariationOn.sum_le hu us]

Premises used: eVariationOn.sum_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : 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 : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
i :
  ∑ i ∈ Finset.range n, (↑C : ℝ≥0∞) * edist (g (u (i + 1))) (g (u i)) =
    (↑C : ℝ≥0∞) * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i))
i₁ : (↑C : ℝ≥0∞) * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i)) ≤ (↑C : ℝ≥0∞) * eVariationOn g s
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist
        ((f ∘ g) ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        ((f ∘ g) ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i)) ≤
    (↑C : ℝ≥0∞) * eVariationOn g s

Tactic:
calc
    (∑ i ∈ Finset.range n, edist (f (g (u (i + 1)))) (f (g (u i)))) ≤
        ∑ i ∈ Finset.range n, C * edist (g (u (i + 1))) (g (u i)) :=
      Finset.sum_le_sum fun i _ => h (hg (us _)) (hg (us _))
    _ = C * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i)) := by rw [Finset.mul_sum]
    _ ≤ C * eVariationOn g s := by grw [eVariationOn.sum_le hu us]

Premises used: eVariationOn, Finset.range, HAdd.hAdd, Finset.sum_le_sum, EDist.edist, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : 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 : ℝ≥0
t : Set E
hf : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
h : BoundedVariationOn g s
⊢ (↑C : ℝ≥0∞) * eVariationOn g s ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : 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 : ℝ≥0
t : Set E
hf : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
h : LocallyBoundedVariationOn g s
⊢ LocallyBoundedVariationOn (f ∘ g) s

Tactic:
fun x y xs ys =>
  hf.comp_boundedVariationOn (hg.mono_left inter_subset_left) (h x y xs ys)

Premises used: LocallyBoundedVariationOn, Set.inter_subset_left, Set.MapsTo.mono_left, LipschitzOnWith.comp_boundedVariationOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : 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 : ℝ≥0
hf : LipschitzWith C f
g : α → E
s : Set α
h : BoundedVariationOn g s
⊢ BoundedVariationOn (f ∘ g) s

Tactic:
hf.lipschitzOnWith.comp_boundedVariationOn (mapsTo_univ _ _) h

Premises used: Set.mapsTo_univ, LipschitzOnWith.comp_boundedVariationOn, LipschitzWith.lipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : 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 : ℝ≥0
hf : LipschitzWith C f
g : α → E
s : Set α
h : LocallyBoundedVariationOn g s
⊢ LocallyBoundedVariationOn (f ∘ g) s

Tactic:
hf.lipschitzOnWith.comp_locallyBoundedVariationOn (mapsTo_univ _ _) h

Premises used: Set.mapsTo_univ, LipschitzOnWith.comp_locallyBoundedVariationOn, LipschitzWith.lipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
C : ℝ≥0
s : Set ℝ
hf : LipschitzOnWith C f s
⊢ LocallyBoundedVariationOn f s

Tactic:
hf.comp_locallyBoundedVariationOn (mapsTo_id _)
    (@monotoneOn_id ℝ _ s).locallyBoundedVariationOn

Premises used: Set.mapsTo_id, MonotoneOn.locallyBoundedVariationOn, LipschitzOnWith.comp_locallyBoundedVariationOn, monotoneOn_id
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
C : ℝ≥0
hf : LipschitzWith C f
s : Set ℝ
⊢ LocallyBoundedVariationOn f s

Tactic:
hf.lipschitzOnWith.locallyBoundedVariationOn

Premises used: LipschitzWith.lipschitzOnWith, LipschitzOnWith.locallyBoundedVariationOn
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : LT β
U : Filter (α × α)
z : β
D : α → α → β
H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s
s : Set (α × α)
⊢ s ∈ U ↔ ∃ i > z, {p : α × α | D p.1 p.2 < i} ⊆ s

Tactic:
simp only [H, subset_def, Prod.forall, mem_setOf]

Premises used: Set.subset_def, Set.mem_setOf, Prod.forall
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : EDist α
x y : α
ε : ℝ≥0∞
⊢ y ∈ eball x ε ↔ edist y x < ε

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Metric.eball