awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Set α
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }
hp :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
    (∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
      edist
        (f
          ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
            (i + 1)))
        (f ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α) i)))
⊢ LE.le (α := ℝ≥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)))
    (⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i + 1)))
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α) i)))
have a : LE.le (α := ℝ≥0∞)
  (∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
    edist
      (f
        ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
          (i + 1)))
      (f ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α) i)))
  (⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
    ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
      edist
        (f
          ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
            (i + 1)))
        (f ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α) i)))
Tactic: rw [hp]
-- 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
s : Set α
⊢ ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i + 1)))
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              i)) ≤
    eVariationOn f s
have a : ∀ (i : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
  ∑ i_1 ∈ Finset.range (i.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
      edist
        (f
          ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
            (i_1 + 1)))
        (f
          ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
            i_1)) ≤
    eVariationOn f 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 : α → E
s t : Set α
hst : t ⊆ s
⊢ eVariationOn f t ≤ eVariationOn f s
have apply : ∀ (i : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }),
  ∑ i_1 ∈ Finset.range i.1, edist (f ((↑i.2 : ℕ → α) (i_1 + 1))) (f ((↑i.2 : ℕ → α) i_1)) ≤ eVariationOn f 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 : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s
have inr : ∀ (this : ∀ {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : y ≤ x), edist (f x) (f y) ≤ eVariationOn f s) (hxy : ¬y ≤ x),
  edist (f x) (f y) ≤ eVariationOn f s
Tactic: wlog hxy : y ≤ x generalizing x 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
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
inr :
  ∀ (this : ∀ {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : y ≤ x), edist (f x) (f y) ≤ eVariationOn f s) (hxy : ¬y ≤ x),
    edist (f x) (f y) ≤ eVariationOn f s
⊢ edist (f x) (f y) ≤ eVariationOn f s
have wlog : ∀ {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : y ≤ x), edist (f x) (f y) ≤ eVariationOn f s
Tactic: wlog hxy : y ≤ x generalizing x y
Cleared hypotheses: x, y, 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
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : y ≤ x), edist (f x) (f y) ≤ eVariationOn f s
hxy : ¬y ≤ x
⊢ edist (f x) (f y) ≤ eVariationOn f s
have inr : edist (f y) (f x) ≤ eVariationOn f s
Tactic: rw [edist_comm]
-- 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
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
u : ℕ → α := fun (n : ℕ) ↦ if n = 0 then y else x
⊢ edist (f x) (f y) ≤ eVariationOn f s
have hu : Monotone u
Tactic: have hu : Monotone u := monotone_nat_of_le_succ fun
  | 0 => hxy
  | (_ + 1) => le_rfl
-- 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
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
u : ℕ → α := fun (n : ℕ) ↦ if n = 0 then y else x
hu : Monotone u
⊢ edist (f x) (f y) ≤ eVariationOn f s
have us : ∀ (i : ℕ), u i ∈ s
Tactic: have us : ∀ i, u i ∈ s := fun
  | 0 => hy
  | (_ + 1) => 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
s : Set α
⊢ eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
have mp : eVariationOn f s = 0 → ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
Tactic: constructor
-- 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
s : Set α
mp : eVariationOn f s = 0 → ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
⊢ eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
have mpr : (∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0) → eVariationOn f s = 0
Tactic: constructor
-- 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
s : Set α
h : eVariationOn f s = 0
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) = 0
have mp : edist (f x) (f y) ≤ eVariationOn f s
Tactic: rw [← nonpos_iff_eq_zero, ← 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
f : α → E
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 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
have 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
Tactic: rw [ENNReal.iSup_eq_zero]
-- 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
s : Set α
hf : (f '' s).Subsingleton
⊢ eVariationOn f s = 0
have rw : ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
Tactic: rw [eq_zero_iff]
-- 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
s : Set α
hf : (f '' s).Subsingleton
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) = 0
have rw : edist (f y) (f y) = 0
Tactic: rw [hf ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩, edist_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
s : Set α
hf : (f '' s).Subsingleton
x : α
xs : x ∈ s
y : α
ys : y ∈ s
rw : edist (f y) (f y) = 0
⊢ edist (f x) (f y) = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [hf ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩, edist_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
ι : 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 : ι) in p, v < eVariationOn (F n) s
have 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 sorry).1,
        edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u sorry).2 : ℕ → α) (i + 1)))
          (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u sorry).2 : ℕ → α) i))),
  ∀ᶠ (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
-- 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
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))))
have 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))))
Tactic: apply tendsto_finsetSum
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
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))
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s
have 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))))
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))
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[singleton '' s] E
⊢ SemicontinuousAt
    (fun (x1 : α →ᵤ[singleton '' s] E) (x2 : ℝ≥0∞) ↦ (fun (f : α →ᵤ[singleton '' s] E) ↦ eVariationOn f s) x1 > x2) f
