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
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this : u (n + 1) ≤ a
hn : u (n + 1) = a
⊢ Tendsto (fun (x : α) ↦ edist (f x) (f (u n))) (𝓝[s ∩ Iio a] a) (𝓝 (edist (f (u (n + 1))) (f (u n))))
have apply : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 (f (u (n + 1))))
Tactic: apply Tendsto.edist _ tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this : u (n + 1) ≤ a
hn : u (n + 1) = a
⊢ Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 (f (u (n + 1))))
have rw : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 (f a))
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this : u (n + 1) ≤ a
hn : u (n + 1) = a
⊢ Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 (f a))
have apply : 𝓝[s ∩ Iio a] a ≤ 𝓝[s ∩ Iic a] a
Tactic: apply h'.tendsto.mono_left
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this : u (n + 1) ≤ a
hn : u (n + 1) = a
⊢ edist (f (u (n + 1))) (f (u n)) + ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Iio a)
have this₁ : Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
  (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
Tactic: have : Tendsto (fun b ↦ edist (f b) (f (u n))
        + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
      (𝓝 (edist (f (u (n + 1))) (f (u n))
        + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))) := by
      apply Tendsto.add_const
      apply Tendsto.edist _ tendsto_const_nhds
      rw [hn]
      apply h'.tendsto.mono_left
      exact nhdsWithin_mono _ (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
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this_1 : u (n + 1) ≤ a
hn : u (n + 1) = a
this :
  Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
    (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
⊢ edist (f (u (n + 1))) (f (u n)) + ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Iio a)
have h₁ : ∀ᶠ (c : α) in 𝓝[s ∩ Iio a] a,
  edist (f c) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a)
Tactic: apply le_of_tendsto 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
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this_1 : u (n + 1) ≤ a
hn : u (n + 1) = a
this :
  Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
    (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
⊢ s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a
have rw : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this_1 : u (n + 1) ≤ a
hn : u (n + 1) = a
this :
  Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
    (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
⊢ s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
have apply : Ioo (u n) a ∈ 𝓝[<] a
Tactic: apply inter_mem_nhdsWithin_inter self_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this_1 : u (n + 1) ≤ a
hn : u (n + 1) = a
this :
  Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
    (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Iio a] a,
    edist (f c) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a)
have this₁ : s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a
Tactic: have : s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a := by
      rw [hn]
      apply inter_mem_nhdsWithin_inter self_mem_nhdsWithin
      exact Ioo_mem_nhdsLT (by grind [StrictMonoOn])
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this_1 : u (n + 1) ≤ a
hn : u (n + 1) = a
this_2 :
  Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
    (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
this : s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Iio a] a,
    edist (f c) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a)
have h₁ : ∀ (b : α) (hb : b ∈ s ∩ Ioo (u n) (u (n + 1))),
  edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a)
