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 α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : x ≤ y
inl : (s ∩ Icc y x).Subsingleton
inl₁ : (s ∩ Ico y x).Subsingleton
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)

Tactic:
rw [eVariationOn.subsingleton, eVariationOn.subsingleton]

Premises used: eVariationOn.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).NeBot
y : α
hy : x ≤ y
⊢ (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).NeBot
y : α
hy : x ≤ y
⊢ (s ∩ Ico 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).NeBot
y : α
hy : y < x
inr :
  ∀ (W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)),
    eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
inr₁ : (𝓝[s ∩ Icc y x ∩ Iio x] x).NeBot
inr₂ : ContinuousWithinAt f (s ∩ Icc y x ∩ Iic x) x
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)

Tactic:
have W := eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt (f := f)
    (s := s ∩ Icc y x) (a := x) ?_ ?_
-- 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 : α
hy : y < x
W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)
⊢ eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)

Tactic:
W
-- 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 : α
hy : y < x
W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)
h₁ : s ∩ Ico y x = s ∩ Icc y x ∩ Iio x
h₂ : s ∩ Icc y x = s ∩ Icc y x ∩ Iic x
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)

Tactic:
convert! W using 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 : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)
⊢ s ∩ Ico y x = s ∩ Icc y x ∩ Iio 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).NeBot
y : α
hy : y < x
W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)
⊢ s ∩ Icc y x = s ∩ Icc y x ∩ Iic 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).NeBot
y : α
hy : y < x
⊢ s ∩ Icc y x ∩ Iio x = s ∩ Iio x ∩ Ici y

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).NeBot
y : α
hy : y < x
inr : Ici y ∈ 𝓝[s ∩ Iio x] x
⊢ (𝓝[s ∩ Icc y x ∩ Iio x] x).NeBot

Tactic:
rwa [show s ∩ Icc y x ∩ Iio x = (s ∩ Iio x) ∩ Ici y by grind, nhdsWithin_inter_of_mem']

Premises used: nhdsWithin_inter_of_mem'
-- 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 : α
hy : y < x
inr : Ici y ∈ 𝓝 x
⊢ Ici y ∈ 𝓝[s ∩ Iio x] x

Tactic:
apply mem_nhdsWithin_of_mem_nhds

Premises used: mem_nhdsWithin_of_mem_nhds
-- 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 : α
hy : y < x
⊢ Ici y ∈ 𝓝 x

Tactic:
Ici_mem_nhds hy

Premises used: Ici_mem_nhds
-- 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 : α
hy : y < x
⊢ Ici y ∈ 𝓝 x

Tactic:
exact Ici_mem_nhds hy

Premises used: Ici_mem_nhds
-- 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 : α
hy : y < x
⊢ s ∩ Icc y x ∩ Iic x ⊆ s ∩ Iic 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).NeBot
y : α
hy : y < x
⊢ ContinuousWithinAt f (s ∩ Icc y x ∩ Iic x) x

Tactic:
apply h.mono (by grind)

Premises used: ContinuousWithinAt.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 : α
h : ContinuousWithinAt f (s ∩ Ici x) x
h₁ :
  ∀ (y : α),
    eVariationOn f (s ∩ Icc x y) =
      eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
        ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
⊢ Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((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 : α
h : ContinuousWithinAt f (s ∩ Ici x) x
y : α
h₁ :
  eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc x y)
h₂ :
  eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Icc x y))
h₃ h₄ : eVariationOn f (s ∩ Icc x y) = eVariationOn f (s ∩ Icc x y)
⊢ eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)

Tactic:
rw [Icc_toDual, ← preimage_inter, comp_ofDual]

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

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

Tactic:
hf.ofDual.tendsto_eVariationOn_Icc_zero_left h

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

Tactic:
exact hf.ofDual.tendsto_eVariationOn_Icc_zero_left h

Premises used: BoundedVariationOn.ofDual, BoundedVariationOn.tendsto_eVariationOn_Icc_zero_left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
inl : ∀ (hs : s ∩ Iio x = ∅), ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
inr : ∀ (hs : (s ∩ Iio x).Nonempty), ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
⊢ ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)

Tactic:
rcases eq_empty_or_nonempty (s ∩ Iio x) with hs | hs

Premises used: Inter.inter, Set.eq_empty_or_nonempty, Set.Iio
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
hs : s ∩ Iio x = ∅
inl : Nonempty E
⊢ ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)

Tactic:
simp only [hs, nhdsWithin_empty, tendsto_bot, exists_const_iff, and_true]