have apply : ∀ x ∈ s, Tendsto (fun (i : α →ᵤ[singleton '' s] E) ↦ id i x) (𝓝 f) (𝓝 (f x))
Tactic: apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E (s.image singleton)) id (𝓝 f) f s _
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
⊢ SemicontinuousAt (fun (x1 : α →ᵤ[{s}] E) (x2 : ℝ≥0∞) ↦ (fun (f : α →ᵤ[{s}] E) ↦ eVariationOn f s) x1 > x2) f
have apply : ∀ x ∈ s, Tendsto (fun (i : α →ᵤ[{s}] E) ↦ id i x) (𝓝 f) (𝓝 (f x))
Tactic: apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E {s}) id (𝓝 f) f s _
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
⊢ ∀ x ∈ s, Tendsto (fun (i : α →ᵤ[{s}] E) ↦ id i x) (𝓝 f) (𝓝 (f x))
have this : Tendsto id (𝓝 f) (𝓝 f)
Tactic: have := @tendsto_id _ (𝓝 f)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this : Tendsto id (𝓝 f) (𝓝 f)
⊢ ∀ x ∈ s, Tendsto (fun (i : α →ᵤ[{s}] E) ↦ id i x) (𝓝 f) (𝓝 (f x))
have 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
Tactic: rw [UniformOnFun.tendsto_iff_tendstoUniformlyOn] at this
Cleared hypotheses: 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
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, Tendsto (fun (i : α →ᵤ[{s}] E) ↦ id i x) (𝓝 f) (𝓝 (f x))
have simp_rw : ∀ x ∈ s, TendstoUniformlyOn id f (𝓝 f) {x}
Tactic: simp_rw [← tendstoUniformlyOn_singleton_iff_tendsto]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal
have rw : edist (f x) (f y) ≤ eVariationOn f s
Tactic: rw [← ENNReal.ofReal_le_ofReal_iff ENNReal.toReal_nonneg, ENNReal.ofReal_toReal h, ← edist_dist]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ f x - f y ≤ (eVariationOn f s).toReal
have apply : |f x - f y| ≤ (eVariationOn f s).toReal
Tactic: apply (le_abs_self _).trans
-- 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
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
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)))
have 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)))
Tactic: rcases le_or_gt (u n) x 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
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)))
⊢ ∃ (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)))
have 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)))
Tactic: rcases le_or_gt (u n) x 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
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
⊢ ∃ (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)))
have 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)))
Tactic: refine ⟨v, n + 2, by grind [Monotone], by grind, (mem_image _ _ _).2 ⟨n + 1, by grind⟩, ?_⟩
-- 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
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
⊢ 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)))
have h₁ : n ≤ n + 2
Tactic: gcongr
-- 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
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
⊢ 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)))
have 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)))
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
-- 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
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)))
⊢ 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)))
have 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)))
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
-- 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
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
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)))
have exists_N : ∃ N ≤ n, x < u N
Tactic: have exists_N : ∃ N, N ≤ n ∧ x < u N := ⟨n, le_rfl, h⟩
-- 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
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_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)))
have hN : N ≤ n ∧ x < u N
Tactic: have hN : N ≤ n ∧ x < u N := Nat.find_spec exists_N
-- 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
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
⊢ Monotone w
have apply : ∀ (i : ℕ), w i ≤ w (i + 1)
Tactic: apply monotone_nat_of_le_succ fun i => ?_
-- 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
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
⊢ w i ≤ w (i + 1)
have inl : ∀ (hi : i + 1 < N), w i ≤ w (i + 1)
Tactic: rcases lt_trichotomy (i + 1) N with (hi | hi | hi)
-- 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
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
inl : ∀ (hi : i + 1 < N), w i ≤ w (i + 1)
⊢ w i ≤ w (i + 1)
have inr : ∀ (hi : i + 1 = N), w i ≤ w (i + 1)
Tactic: rcases lt_trichotomy (i + 1) N with (hi | hi | hi)