awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 c - f b ≤ variationOnFromTo f s a c - variationOnFromTo f s a b
have f₃ : variationOnFromTo f s b c = 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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
have inl : ∀ (h : x ≤ y), variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
Tactic: rcases le_total x y with (h | h)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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)
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
have inr : ∀ (h : y ≤ x), variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
Tactic: rcases le_total x y with (h | h)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
have inl : (eVariationOn (f ∘ φ) (t ∩ Icc x y)).toReal = 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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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)
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
have inl₁ : (eVariationOn (f ∘ φ) (t ∩ Icc x y)).toReal = (eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))).toReal
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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
have inl₂ : (eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))).toReal = (eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))).toReal
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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
have inr : -(eVariationOn (f ∘ φ) (t ∩ Icc y x)).toReal = 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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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)
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
have inr₁ : -(eVariationOn (f ∘ φ) (t ∩ Icc y x)).toReal = -(eVariationOn f (φ '' t ∩ Icc (φ y) (φ x))).toReal
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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
have inr₂ : -(eVariationOn f (φ '' t ∩ Icc (φ y) (φ x))).toReal = -(eVariationOn f (φ '' t ∩ Icc (φ y) (φ x))).toReal
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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
have h : ∀ (y : α), variationOnFromTo f univ a y = variationOnFromTo f univ a x + variationOnFromTo f univ x y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 : α
⊢ variationOnFromTo f univ a y = variationOnFromTo f univ a x + variationOnFromTo f univ x y
have h : variationOnFromTo f univ a y = variationOnFromTo f univ a y
Tactic: rw [variationOnFromTo.add hf.locallyBoundedVariationOn (mem_univ _) (mem_univ _) (mem_univ _)]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
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
⊢ ContinuousWithinAt (variationOnFromTo f univ a) (Ici x) x
have this : 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 _)]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 (variationOnFromTo f univ a) (Ici x) x
have rw : ContinuousWithinAt (Y := ℝ) (fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y) (Ici x) x
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 (Y := ℝ) (fun (y : α) ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y) (Ici x) x
have apply : ContinuousWithinAt (variationOnFromTo f univ x) (Ici x) x
Tactic: apply continuousWithinAt_const.add
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 (variationOnFromTo f univ x) (Ici x) x
have suffices : ContinuousWithinAt (Y := ℝ) (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (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
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 (Y := ℝ) (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (Ici x) x
have simp : Tendsto (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (𝓝[≥] x) (𝓝 (eVariationOn f (univ ∩ {x})).toReal)
Tactic: simp only [ContinuousWithinAt, Icc_self]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (𝓝[≥] x) (𝓝 (eVariationOn f (univ ∩ {x})).toReal)
have rw : Tendsto (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (𝓝[≥] x) (𝓝 (ENNReal.toReal 0))
Tactic: rw [eVariationOn.subsingleton _ (by grind [Set.Subsingleton])]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 (fun (y : α) ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (𝓝[≥] x) (𝓝 (ENNReal.toReal 0))
have apply : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (univ ∩ Icc x y)) (𝓝[≥] x) (𝓝 0)
Tactic: apply (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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)) (𝓝[≥] x) (𝓝 0)
have apply : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (univ ∩ Icc x y)) (𝓝[univ] x) (𝓝 0)
Tactic: apply Tendsto.mono_left _ (nhdsWithin_mono _ (subset_univ _))
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
⊢ ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q
have inl : ∀ (h : LocallyBoundedVariationOn f ∅), ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p ∅ ∧ MonotoneOn q ∅ ∧ f = p - q
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨c, cs⟩)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q
have inr : ∀ (c : α) (cs : c ∈ s), ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨c, cs⟩)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ eVariationOn (f ∘ g) s ≤ (↑C : ℝ≥0∞) * eVariationOn g s
have 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
Tactic: apply iSup_le _
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 ∈ 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))
have 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)))
Tactic: rw [Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ (↑C : ℝ≥0∞) * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i)) ≤ (↑C : ℝ≥0∞) * eVariationOn g s
have grw : (↑C : ℝ≥0∞) * eVariationOn g s ≤ (↑C : ℝ≥0∞) * eVariationOn g s
Tactic: grw [eVariationOn.sum_le hu us]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 ∈ 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
have 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: 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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 ∈ 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
have i₁ : (↑C : ℝ≥0∞) * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u 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]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u_2
m m' : PseudoEMetricSpace α
h : Eq.{u_2 + 1} (α := EDist α) toEDist toEDist
⊢ m = m'
have obtain : ∀ [toEDist : EDist α] (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x)
  (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) (U : UniformSpace α)
  (hU : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε})
  (h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist),
  { toEDist := toEDist, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
      toUniformSpace := U, uniformity_edist := hU : PseudoEMetricSpace α } =
    m'
