awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
mp : eVariationOn f s = 0 → ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
mpr : (∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0) → eVariationOn f s = 0
⊢ eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Tactic:
constructor
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
h : eVariationOn f s = 0
x : α
xs : x ∈ s
y : α
ys : y ∈ s
mp : edist (f x) (f y) ≤ eVariationOn f s
⊢ edist (f x) (f y) = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← h]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
h : eVariationOn f s = 0
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
edist_le f xs ys

Premises used: eVariationOn.edist_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
h : eVariationOn f s = 0
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
exact edist_le f xs ys

Premises used: eVariationOn.edist_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
mpr :
  ∀ (i : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    Eq (α := ℝ≥0∞) (∑ i_1 ∈ Finset.range i.1, edist (f ((↑i.2 : ℕ → α) (i_1 + 1))) (f ((↑i.2 : ℕ → α) i_1))) 0
⊢ Eq (α := ℝ≥0∞)
    (⨆ (p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
      ∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)))
    0

Tactic:
rw [ENNReal.iSup_eq_zero]

Premises used: ENNReal.iSup_eq_zero
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
⊢ Eq (α := ℝ≥0∞)
    (∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i)))
    0

Tactic:
Finset.sum_eq_zero fun i _ => h _ (us i.succ) _ (us i)

Premises used: Finset.sum_eq_zero, Prod.mk, Subtype.mk, And.intro, Subtype.val, Nat.succ, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
⊢ Eq (α := ℝ≥0∞)
    (∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i)))
    0

Tactic:
exact Finset.sum_eq_zero fun i _ => h _ (us i.succ) _ (us i)

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : (f '' s).Subsingleton
rw : ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
⊢ eVariationOn f s = 0

Tactic:
rw [eq_zero_iff]

Premises used: eVariationOn.eq_zero_iff
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : (f '' s).Subsingleton
x : α
xs : x ∈ s
y : α
ys : y ∈ s
rw : edist (f y) (f y) = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ edist (f x) (f y) = 0

Tactic:
rw [hf ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩, edist_self]

Premises used: PseudoEMetricSpace.edist_self, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hs : s.Subsingleton
⊢ eVariationOn f s = 0

Tactic:
constant_on (hs.image f)

Premises used: Set.Subsingleton.image, eVariationOn.constant_on
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun (i : ι) ↦ F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
⊢ ∃ (p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    v < ∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i))

Tactic:
lt_iSup_iff.mp hv

Premises used: Iff.mp, lt_iSup_iff
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun (i : ι) ↦ F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
obtain :
  ∀ (n : ℕ) (u : ℕ → α) (um : Monotone u) (us : ∀ (i : ℕ), u i ∈ s)
    (hlt :
      v <
        ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
          edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
            (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i))),
    ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

Tactic:
obtain ⟨⟨n, ⟨u, um, us⟩⟩, hlt⟩ :
    ∃ p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ i, u i ∈ s },
      v < ∑ i ∈ Finset.range p.1, edist (f ((p.2 : ℕ → α) (i + 1))) (f ((p.2 : ℕ → α) i)) :=
    lt_iSup_iff.mp hv

Premises used: Iff.mp, lt_iSup_iff
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun (i : ι) ↦ F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt :
  v <
    ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i))
a :
  ∀ i ∈ Finset.range n,
    Tendsto (fun (b : ι) ↦ edist (F b (u (i + 1))) (F b (u i))) p (𝓝 (edist (f (u (i + 1))) (f (u i))))
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))

Tactic:
apply tendsto_finsetSum

Premises used: tendsto_finsetSum
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun (i : ι) ↦ F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt :
  v <
    ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i))
⊢ ∀ i ∈ Finset.range n,
    Tendsto (fun (b : ι) ↦ edist (F b (u (i + 1))) (F b (u i))) p (𝓝 (edist (f (u (i + 1))) (f (u i))))

Tactic:
fun i _ => Tendsto.edist (Ffs (u i.succ) (us i.succ)) (Ffs (u i) (us i))

Premises used: Nat.succ, Filter.Tendsto.edist
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun (i : ι) ↦ F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt :
  v <
    ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i))
⊢ ∀ i ∈ Finset.range n,
    Tendsto (fun (b : ι) ↦ edist (F b (u (i + 1))) (F b (u i))) p (𝓝 (edist (f (u (i + 1))) (f (u i))))

Tactic:
exact fun i _ => Tendsto.edist (Ffs (u i.succ) (us i.succ)) (Ffs (u i) (us i))

Premises used: Filter.Tendsto.edist
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun (i : ι) ↦ F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt :
  v <
    ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i))
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))

