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 : 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
obtain : ∀ (y : α) (y_mem : y ∈ s) (hy : eVariationOn f (s ∩ Ici y) < ε), ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x 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⟩
-- 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
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
⊢ ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
⟨f '' (s ∩ Ici y), ?_, ?_⟩

Premises used: Set.Ici, Inter.inter, And.intro, Exists.intro, Set.image
-- 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
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
refine_1 : f '' (s ∩ Ici y) ∈ map f L
refine_2 : ∀ x ∈ f '' (s ∩ Ici y), ∀ y_1 ∈ f '' (s ∩ Ici y), edist x y_1 < ε
⊢ ∃ t ∈ map f L, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
refine ⟨f '' (s ∩ Ici y), ?_, ?_⟩
-- 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
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
refine_1 : f ⁻¹' f '' (s ∩ Ici y) ∈ L
⊢ f '' (s ∩ Ici y) ∈ map f L

Tactic:
simp only [mem_map]

Premises used: Filter.mem_map
-- 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
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
⊢ f ⁻¹' f '' (s ∩ Ici y) ∈ L

Tactic:
apply mem_of_superset (hL y y_mem) (subset_preimage_image _ _)

Premises used: Set.subset_preimage_image, Filter.mem_of_superset
-- 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
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
a : α
ha : a ∈ s ∩ Ici y
b : α
hb : b ∈ s ∩ Ici y
⊢ edist (f a) (f b) < ε

Tactic:
(eVariationOn.edist_le _ ha hb).trans_lt hy

Premises used: eVariationOn.edist_le, LE.le.trans_lt
-- 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
y : α
y_mem : y ∈ s
hy : eVariationOn f (s ∩ Ici y) < ε
a : α
ha : a ∈ s ∩ Ici y
b : α
hb : b ∈ s ∩ Ici y
⊢ edist (f a) (f b) < ε

Tactic:
exact (eVariationOn.edist_le _ ha hb).trans_lt hy

Premises used: eVariationOn.edist_le, LE.le.trans_lt
-- 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 α
hf : BoundedVariationOn f s
x : α
simp_rw : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iio x ∩ Ici y)) (𝓝[s ∩ Iio x] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)

Tactic:
simp_rw [← Iio_inter_Ici, ← inter_assoc]

Premises used: Set.inter_assoc, Set.Iio_inter_Ici
-- 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 α
hf : BoundedVariationOn f s
x : α
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iio x ∩ Ici y)) (𝓝[s ∩ Iio x] x) (𝓝 0)

Tactic:
(hf.mono inter_subset_left).tendsto_eVariationOn_Ici_zero_of_filter (𝓝[s ∩ Iio x] x)
      (fun y hy ↦ inter_mem_nhdsWithin _ (Ici_mem_nhds hy.2))

Premises used: BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filter, inter_mem_nhdsWithin, nhdsWithin, Set.inter_subset_left, Inter.inter, And.right, Ici_mem_nhds, Set.Iio, BoundedVariationOn.mono
-- 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 α
hf : BoundedVariationOn f s
x : α
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iio x ∩ Ici y)) (𝓝[s ∩ Iio x] x) (𝓝 0)

Tactic:
exact (hf.mono inter_subset_left).tendsto_eVariationOn_Ici_zero_of_filter (𝓝[s ∩ Iio x] x)
      (fun y hy ↦ inter_mem_nhdsWithin _ (Ici_mem_nhds hy.2))

Premises used: BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filter, inter_mem_nhdsWithin, nhdsWithin, Set.inter_subset_left, Inter.inter, And.right, Ici_mem_nhds, Set.Iio, BoundedVariationOn.mono
-- 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 α
hf : BoundedVariationOn f s
x : α
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)

Tactic:
have A : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0) := by
    simp_rw [← Iio_inter_Ici, ← inter_assoc]
    exact (hf.mono inter_subset_left).tendsto_eVariationOn_Ici_zero_of_filter (𝓝[s ∩ Iio x] x)
      (fun y hy ↦ inter_mem_nhdsWithin _ (Ici_mem_nhds hy.2))
-- 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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
apply : (𝓝[s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)

Tactic:
apply tendsto_const_nhds.congr'

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- 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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
a : α
ha : a ∈ s ∩ Ici x
⊢ Ico a x = ∅

Tactic:
grind
-- 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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
a : α
ha : a ∈ s ∩ Ici x
⊢ 0 = eVariationOn f (s ∩ Ico a x)

Tactic:
simp [show Ico a x = ∅ by grind]
-- 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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        x_1 ∈ s ∩ Ici x →
          Membership.mem (γ := Set α)
            {x_2 : α |
              (fun (x_3 : α) ↦
                  Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (0 : ℝ≥0∞)) x_3) ((fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) x_3))
                x_2}
            x_1}
      a
h₁ h₂ : ∀ (a : α) (ha : a ∈ s ∩ Ici x), 0 = eVariationOn f (s ∩ Ico a x)
⊢ (𝓝[s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha using by simp [show Ico a x = ∅ by grind]

Premises used: self_mem_nhdsWithin
-- 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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)

Tactic:
have B : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0) := by
    apply tendsto_const_nhds.congr'
    filter_upwards [self_mem_nhdsWithin] with a ha using by simp [show Ico a x = ∅ by grind]