Tactic: filter_upwards [this] with b hb
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this_1 : u (n + 1) ≤ a
hn : u (n + 1) = a
this_2 :
  Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
    (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
this : s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a
b : α
hb : b ∈ s ∩ Ioo (u n) (u (n + 1))
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else b
⊢ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    ∑ i ∈ Finset.range (n + 1), edist (f (v (i + 1))) (f (v i))
have simp : edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
  edist (f (v (n + 1))) (f (v n)) + ∑ x ∈ Finset.range n, edist (f (v (x + 1))) (f (v x))
Tactic: simp only [Finset.range_add_one, Finset.mem_range, lt_self_iff_false, not_false_eq_true,
        Finset.sum_insert]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this_1 : u (n + 1) ≤ a
hn : u (n + 1) = a
this_2 :
  Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
    (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
this : s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a
b : α
hb : b ∈ s ∩ Ioo (u n) (u (n + 1))
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else b
⊢ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    edist (f (v (n + 1))) (f (v n)) + ∑ x ∈ Finset.range n, edist (f (v (x + 1))) (f (v x))
have e_a : edist (f b) (f (u n)) = edist (f (v (n + 1))) (f (v n))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this_1 : u (n + 1) ≤ a
hn : u (n + 1) = a
this_2 :
  Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
    (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
this : s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a
b : α
hb : b ∈ s ∩ Ioo (u n) (u (n + 1))
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else b
e_a : edist (f b) (f (u n)) = edist (f (v (n + 1))) (f (v n))
⊢ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    edist (f (v (n + 1))) (f (v n)) + ∑ x ∈ Finset.range n, edist (f (v (x + 1))) (f (v x))
have e_a₁ : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
  (∑ x ∈ Finset.range n, edist (f (v (x + 1))) (f (v x)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this_1 : u (n + 1) ≤ a
hn : u (n + 1) = a
this_2 :
  Tendsto (fun (b : α) ↦ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) (𝓝[s ∩ Iio a] a)
    (𝓝 (edist (f (u (n + 1))) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
this : s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a
b : α
hb : b ∈ s ∩ Ioo (u n) (u (n + 1))
v : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else b
⊢ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a)
have calc : edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
  ∑ i ∈ Finset.range (n + 1), edist (f (v (i + 1))) (f (v i))
Tactic: calc edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))
    _ = ∑ i ∈ Finset.range (n + 1), edist (f (v (i + 1))) (f (v i)) := by
      simp only [Finset.range_add_one, Finset.mem_range, lt_self_iff_false, not_false_eq_true,
        Finset.sum_insert]
      congr 1 <;> grind [Finset.sum_congr]
    _ ≤ eVariationOn f (s ∩ Iio a) :=
      sum_le_of_monotoneOn_Iic (by grind [MonotoneOn, StrictMonoOn]) (by grind [StrictMonoOn])
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Ioi a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Ici a) a
⊢ eVariationOn f (s ∩ Ioi a) = eVariationOn f (s ∩ Ici a)
have rw : eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Ioi a)) =
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Ici a))
Tactic: rw [← comp_ofDual f, ← comp_ofDual f]
-- 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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
⊢ ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)
have obtain : ∀ (n : ℕ) (u : ℕ → α) (hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))) (u_mono : Monotone u)
  (u_mem : ∀ (i : ℕ), u i ∈ s), ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)
Tactic: obtain ⟨n, u, ⟨u_mono, u_mem⟩, hu⟩ : ∃ n u, (Monotone u ∧ ∀ (i : ℕ), u i ∈ s) ∧
      ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) := by
    simpa [eVariationOn, lt_iSup_iff] using 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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ε < eVariationOn f (s ∩ Icc (u 0) (u n))
have apply : ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Icc (u 0) (u n))
Tactic: apply hu.trans_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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : ∀ ⦃a b : ℕ⦄, a ≤ b → u a ≤ u b
u_mem : ∀ (i : ℕ), u i ∈ s
v : (i : ℕ) → α := fun (i : ℕ) ↦ min (u i) (u n)
⊢ ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Icc (u 0) (u n))
have calc : Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
  (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)))
Tactic: calc ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
    _ = ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by grind [Finset.sum_congr]
    _ ≤ eVariationOn f (s ∩ Icc (u 0) (u n)) :=
      sum_le_of_monotoneOn_Iic (by grind [MonotoneOn]) (by grind)