Tactic:
have : Tendsto (fun j => ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
      (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))) := by
    apply tendsto_finsetSum
    exact fun i _ => Tendsto.edist (Ffs (u i.succ) (us i.succ)) (Ffs (u i) (us i))
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun (i : ι) ↦ F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt :
  v <
    ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i))
this :
  Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

Tactic:
(this.eventually_const_lt hlt).mono fun i h => h.trans_le (sum_le um us)

Premises used: Filter.Tendsto.eventually_const_lt, Filter.Eventually.mono, eVariationOn.sum_le, LT.lt.trans_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun (i : ι) ↦ F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt :
  v <
    ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i))
this :
  Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

Tactic:
exact (this.eventually_const_lt hlt).mono fun i h => h.trans_le (sum_le um us)

Premises used: Filter.Tendsto.eventually_const_lt, Filter.Eventually.mono, eVariationOn.sum_le, LT.lt.trans_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[singleton '' s] E
apply : ∀ x ∈ s, Tendsto (fun (i : α →ᵤ[singleton '' s] E) ↦ id i x) (𝓝 f) (𝓝 (f x))
⊢ SemicontinuousAt
    (fun (x1 : α →ᵤ[singleton '' s] E) (x2 : ℝ≥0∞) ↦ (fun (f : α →ᵤ[singleton '' s] E) ↦ eVariationOn f s) x1 > x2) f

Tactic:
apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E (s.image singleton)) id (𝓝 f) f s _

Premises used: eVariationOn.lowerSemicontinuous_aux
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[singleton '' s] E
⊢ ∀ x ∈ s, Tendsto (fun (i : α →ᵤ[singleton '' s] E) ↦ id i x) (𝓝 f) (𝓝 (f x))

Tactic:
simpa only [UniformOnFun.tendsto_iff_tendstoUniformlyOn, mem_image, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, tendstoUniformlyOn_singleton_iff_tendsto] using @tendsto_id _ (𝓝 f)

Premises used: Filter.tendsto_id, and_imp, UniformOnFun.tendsto_iff_tendstoUniformlyOn, Set.mem_image, forall_exists_index, tendstoUniformlyOn_singleton_iff_tendsto, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
apply : ∀ x ∈ s, Tendsto (fun (i : α →ᵤ[{s}] E) ↦ id i x) (𝓝 f) (𝓝 (f x))
⊢ SemicontinuousAt (fun (x1 : α →ᵤ[{s}] E) (x2 : ℝ≥0∞) ↦ (fun (f : α →ᵤ[{s}] E) ↦ eVariationOn f s) x1 > x2) f

Tactic:
apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E {s}) id (𝓝 f) f s _

Premises used: eVariationOn.lowerSemicontinuous_aux
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
⊢ Tendsto id (𝓝 f) (𝓝 f)

Tactic:
have := @tendsto_id _ (𝓝 f)
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this : Tendsto id (𝓝 f) (𝓝 f)
⊢ ∀ (s_1 : Set α),
    Membership.mem (γ := Set (Set α)) {s} s_1 →
      TendstoUniformlyOn (β := E) ((⇑(UniformOnFun.toFun {s}) : (a : α →ᵤ[{s}] E) → α → E) ∘ id)
        ((UniformOnFun.toFun {s} : (a : α →ᵤ[{s}] E) → α → E) f) (𝓝 f) s_1

Tactic:
rw [UniformOnFun.tendsto_iff_tendstoUniformlyOn] at this

Premises used: UniformOnFun.tendsto_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this :
  ∀ (s_1 : Set α),
    Membership.mem (γ := Set (Set α)) {s} s_1 →
      TendstoUniformlyOn (β := E) ((⇑(UniformOnFun.toFun {s}) : (a : α →ᵤ[{s}] E) → α → E) ∘ id)
        ((UniformOnFun.toFun {s} : (a : α →ᵤ[{s}] E) → α → E) f) (𝓝 f) s_1
simp_rw : ∀ x ∈ s, TendstoUniformlyOn id f (𝓝 f) {x}
⊢ ∀ x ∈ s, Tendsto (fun (i : α →ᵤ[{s}] E) ↦ id i x) (𝓝 f) (𝓝 (f x))

Tactic:
simp_rw [← tendstoUniformlyOn_singleton_iff_tendsto]

Premises used: tendstoUniformlyOn_singleton_iff_tendsto
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this :
  ∀ (s_1 : Set α),
    Membership.mem (γ := Set (Set α)) {s} s_1 →
      TendstoUniformlyOn (β := E) ((⇑(UniformOnFun.toFun {s}) : (a : α →ᵤ[{s}] E) → α → E) ∘ id)
        ((UniformOnFun.toFun {s} : (a : α →ᵤ[{s}] E) → α → E) f) (𝓝 f) s_1
⊢ ∀ x ∈ s, TendstoUniformlyOn id f (𝓝 f) {x}

