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
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
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))
⊢ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a)

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])

Premises used: eVariationOn.sum_le_of_monotoneOn_Iic, eVariationOn, Inter.inter, Finset.range, HAdd.hAdd, EDist.edist, OfNat.ofNat, Set.Iio
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
rw :
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Ioi a)) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Ici a))
⊢ eVariationOn f (s ∩ Ioi a) = eVariationOn f (s ∩ Ici a)

Tactic:
rw [← comp_ofDual f, ← comp_ofDual f]

Premises used: eVariationOn.comp_ofDual
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Ioi a)) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Ici a))

Tactic:
eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt h h'

Premises used: Set.Ioi, Set.Ici, Set.Mem, setOf, Set.inter, Set.preimage, eVariationOn.eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ → α), (Monotone u ∧ ∀ (i : ℕ), u i ∈ s) ∧ ε < ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))

Tactic:
simpa [eVariationOn, lt_iSup_iff] using h

Premises used: eVariationOn, lt_iSup_iff
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
ε : ℝ≥0∞
s : Set α
h : ε < eVariationOn f s
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)
⊢ ∃ 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
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
apply : ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Icc (u 0) (u n))
⊢ ε < eVariationOn f (s ∩ Icc (u 0) (u n))

Tactic:
apply hu.trans_le

Premises used: LT.lt.trans_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
⊢ 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:
grind [Finset.sum_congr]

Premises used: Finset.sum_congr
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
ε : ℝ≥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)
⊢ MonotoneOn v (Iic n)

Tactic:
grind [MonotoneOn]

Premises used: MonotoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
⊢ ∀ i ≤ n, v i ∈ s ∩ Icc (u 0) (u n)

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
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)))
⊢ ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Icc (u 0) (u n))

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)

Premises used: eVariationOn.sum_le_of_monotoneOn_Iic, eVariationOn, Inter.inter, Finset.range, Set.Icc, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))

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

Tactic:
⟨u 0, u_mem _, u n, u_mem _, ?_, A⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
refine : u 0 < u n
⊢ ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Icc a b)

Tactic:
refine ⟨u 0, u_mem _, u n, u_mem _, ?_, A⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
by_contra! : ∀ (this : u n ≤ u 0), False
⊢ u 0 < u n

Tactic:
by_contra!
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 ∈ s ∧ u 0 ≤ a ∧ a ≤ u n

Tactic:
simp only [mem_inter_iff, mem_Icc] at ha hb

Premises used: Set.mem_inter_iff, Set.mem_Icc
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ b ∈ s ∧ u 0 ≤ b ∧ b ≤ u n

Tactic:
simp only [mem_inter_iff, mem_Icc] at ha hb

Premises used: Set.mem_inter_iff, Set.mem_Icc
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
order₄ order₅ order₆ order₇ order₈ order₉ order₁₀ order₁₁ : a ≠ b → False
⊢ a = b

Tactic:
order
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ (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
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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_1 : u n ≤ u 0
this : (s ∩ Icc (u 0) (u n)).Subsingleton
⊢ False

Tactic:
simp [this] at A
-- 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
inl :
  ∀ (hf : BoundedVariationOn f ∅) (hL : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∅ ∩ Ici y ∈ L),
    Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (∅ ∩ Ici y)) L (𝓝 0)
inr : ∀ (x₀ : α) (hx₀ : x₀ ∈ s), Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)

Tactic:
rcases eq_empty_or_nonempty s with rfl | ⟨x₀, hx₀⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
L : Filter α
hf : BoundedVariationOn f ∅
hL : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∅ ∩ Ici y ∈ L
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (∅ ∩ Ici y)) L (𝓝 0)

Tactic:
simpa using tendsto_const_nhds

Premises used: tendsto_const_nhds
-- 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
⊢ ∀ a' < 0, ∀ᶠ (b : α) in L, a' < eVariationOn f (s ∩ Ici b)

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
apply : ∀ (ε : ℝ≥0∞) (εpos : ε > 0), ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)