-- 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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)
have A : ε < eVariationOn f (s ∩ Icc (u 0) (u n))
Tactic: have A : ε < eVariationOn f (s ∩ Icc (u 0) (u n)) := by
    apply hu.trans_le
    simp only [Monotone] at u_mono
    let v (i : ℕ) := min (u i) (u n)
    calc ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
    _ = ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by grind [Finset.sum_congr]
    _ ≤ eVariationOn f (s ∩ Icc (u 0) (u n)) :=
      sum_le_of_monotoneOn_Iic (by grind [MonotoneOn]) (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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
A : ε < eVariationOn f (s ∩ Icc (u 0) (u n))
⊢ ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)
have refine : u 0 < u n
Tactic: refine ⟨u 0, u_mem _, u n, u_mem _, ?_, A⟩
-- 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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
A : ε < eVariationOn f (s ∩ Icc (u 0) (u n))
⊢ u 0 < u n
have by_contra! : ∀ (this : u n ≤ u 0), False
Tactic: by_contra!
-- 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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
A : ε < eVariationOn f (s ∩ Icc (u 0) (u n))
this : u n ≤ u 0
a : α
ha : a ∈ s ∩ Icc (u 0) (u n)
b : α
hb : b ∈ s ∩ Icc (u 0) (u n)
⊢ a = b
have ha₁ : a ∈ s ∧ u 0 ≤ a ∧ a ≤ u n
Tactic: simp only [mem_inter_iff, mem_Icc] at ha hb
Cleared hypotheses: ha, hb
-- 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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
A : ε < eVariationOn f (s ∩ Icc (u 0) (u n))
this : u n ≤ u 0
a : α
ha : a ∈ s ∩ Icc (u 0) (u n)
b : α
hb : b ∈ s ∩ Icc (u 0) (u n)
ha₁ : a ∈ s ∧ u 0 ≤ a ∧ a ≤ u n
⊢ a = b
have hb₁ : b ∈ s ∧ u 0 ≤ b ∧ b ≤ u n
Tactic: simp only [mem_inter_iff, mem_Icc] at ha hb
Cleared hypotheses: ha, hb
-- 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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
A : ε < eVariationOn f (s ∩ Icc (u 0) (u n))
this : u n ≤ u 0
a b : α
ha : a ∈ s ∧ u 0 ≤ a ∧ a ≤ u n
hb : b ∈ s ∧ u 0 ≤ b ∧ b ≤ u n
⊢ a = b
have order : ¬a = b → False
Tactic: order
-- 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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
A : ε < eVariationOn f (s ∩ Icc (u 0) (u n))
this : u n ≤ u 0
a b : α
ha : a ∈ s ∧ u 0 ≤ a ∧ a ≤ u n
hb : b ∈ s ∧ u 0 ≤ b ∧ b ≤ u n
order order₁ order₂ order₃ : ¬a = b → False
⊢ a = b
have order₄ : a ≠ b → False
Tactic: order
-- 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
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
n : ℕ
u : ℕ → α
hu : ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
A : ε < eVariationOn f (s ∩ Icc (u 0) (u n))
this : u n ≤ u 0
⊢ False
have this₁ : (s ∩ Icc (u 0) (u n)).Subsingleton
Tactic: have : Set.Subsingleton (s ∩ Icc (u 0) (u n)) := by
    intro a ha b hb
    simp only [mem_inter_iff, mem_Icc] at ha hb
    order
-- 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 : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
have inl : ∀ (hf : BoundedVariationOn f ∅) (hL : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∅ ∩ Ici y ∈ L),
  Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (∅ ∩ Ici y)) L (𝓝 0)
Tactic: rcases eq_empty_or_nonempty s with rfl | ⟨x₀, hx₀⟩
Cleared hypotheses: s, hf, hL
-- 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 : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
inl :
  ∀ (hf : BoundedVariationOn f ∅) (hL : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∅ ∩ Ici y ∈ L),
    Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (∅ ∩ Ici y)) L (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
have inr : ∀ (x₀ : α) (hx₀ : x₀ ∈ s), Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
Tactic: rcases eq_empty_or_nonempty s with rfl | ⟨x₀, 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 α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
have apply : ∀ (ε : ℝ≥0∞) (εpos : ε > 0), ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε
Tactic: apply tendsto_order.2 ⟨by simp, fun ε εpos ↦ ?_⟩
-- 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 : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε
have obtain : ∀ (δ : ℝ≥0∞) (δpos : 0 < δ) (hδ : δ < ε), ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε
Tactic: obtain ⟨δ, δpos, hδ⟩ : ∃ δ, δ ∈ Ioo 0 ε := exists_between εpos
-- 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 : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
⊢ ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε
have by_contra! : ∀ (H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)), False
Tactic: by_contra! 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 α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)
y : α
hy : y ∈ s
⊢ ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')
have obtain : ∀ (y' : α) (hy' : ε ≤ eVariationOn f (s ∩ Ici y')) (y'_mem : y' ∈ s ∩ Ici y),
  ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')
Tactic: obtain ⟨y', hy', y'_mem⟩ : ∃ y', ε ≤ eVariationOn f (s ∩ Ici y') ∧ y' ∈ s ∩ Ici y :=
      (H.and_eventually (hL y hy)).exists