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 α
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' : α
hy' : ε ≤ eVariationOn f (s ∩ Ici y')
y'_mem : y' ∈ s ∩ Ici y
⊢ ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')
have obtain : ∀ (a : α) (ha : a ∈ s ∩ Ici y') (b : α) (hb : b ∈ s ∩ Ici y') (hab : a < b)
  (h : δ < eVariationOn f (s ∩ Ici y' ∩ Icc a b)), ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')
Tactic: obtain ⟨a, ha, b, hb, hab, h⟩ : ∃ a ∈ s ∩ Ici y', ∃ b ∈ s ∩ Ici y', a < b ∧
      δ < eVariationOn f ((s ∩ Ici y') ∩ Icc a b) :=
        exists_lt_eVariationOn_inter_Icc (hδ.trans_le 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 α
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' : α
hy' : ε ≤ eVariationOn f (s ∩ Ici y')
y'_mem : y' ∈ s ∩ Ici y
a : α
ha : a ∈ s ∩ Ici y'
b : α
hb : b ∈ s ∩ Ici y'
hab : a < b
h : δ < eVariationOn f (s ∩ Ici y' ∩ Icc a b)
⊢ ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')
have refine : δ ≤ eVariationOn f (s ∩ Icc y b)
Tactic: refine ⟨b, ⟨hb.1, le_trans y'_mem.2 hb.2⟩, ?_⟩
-- 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 α
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' : α
hy' : ε ≤ eVariationOn f (s ∩ Ici y')
y'_mem : y' ∈ s ∩ Ici y
a : α
ha : a ∈ s ∩ Ici y'
b : α
hb : b ∈ s ∩ Ici y'
hab : a < b
h : δ < eVariationOn f (s ∩ Ici y' ∩ Icc a b)
⊢ δ ≤ eVariationOn f (s ∩ Icc y b)
have this : Ici y' ∩ Icc a b = Icc a b
Tactic: have : Ici y' ∩ Icc a b = Icc a b := 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
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' : α
hy' : ε ≤ eVariationOn f (s ∩ Ici y')
y'_mem : y' ∈ s ∩ Ici y
a : α
ha : a ∈ s ∩ Ici y'
b : α
hb : b ∈ s ∩ Ici y'
hab : a < b
h : δ < eVariationOn f (s ∩ Ici y' ∩ Icc a b)
this : Ici y' ∩ Icc a b = Icc a b
⊢ δ ≤ eVariationOn f (s ∩ Icc y b)
have h₁ : δ < eVariationOn f (s ∩ Icc a b)
Tactic: rw [inter_assoc, this] at h
Cleared hypotheses: h, this
-- 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 α
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)
⊢ False
have B : ∀ (y : α) (hy : y ∈ s), ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')
Tactic: have B (y) (hy : y ∈ s) : ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y') := by
    obtain ⟨y', hy', y'_mem⟩ : ∃ y', ε ≤ eVariationOn f (s ∩ Ici y') ∧ y' ∈ s ∩ Ici y :=
      (H.and_eventually (hL y hy)).exists
    obtain ⟨a, ha, b, hb, hab, h⟩ : ∃ a ∈ s ∩ Ici y', ∃ b ∈ s ∩ Ici y', a < b ∧
      δ < eVariationOn f ((s ∩ Ici y') ∩ Icc a b) :=
        exists_lt_eVariationOn_inter_Icc (hδ.trans_le hy')
    refine ⟨b, ⟨hb.1, le_trans y'_mem.2 hb.2⟩, ?_⟩
    have : Ici y' ∩ Icc a b = Icc a b := by grind
    rw [inter_assoc, this] at h
    exact h.le.trans (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
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)
B : ∀ (y : α) (hy : y ∈ s), ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')
⊢ False
have choose! : ∀ (y : (y : α) → α) (y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1)
  (le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))), False
Tactic: choose! y y_mem le_y using B
Cleared hypotheses: B
-- 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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
n : ℕ
ih : v n ∈ s
⊢ v (n + 1) ∈ s
have succ : y (y^[n] x₀) ∈ s
Tactic: simp only [Function.iterate_succ', Function.comp_apply, v]
-- 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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
n : ℕ
⊢ v n ∈ s
have zero : v 0 ∈ s
Tactic: induction n with
    | zero => simpa [v] using hx₀
    | succ n ih =>
      simp only [Function.iterate_succ', Function.comp_apply, v]
      exact (y_mem _ ih).1
Cleared hypotheses: 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 α
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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
n : ℕ
zero : v 0 ∈ s
⊢ v n ∈ s
have succ : ∀ (n : ℕ) (ih : v n ∈ s), v (n + 1) ∈ s
Tactic: induction n with
    | zero => simpa [v] using hx₀
    | succ n ih =>
      simp only [Function.iterate_succ', Function.comp_apply, v]
      exact (y_mem _ ih).1
Cleared hypotheses: n
-- 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 α
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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
⊢ False
have I : ∀ (n : ℕ), v n ∈ s
Tactic: have I n : v n ∈ s := by
    induction n with
    | zero => simpa [v] using hx₀
    | succ n ih =>
      simp only [Function.iterate_succ', Function.comp_apply, v]
      exact (y_mem _ ih).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
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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
n : ℕ
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, δ) (∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (v i) (v (i + 1))))
have h : ∀ (i : ℕ) (hi : i ∈ Finset.range n), δ ≤ eVariationOn f (s ∩ Icc (v i) (v (i + 1)))
Tactic: gcongr with i 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 α
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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
n i : ℕ
hi : i ∈ Finset.range n
⊢ δ ≤ eVariationOn f (s ∩ Icc (v i) (v (i + 1)))
have h : δ ≤ eVariationOn f (s ∩ Icc (y^[i] x₀) (y (y^[i] x₀)))
Tactic: simp only [Function.iterate_succ', Function.comp_apply, v]
-- 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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
n : ℕ
⊢ ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (v i) (v (i + 1))) = eVariationOn f (s ∩ Icc (v 0) (v n))
have hE : Monotone v
Tactic: apply eVariationOn.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 : α → 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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
n : ℕ
hE : Monotone v
⊢ ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (v i) (v (i + 1))) = eVariationOn f (s ∩ Icc (v 0) (v n))
have hn : ∀ (i : ℕ), 0 < i → i < n → v i ∈ s
Tactic: apply eVariationOn.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 : α → 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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
n : ℕ
⊢ Monotone v
have apply : ∀ (n : ℕ), v n ≤ v (n + 1)
Tactic: apply monotone_nat_of_le_succ (fun 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 α
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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
n_1 n : ℕ
⊢ v n ≤ v (n + 1)
have simp : y^[n] x₀ ≤ y (y^[n] x₀)
Tactic: simp only [Function.iterate_succ', Function.comp_apply, v]
-- 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 α
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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
⊢ False
have J : ∀ (n : ℕ), (↑n : ℝ≥0∞) * δ ≤ eVariationOn f s
Tactic: have J (n : ℕ) : n * δ ≤ eVariationOn f s := calc
    n * δ
    _ = ∑ i ∈ Finset.range n, δ := by simp
    _ ≤ ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (v i) (v (i + 1))) := by
      gcongr with i hi
      simp only [Function.iterate_succ', Function.comp_apply, v]
      grind
    _ = eVariationOn f (s ∩ Icc (v 0) (v n)) := by
      apply eVariationOn.sum
      · apply monotone_nat_of_le_succ (fun n ↦ ?_)
        simp only [Function.iterate_succ', Function.comp_apply, v]
        exact (y_mem _ (I n)).2
      · grind
    _ ≤ eVariationOn f s := mono _ inter_subset_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
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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
J : ∀ (n : ℕ), (↑n : ℝ≥0∞) * δ ≤ eVariationOn f s
⊢ False
have this : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * δ) atTop (𝓝 (∞ * δ))
Tactic: have : Tendsto (fun (n : ℕ) ↦ n * δ) atTop (𝓝 (∞ * δ)) :=
    ENNReal.Tendsto.mul_const ENNReal.tendsto_nat_nhds_top (by simp)
-- 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 α
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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
J : ∀ (n : ℕ), (↑n : ℝ≥0∞) * δ ≤ eVariationOn f s
this : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * δ) atTop (𝓝 (∞ * δ))
⊢ False
have this₁ : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * δ) atTop (𝓝 ∞)
Tactic: rw [ENNReal.top_mul δpos.ne'] at this
Cleared hypotheses: this
-- 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 α
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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
J : ∀ (n : ℕ), (↑n : ℝ≥0∞) * δ ≤ eVariationOn f s
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * δ) atTop (𝓝 ∞)
⊢ False
have this₁ : ∞ ≤ eVariationOn f s
Tactic: have : ∞ ≤ eVariationOn f s := le_of_tendsto this (Eventually.of_forall J)
-- 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 : eVariationOn 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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
J : ∀ (n : ℕ), (↑n : ℝ≥0∞) * δ ≤ eVariationOn f s
this_1 : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * δ) atTop (𝓝 ∞)
this : ∞ ≤ eVariationOn f s
⊢ False
have order : ¬False → 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
s : Set α
hf : eVariationOn 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 : (y : α) → α
y_mem : ∀ (y_1 : α) (hy : y_1 ∈ s), y y_1 ∈ s ∩ Ici y_1
le_y : ∀ (y_1 : α) (hy : y_1 ∈ s), δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : (n : ℕ) → α := fun (n : ℕ) ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
J : ∀ (n : ℕ), (↑n : ℝ≥0∞) * δ ≤ eVariationOn f s
this_1 : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * δ) atTop (𝓝 ∞)
this : ∞ ≤ eVariationOn f s
order order₁ order₂ order₃ : ¬False → False
⊢ False
have order₄ : True → 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
inst_2 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
hs : s.Nonempty
⊢ ∃ (l : E), Tendsto f L (𝓝 l)
have rcases : ∀ (x₀ : α) (hx₀ : x₀ ∈ s), ∃ (l : E), Tendsto f L (𝓝 l)
Tactic: rcases hs with ⟨x₀, hx₀⟩
Cleared hypotheses: hs
-- 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 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
⊢ ∃ (l : E), Tendsto f L (𝓝 l)
have inl : ∀ (h : L = ⊥), ∃ (l : E), Tendsto f L (𝓝 l)
Tactic: rcases Filter.eq_or_neBot L 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
inst_2 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
inl : ∀ (h : L = ⊥), ∃ (l : E), Tendsto f L (𝓝 l)
⊢ ∃ (l : E), Tendsto f L (𝓝 l)
have inr : ∀ (h : L.NeBot), ∃ (l : E), Tendsto f L (𝓝 l)
Tactic: rcases Filter.eq_or_neBot L 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
inst_2 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L = ⊥
⊢ ∃ (l : E), Tendsto f L (𝓝 l)
have inl : Nonempty E
Tactic: simp only [h, tendsto_bot, exists_const_iff, and_true]
-- 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 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
⊢ ∃ (l : E), Tendsto f L (𝓝 l)
have inr : Cauchy (map f L)
Tactic: apply CompleteSpace.complete
-- 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 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
⊢ Cauchy (map f L)
have apply : ∀ (ε : ℝ≥0∞) (εpos : ε > 0), ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
Tactic: apply EMetric.cauchy_iff.2 ⟨by simp [neBot_iff.mp h], fun ε εpos ↦ ?_⟩
-- 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 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε
have W : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
Tactic: have W := hf.tendsto_eVariationOn_Ici_zero_of_filter L 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
inst_2 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
W : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
⊢ ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε
have rcases : ∀ (y : α) (hy : eVariationOn f (s ∩ Ici y) < ε) (h'y : (s ∩ Ici x₀) y), ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε
Tactic: rcases (((tendsto_order.1 W).2 ε εpos).and (hL x₀ hx₀)).exists with ⟨y, hy, h'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
inst_2 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
have obtain : ∀ (y : α) (y_mem : y ∈ s) (hy : eVariationOn f (s ∩ Ici y) < ε), ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
Tactic: obtain ⟨y, y_mem, hy⟩ : ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε := by
    have W := hf.tendsto_eVariationOn_Ici_zero_of_filter L hL
    rcases (((tendsto_order.1 W).2 ε εpos).and (hL x₀ hx₀)).exists with ⟨y, hy, h'y⟩
    exact ⟨y, h'y.1, 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
inst_2 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
⊢ ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
have refine_1 : f '' (s ∩ Ici y) ∈ map f L
Tactic: refine ⟨f '' (s ∩ Ici 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
inst_2 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
refine_1 : f '' (s ∩ Ici y) ∈ map f L
⊢ ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
have refine_2 : ∀ x ∈ f '' (s ∩ Ici y), ∀ y_1 ∈ f '' (s ∩ Ici y), edist x y_1 < ε
Tactic: refine ⟨f '' (s ∩ Ici 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
inst_2 : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
⊢ f '' (s ∩ Ici y) ∈ map f L
have refine_1 : f ⁻¹' f '' (s ∩ Ici y) ∈ L
Tactic: simp only [mem_map]