-- 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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
B : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
⊢ s = s ∩ Iio x ∪ s ∩ Ici x

Tactic:
grind
-- 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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
B : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
nth_rewrite : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x ∪ s ∩ Ici x] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s] x) (𝓝 0)

Tactic:
nth_rewrite 2 [show s = (s ∩ Iio x) ∪ (s ∩ Ici x) by grind]
-- 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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
B : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
rw :
  Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0) ∧
    Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x ∪ s ∩ Ici x] x) (𝓝 0)

Tactic:
rw [nhdsWithin_union, tendsto_sup]

Premises used: Filter.tendsto_sup, nhdsWithin_union
-- 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 α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
B : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0) ∧
    Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)

Tactic:
simp [A, B]
-- 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 α
hf : BoundedVariationOn f s
x : α
h :
  ∀ (y : α),
    eVariationOn f (s ∩ Ioc x y) =
      eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
        ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
⊢ Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)

Tactic:
ext y
-- 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 α
hf : BoundedVariationOn f s
x y : α
h :
  eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc x y)
h₁ :
  eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Ioc x y))
h₂ h₃ : eVariationOn f (s ∩ Ioc x y) = eVariationOn f (s ∩ Ioc x y)
⊢ eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)

Tactic:
rw [Ico_toDual, ← preimage_inter, comp_ofDual]

Premises used: Set.preimage_inter, Set.Ico_toDual, 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 α
hf : BoundedVariationOn f s
x : α
⊢ Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)

Tactic:
have : (fun y ↦ eVariationOn f (s ∩ Ioc x y)) =
      (fun y ↦ eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s ∩ Ico (toDual y) (toDual x))) := by
    ext y
    rw [Ico_toDual, ← preimage_inter, 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 α
hf : BoundedVariationOn f s
x : α
this :
  Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
rw :
  Tendsto (β := ℝ≥0∞)
    (fun (y : α) ↦
      eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
        ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ))
    (𝓝[s] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) (𝓝[s] x) (𝓝 0)

Tactic:
rw [this]
-- 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 α
hf : BoundedVariationOn f s
x : α
this :
  Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (y : α) ↦
      eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
        ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ))
    (𝓝[s] x) (𝓝 0)

Tactic:
hf.ofDual.tendsto_eVariationOn_Ico_zero (toDual x)

Premises used: OrderDual.toDual, Set.Mem, setOf, BoundedVariationOn.ofDual, Set.preimage, BoundedVariationOn.tendsto_eVariationOn_Ico_zero, OrderDual, DFunLike.coe
-- 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 α
hf : BoundedVariationOn f s
x : α
this :
  Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (y : α) ↦
      eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
        ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ))
    (𝓝[s] x) (𝓝 0)

Tactic:
exact hf.ofDual.tendsto_eVariationOn_Ico_zero (toDual x)

Premises used: OrderDual.toDual, BoundedVariationOn.ofDual, BoundedVariationOn.tendsto_eVariationOn_Ico_zero, DFunLike.coe
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
inl : ∀ (h' : 𝓝[s ∩ Iio x] x = ⊥), Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)
inr : ∀ (h' : (𝓝[s ∩ Iio x] x).NeBot), Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)

Tactic:
rcases eq_or_neBot (𝓝[s ∩ Iio x] x) with h' | h'

Premises used: nhdsWithin, Inter.inter, Filter.eq_or_neBot, 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
inl : (𝓝[s] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)

Tactic:
apply tendsto_const_nhds.congr'

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
⊢ s = s ∩ Iio x ∪ s ∩ Ici x

Tactic:
grind
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
⊢ s = s ∩ Iio x ∪ s ∩ Ici x

Tactic:
have : s = (s ∩ Iio x) ∪ (s ∩ Ici x) := by grind
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
inl : (𝓝[s ∩ Iio x ∪ s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
⊢ (𝓝[s] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)

Tactic:
nth_rewrite 1 [this]
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
inl : (𝓝[s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
⊢ (𝓝[s ∩ Iio x ∪ s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)

Tactic:
simp only [nhdsWithin_union, h', bot_le, sup_of_le_right]

Premises used: sup_of_le_right, nhdsWithin_union, bot_le
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
h₁ : ∀ (y : α) (hy : y ∈ s ∩ Ici x), 0 = eVariationOn f (s ∩ Icc y x)
⊢ (𝓝[s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Premises used: self_mem_nhdsWithin
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
y : α
hy : y ∈ s ∩ Ici x
⊢ (s ∩ Icc y x).Subsingleton

Tactic:
grind [Set.Subsingleton]

Premises used: Set.Subsingleton
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
y : α
hy : y ∈ s ∩ Ici x
⊢ 0 = eVariationOn f (s ∩ Icc y x)

Tactic:
apply (eVariationOn.subsingleton _ (by grind [Set.Subsingleton])).symm

Premises used: eVariationOn.subsingleton, Eq.symm
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
apply : ∀ (y : α), eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)

Tactic:
apply (hf.tendsto_eVariationOn_Ico_zero x).congr (fun y ↦ ?_)

Premises used: Filter.Tendsto.congr, BoundedVariationOn.tendsto_eVariationOn_Ico_zero
-- 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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
inl : ∀ (hy : x ≤ y), eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
inr : ∀ (hy : y < x), eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)

Tactic:
rcases le_or_gt x y with hy | hy

Premises used: le_or_gt