Tactic:
fun x xs => (this s rfl).mono (singleton_subset_iff.mpr xs)

Premises used: Iff.mpr, Set.singleton_subset_iff, TendstoUniformlyOn.mono, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this :
  ∀ (s_1 : Set α),
    Membership.mem (γ := Set (Set α)) {s} s_1 →
      TendstoUniformlyOn (β := E) ((⇑(UniformOnFun.toFun {s}) : (a : α →ᵤ[{s}] E) → α → E) ∘ id)
        ((UniformOnFun.toFun {s} : (a : α →ᵤ[{s}] E) → α → E) f) (𝓝 f) s_1
⊢ ∀ x ∈ s, TendstoUniformlyOn id f (𝓝 f) {x}

Tactic:
exact fun x xs => (this s rfl).mono (singleton_subset_iff.mpr xs)

Premises used: Iff.mpr, Set.singleton_subset_iff, TendstoUniformlyOn.mono, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_3
inst_1 : PseudoMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
rw : edist (f x) (f y) ≤ eVariationOn f s
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal

Tactic:
rw [← ENNReal.ofReal_le_ofReal_iff ENNReal.toReal_nonneg, ENNReal.ofReal_toReal h, ← edist_dist]

Premises used: ENNReal.ofReal_le_ofReal_iff, ENNReal.ofReal_toReal, ENNReal.toReal_nonneg, edist_dist
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_3
inst_1 : PseudoMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
edist_le f hx hy

Premises used: eVariationOn.edist_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_3
inst_1 : PseudoMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
exact edist_le f hx hy

Premises used: eVariationOn.edist_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
apply : |f x - f y| ≤ (eVariationOn f s).toReal
⊢ f x - f y ≤ (eVariationOn f s).toReal

Tactic:
apply (le_abs_self _).trans

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal

Tactic:
h.dist_le hx hy

Premises used: BoundedVariationOn.dist_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal

Tactic:
exact h.dist_le hx hy

Premises used: BoundedVariationOn.dist_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
inl :
  ∀ (h : u n ≤ x),
    ∃ (v : ℕ → α) (m : ℕ),
      Monotone v ∧
        (∀ (i : ℕ), v i ∈ s) ∧
          x ∈ v '' Iio m ∧
            LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
              (∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)))
inr :
  ∀ (h : x < u n),
    ∃ (v : ℕ → α) (m : ℕ),
      Monotone v ∧
        (∀ (i : ℕ), v i ∈ s) ∧
          x ∈ v '' Iio m ∧
            LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
              (∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)))
⊢ ∃ (v : ℕ → α) (m : ℕ),
    Monotone v ∧
      (∀ (i : ℕ), v i ∈ s) ∧
        x ∈ v '' Iio m ∧
          LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
            (∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)))

Tactic:
rcases le_or_gt (u n) x with (h | h)

Premises used: le_or_gt
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else x
⊢ Monotone v

Tactic:
grind [Monotone]

Premises used: Monotone
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else x
⊢ ∀ (i : ℕ), v i ∈ s

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else x
⊢ n + 1 ∈ Iio (n + 2) ∧ v (n + 1) = x

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else x
inl :
  LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ j ∈ Finset.range (n + 2), edist (f (v (j + 1))) (f (v j)))
⊢ ∃ (v : ℕ → α) (m : ℕ),
    Monotone v ∧
      (∀ (i : ℕ), v i ∈ s) ∧
        x ∈ v '' Iio m ∧
          LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
            (∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)))

Tactic:
refine ⟨v, n + 2, by grind [Monotone], by grind, (mem_image _ _ _).2 ⟨n + 1, by grind⟩, ?_⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else x
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)))

Tactic:
grind [Finset.sum_congr]

Premises used: Finset.sum_congr
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else x
h₁ : n ≤ n + 2
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)))
    (∑ j ∈ Finset.range (n + 2), edist (f (v (j + 1))) (f (v j)))

Tactic:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else x
⊢ n ≤ n + 2

Tactic:
apply Nat.le_add_right

Premises used: Nat.le_add_right
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else x
i :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)))
i₁ :
  LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)))
    (∑ j ∈ Finset.range (n + 2), edist (f (v (j + 1))) (f (v j)))
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ j ∈ Finset.range (n + 2), edist (f (v (j + 1))) (f (v j)))

Tactic:
calc
      (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
          ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by grind [Finset.sum_congr]
      _ ≤ ∑ j ∈ Finset.range (n + 2), edist (f (v (j + 1))) (f (v j)) := by
        gcongr
        apply Nat.le_add_right

Premises used: Finset.range, HAdd.hAdd, EDist.edist, OfNat.ofNat, Finset.sum