Premises used: Filter.tendsto_bot, and_true, exists_const_iff, nhdsWithin_empty
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
hs : s ∩ Iio x = ∅
⊢ 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
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
hs : s ∩ Iio x = ∅
⊢ 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
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
hs : (s ∩ Iio x).Nonempty
⊢ ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)

Tactic:
BoundedVariationOn.exists_tendsto_left_of_filter (s := s ∩ Iio x)
    (hf.mono inter_subset_left) _ (fun y hy ↦ inter_mem_nhdsWithin _ (Ici_mem_nhds hy.2)) hs

Premises used: inter_mem_nhdsWithin, BoundedVariationOn.exists_tendsto_left_of_filter, 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 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
hs : (s ∩ Iio x).Nonempty
⊢ ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)

Tactic:
exact BoundedVariationOn.exists_tendsto_left_of_filter (s := s ∩ Iio x)
    (hf.mono inter_subset_left) _ (fun y hy ↦ inter_mem_nhdsWithin _ (Ici_mem_nhds hy.2)) hs

Premises used: inter_mem_nhdsWithin, BoundedVariationOn.exists_tendsto_left_of_filter, 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 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
⊢ ∃ (l : E), Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)

Tactic:
hf.ofDual.exists_tendsto_left (toDual x)

Premises used: OrderDual.toDual, Set.Ioi, Set.Mem, setOf, BoundedVariationOn.ofDual, BoundedVariationOn.exists_tendsto_left, Set.preimage, OrderDual, DFunLike.coe
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
hf : BoundedVariationOn f univ
x : α
h : ∃ (y : E), Tendsto f (𝓝[<] x) (𝓝 y)
⊢ Tendsto f (𝓝[<] x) (𝓝 (Function.leftLim f x))

Tactic:
apply tendsto_leftLim_of_tendsto

Premises used: tendsto_leftLim_of_tendsto
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ ∃ (l : E), Tendsto f (𝓝[univ ∩ Iio x] x) (𝓝 l)

Tactic:
hf.exists_tendsto_left x

Premises used: BoundedVariationOn.exists_tendsto_left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
hf : BoundedVariationOn f univ
x : α
h : ∀ (x_1 : E), Iio x = univ ∩ Iio x
⊢ ∃ (y : E), Tendsto f (𝓝[<] x) (𝓝 y)

Tactic:
convert! hf.exists_tendsto_left x

Premises used: BoundedVariationOn.exists_tendsto_left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
hf : BoundedVariationOn f univ
x : α
x_1 : E
⊢ Iio x = univ ∩ Iio x

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ Tendsto f (𝓝[>] x) (𝓝 (Function.rightLim f x))

Tactic:
hf.ofDual.tendsto_leftLim x

Premises used: Set.Ioi, setOf, BoundedVariationOn.ofDual, BoundedVariationOn.tendsto_leftLim, Function.rightLim, OrderDual
-- 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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
rw :
  ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (g
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i + 1)))
          (g
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              i)) ≤
    eVariationOn f s
⊢ eVariationOn g s ≤ eVariationOn f s

Tactic:
rw [eVariationOn_eq_strictMonoOn]

Premises used: eVariationOn.eVariationOn_eq_strictMonoOn
-- 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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
h :
  ∀ (i : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
    ∑ i_1 ∈ Finset.range (i.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (g
            ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i_1 + 1)))
          (g
            ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              i_1)) ≤
      eVariationOn f s
⊢ ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (g
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i + 1)))
          (g
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              i)) ≤
    eVariationOn f s

Tactic:
apply iSup_le

Premises used: iSup_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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
h : ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x)) ≤ eVariationOn f s
⊢ ∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) n
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))),
      edist
        (g
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) n
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))) :
              ℕ → α)
            (i + 1)))
        (g
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) n
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))) :
              ℕ → α)
            i)) ≤
    eVariationOn f s

Tactic:
simp only
-- 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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨u 0⟩
-- 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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this : Nonempty α
apply : ∀ (c : ℝ≥0∞) (hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))), c < eVariationOn f s
⊢ ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x)) ≤ eVariationOn f s

Tactic:
apply le_of_forall_lt (fun c hc ↦ ?_)

Premises used: le_of_forall_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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
⊢ Continuous[Pi.topologicalSpace, _] fun (v : ℕ → E) ↦ ∑ i ∈ Finset.range n, edist (v (i + 1)) (v i)

Tactic:
fun_prop