Tactic: obtain ⟨_, _, _, U, hU⟩ := m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u_2
m' : PseudoEMetricSpace α
ed : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
h : Eq.{u_2 + 1} (α := EDist α) toEDist toEDist
⊢ { toEDist := ed, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
      toUniformSpace := U, uniformity_edist := hU : PseudoEMetricSpace α } =
    m'
have obtain : ∀ [toEDist : EDist α] (edist_self_1 : ∀ (x : α), edist x x = 0) (edist_comm_1 : ∀ (x y : α), edist x y = edist y x)
  (edist_triangle_1 : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) (U' : UniformSpace α)
  (hU' : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε})
  (h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist),
  { toEDist := ed, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
      toUniformSpace := U, uniformity_edist := hU : PseudoEMetricSpace α } =
    { toEDist := toEDist, edist_self := edist_self_1, edist_comm := edist_comm_1, edist_triangle := edist_triangle_1,
      toUniformSpace := U', uniformity_edist := hU' }
Tactic: obtain ⟨_, _, _, U', hU'⟩ := m'
Cleared hypotheses: m', h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u_2
ed : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
ed' : EDist α
edist_self_1 : ∀ (x : α), edist x x = 0
edist_comm_1 : ∀ (x y : α), edist x y = edist y x
edist_triangle_1 : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U' : UniformSpace α
hU' : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
h : Eq.{u_2 + 1} (α := EDist α) toEDist toEDist
⊢ { toEDist := ed, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
      toUniformSpace := U, uniformity_edist := hU : PseudoEMetricSpace α } =
    { toEDist := ed', edist_self := edist_self_1, edist_comm := edist_comm_1, edist_triangle := edist_triangle_1,
      toUniformSpace := U', uniformity_edist := hU' }
have e_toUniformSpace : U = U'
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist z x + edist z y
have rw : edist x y ≤ edist x z + edist z y
Tactic: rw [edist_comm z]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist y z
have rw : edist x y ≤ edist x z + edist z y
Tactic: rw [edist_comm y]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z
have a : edist x z ≤ edist y z
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
a : edist x z ≤ edist y z
⊢ edist x z = edist y z
have a₁ : edist y z ≤ edist x z
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist y z
have a : edist x z ≤ edist x y + edist y z
Tactic: rw [← zero_add (edist y z), ← h]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z
have h₁ : edist y x = 0
Tactic: rw [edist_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist x z
have a : edist y z ≤ edist y x + edist x z
Tactic: rw [← zero_add (edist x z), ← h]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist z x = edist z y
have rw : edist x z = edist y z
Tactic: rw [edist_comm z x, edist_comm z y]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z t : α
⊢ edist x t ≤ edist x y + edist y z + edist z t
have grw : edist x z + edist z t ≤ edist x y + edist y z + edist z t
Tactic: grw [edist_triangle _ z, edist_triangle]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z t : α
grw : edist x z + edist z t ≤ edist x y + edist y z + edist z t
⊢ edist x t ≤ edist x y + edist y z + edist z t
have grw₁ : edist x y + edist y z + edist z t ≤ edist x y + edist y z + edist z t
Tactic: grw [edist_triangle _ z, edist_triangle]