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 α
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')

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))
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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')
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
⊢ False

Tactic:
choose! y y_mem le_y using B
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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₀
⊢ v 0 ∈ s

Tactic:
simpa [v] using hx₀
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
succ : y (y^[n] x₀) ∈ s
⊢ v (n + 1) ∈ s

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, v]

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ y (y^[n] x₀) ∈ s

Tactic:
(y_mem _ ih).1

Premises used: Set.Mem, And.left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ y (y^[n] x₀) ∈ s

Tactic:
exact (y_mem _ ih).1

Premises used: And.left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
succ : ∀ (n : ℕ) (ih : v n ∈ s), v (n + 1) ∈ s
⊢ v n ∈ 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

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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

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
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
⊢ (↑n : ℝ≥0∞) * δ = ∑ i ∈ Finset.range n, δ

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
h : ∀ (i : ℕ) (hi : i ∈ Finset.range n), δ ≤ eVariationOn f (s ∩ Icc (v i) (v (i + 1)))
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, δ) (∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (v i) (v (i + 1))))

Tactic:
gcongr with i hi
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
h : δ ≤ eVariationOn f (s ∩ Icc (y^[i] x₀) (y (y^[i] x₀)))
⊢ δ ≤ eVariationOn f (s ∩ Icc (v i) (v (i + 1)))

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, v]

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 (y^[i] x₀) (y (y^[i] 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 α
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
hn : ∀ (i : ℕ), 0 < i → i < n → v i ∈ s
⊢ ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (v i) (v (i + 1))) = eVariationOn f (s ∩ Icc (v 0) (v n))

Tactic:
apply eVariationOn.sum

Premises used: eVariationOn.sum
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
apply : ∀ (n : ℕ), v n ≤ v (n + 1)
⊢ Monotone v

Tactic:
apply monotone_nat_of_le_succ (fun n ↦ ?_)

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
simp : y^[n] x₀ ≤ y (y^[n] x₀)
⊢ v n ≤ v (n + 1)

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, v]

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
⊢ y^[n] x₀ ≤ y (y^[n] x₀)

Tactic:
(y_mem _ (I n)).2

Premises used: Set.Ici, Set.Mem, setOf, And.right
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
⊢ y^[n] x₀ ≤ y (y^[n] x₀)

Tactic:
exact (y_mem _ (I n)).2

Premises used: And.right
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ), 0 < i → i < n → 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 α
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 : ℕ), (↑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
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ Ne (α := ℝ≥0∞) ∞ 0 ∨ δ ≠ ∞

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * δ) atTop (𝓝 (∞ * δ))

Tactic:
have : Tendsto (fun (n : ℕ) ↦ n * δ) atTop (𝓝 (∞ * δ)) :=
    ENNReal.Tendsto.mul_const ENNReal.tendsto_nat_nhds_top (by simp)
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 (𝓝 (∞ * δ))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * δ) atTop (𝓝 ∞)

Tactic:
rw [ENNReal.top_mul δpos.ne'] at this

Premises used: ENNReal.top_mul, LT.lt.ne'
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 (𝓝 ∞)
⊢ ∞ ≤ eVariationOn f s

Tactic:
have : ∞ ≤ eVariationOn f s := le_of_tendsto this (Eventually.of_forall J)
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
order₄ order₅ order₆ order₇ order₈ order₉ order₁₀ order₁₁ : True → False
⊢ False

Tactic:
order
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
rcases : ∀ (x₀ : α) (hx₀ : x₀ ∈ s), ∃ (l : E), Tendsto f L (𝓝 l)
⊢ ∃ (l : E), Tendsto f L (𝓝 l)

Tactic:
rcases hs with ⟨x₀, hx₀⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
inr : ∀ (h : L.NeBot), ∃ (l : E), Tendsto f L (𝓝 l)
⊢ ∃ (l : E), Tendsto f L (𝓝 l)

Tactic:
rcases Filter.eq_or_neBot L with h | h

Premises used: Filter.eq_or_neBot
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 = ⊥
inl : Nonempty E
⊢ ∃ (l : E), Tendsto f L (𝓝 l)

Tactic:
simp only [h, tendsto_bot, exists_const_iff, and_true]

Premises used: Filter.tendsto_bot, and_true, exists_const_iff
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 = ⊥
⊢ Nonempty E

Tactic:
⟨f x₀⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 = ⊥
⊢ Nonempty E

Tactic:
exact ⟨f x₀⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
inr : Cauchy (map f L)
⊢ ∃ (l : E), Tendsto f L (𝓝 l)

Tactic:
apply CompleteSpace.complete

Premises used: CompleteSpace.complete
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ map f L ≠ ⊥

Tactic:
simp [neBot_iff.mp h]

Premises used: Filter.neBot_iff, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
apply : ∀ (ε : ℝ≥0∞) (εpos : ε > 0), ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
⊢ Cauchy (map f L)

Tactic:
apply EMetric.cauchy_iff.2 ⟨by simp [neBot_iff.mp h], fun ε εpos ↦ ?_⟩

Premises used: Iff.mpr, And.intro, EMetric.cauchy_iff
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)

Tactic:
have W := hf.tendsto_eVariationOn_Ici_zero_of_filter L hL
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
rcases : ∀ (y : α) (hy : eVariationOn f (s ∩ Ici y) < ε) (h'y : (s ∩ Ici x₀) y), ∃ y ∈ s, eVariationOn f (s ∩ Ici 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⟩

Premises used: tendsto_order, Filter.Eventually.and, Filter.Eventually.exists, And.right, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : α
hy : eVariationOn f (s ∩ Ici y) < ε
h'y : (s ∩ Ici x₀) y
⊢ ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε

Tactic:
⟨y, h'y.1, hy⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : α
hy : eVariationOn f (s ∩ Ici y) < ε
h'y : (s ∩ Ici x₀) y
⊢ ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε

Tactic:
exact ⟨y, h'y.1, hy⟩