Tactic:
apply tendsto_order.2 ⟨by simp, fun ε εpos ↦ ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- 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∞), δ ∈ Ioo 0 ε

Tactic:
exists_between εpos

Premises used: Set.Mem, setOf, exists_between, Set.Ioo
-- 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
obtain : ∀ (δ : ℝ≥0∞) (δpos : 0 < δ) (hδ : δ < ε), ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε
⊢ ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ, δ ∈ Ioo 0 ε := exists_between εpos

Premises used: exists_between, OfNat.ofNat, Set.Ioo
-- 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δ : δ < ε
by_contra! : ∀ (H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)), False
⊢ ∀ᶠ (b : α) in L, eVariationOn f (s ∩ Ici b) < ε

Tactic:
by_contra! H
-- 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' : α), ε ≤ eVariationOn f (s ∩ Ici y') ∧ y' ∈ s ∩ Ici y

Tactic:
(H.and_eventually (hL y hy)).exists

Premises used: Set.Mem, setOf, Set.inter, Filter.Frequently.and_eventually, Filter.Frequently.exists
-- 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
obtain :
  ∀ (y' : α) (hy' : ε ≤ eVariationOn f (s ∩ Ici y')) (y'_mem : y' ∈ s ∩ Ici y),
    ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y 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

Premises used: Set.Ici, Filter.Frequently.and_eventually, Filter.Frequently.exists
-- 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' : α
hy' : ε ≤ eVariationOn f (s ∩ Ici y')
y'_mem : y' ∈ s ∩ Ici y
⊢ ∃ a ∈ s ∩ Ici y', ∃ b ∈ s ∩ Ici y', a < b ∧ δ < eVariationOn f (s ∩ Ici y' ∩ Icc a b)

Tactic:
exists_lt_eVariationOn_inter_Icc (hδ.trans_le hy')

Premises used: LT.lt.trans_le, eVariationOn.exists_lt_eVariationOn_inter_Icc
-- 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' : α
hy' : ε ≤ eVariationOn f (s ∩ Ici y')
y'_mem : y' ∈ s ∩ Ici y
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')
⊢ ∃ 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')

Premises used: Set.Ici, LT.lt.trans_le, eVariationOn.exists_lt_eVariationOn_inter_Icc
-- 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' : α
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')

Tactic:
⟨b, ⟨hb.1, le_trans y'_mem.2 hb.2⟩, ?_⟩

Premises used: And.right, And.left, And.intro, Exists.intro, le_trans
-- 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' : α
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)
refine : δ ≤ eVariationOn f (s ∩ Icc y b)
⊢ ∃ y' ∈ s ∩ Ici y, δ ≤ eVariationOn f (s ∩ Icc y y')

Tactic:
refine ⟨b, ⟨hb.1, le_trans y'_mem.2 hb.2⟩, ?_⟩
-- 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' : α
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)
⊢ Ici y' ∩ Icc a b = Icc a b

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 : α
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)
⊢ Ici y' ∩ Icc a b = Icc a b

Tactic:
have : Ici y' ∩ Icc a b = Icc a b := 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)
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 a b)

Tactic:
rw [inter_assoc, this] at h

Premises used: Set.inter_assoc
-- 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' : α
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
h₁ : δ < eVariationOn f (s ∩ Icc a b)
⊢ Ici y' ∩ Icc a b = Icc a b

Tactic:
rw [inter_assoc, this] at h

Premises used: Set.inter_assoc
-- 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' : α
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 ∩ Icc a b)
this : Ici y' ∩ Icc a b = Icc a b
⊢ s ∩ Icc a b ⊆ s ∩ Icc y b

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 : α
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 ∩ Icc a b)
this : Ici y' ∩ Icc a b = Icc a b
⊢ δ ≤ eVariationOn f (s ∩ Icc y b)

Tactic:
exact h.le.trans (mono _ (by grind))

Premises used: LT.lt.le, eVariationOn.mono, LE.le.trans