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 α
inst_4 : CompleteSpace E
inst_5 : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
this : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim f x))
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x

Tactic:
continuousWithinAt_Iio_iff_Iic.1 this

Premises used: Iff.mp, continuousWithinAt_Iio_iff_Iic
-- 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 α
inst_4 : CompleteSpace E
inst_5 : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
this : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim f x))
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x

Tactic:
exact continuousWithinAt_Iio_iff_Iic.1 this

Premises used: Iff.mp, continuousWithinAt_Iio_iff_Iic
-- 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 α
inst_4 : CompleteSpace E
inst_5 : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ ContinuousWithinAt (Function.rightLim f) (Ici x) x

Tactic:
BoundedVariationOn.continuousWithinAt_leftLim hf.ofDual

Premises used: BoundedVariationOn.continuousWithinAt_leftLim, Set.Ici, setOf, BoundedVariationOn.ofDual, Function.rightLim, OrderDual
-- 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
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ici y)) (𝓟 s ⊓ atTop) (𝓝 0)

Tactic:
hf.tendsto_eVariationOn_Ici_zero_of_filter _
    (fun y _ ↦ inter_mem_inf (mem_principal_self s) (Ici_mem_atTop y))

Premises used: BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filter, Filter.mem_principal_self, Filter.inter_mem_inf, Filter.Ici_mem_atTop
-- 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
h :
  ∀ (y : α),
    eVariationOn f (s ∩ Iic y) =
      eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
        ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ)
⊢ Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iic y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ)

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

Tactic:
rw [Ici_toDual, ← preimage_inter, comp_ofDual]

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

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

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

Tactic:
hf.ofDual.tendsto_eVariationOn_Ici_zero

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

Tactic:
exact hf.ofDual.tendsto_eVariationOn_Ici_zero

Premises used: BoundedVariationOn.ofDual, BoundedVariationOn.tendsto_eVariationOn_Ici_zero
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
hE : Nonempty E
f : α → E
s : Set α
hf : BoundedVariationOn f s
inl : ∀ (hf : BoundedVariationOn f ∅), ∃ (l : E), Tendsto f (𝓟 ∅ ⊓ atTop) (𝓝 l)
inr : ∀ (hs : s.Nonempty), ∃ (l : E), Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)
⊢ ∃ (l : E), Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)

Tactic:
rcases eq_empty_or_nonempty s with rfl | hs

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
inst_2 : CompleteSpace E
hE : Nonempty E
f : α → E
hf : BoundedVariationOn f ∅
⊢ ∃ (l : E), Tendsto f (𝓟 ∅ ⊓ atTop) (𝓝 l)

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
hE : Nonempty E
f : α → E
s : Set α
hf : BoundedVariationOn f s
hs : s.Nonempty
⊢ ∃ (l : E), Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)

Tactic:
hf.exists_tendsto_left_of_filter _
      (fun y hy ↦ inter_mem_inf (mem_principal_self s) (Ici_mem_atTop _)) hs

Premises used: Filter.mem_principal_self, Filter.inter_mem_inf, BoundedVariationOn.exists_tendsto_left_of_filter, Filter.Ici_mem_atTop
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
hE : Nonempty E
f : α → E
s : Set α
hf : BoundedVariationOn f s
hs : s.Nonempty
⊢ ∃ (l : E), Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)

Tactic:
exact hf.exists_tendsto_left_of_filter _
      (fun y hy ↦ inter_mem_inf (mem_principal_self s) (Ici_mem_atTop _)) hs

Premises used: Filter.mem_principal_self, Filter.inter_mem_inf, BoundedVariationOn.exists_tendsto_left_of_filter, Filter.Ici_mem_atTop
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
hE : Nonempty E
f : α → E
s : Set α
hf : BoundedVariationOn f s
⊢ ∃ (l : E), Tendsto f (𝓟 s ⊓ atBot) (𝓝 l)

Tactic:
hf.ofDual.exists_tendsto_atTop

Premises used: Set.Mem, BoundedVariationOn.exists_tendsto_atTop, setOf, BoundedVariationOn.ofDual, Set.preimage, Set.Iic, OrderDual
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
hE : Nonempty E
f : α → E
hf : BoundedVariationOn f univ
⊢ ∃ (x : E), Tendsto f atTop (𝓝 x)

Tactic:
simpa using hf.exists_tendsto_atTop

Premises used: BoundedVariationOn.exists_tendsto_atTop
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
hE : Nonempty E
f : α → E
hf : BoundedVariationOn f univ
⊢ ∃ (x : E), Tendsto f atBot (𝓝 x)

Tactic:
simpa using hf.exists_tendsto_atBot

Premises used: BoundedVariationOn.exists_tendsto_atBot
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
apply :
  ∀ (i : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b }),
    ∑ i_1 ∈ Finset.range i.1, edist (f ((↑i.2 : ℕ → α) (i_1 + 1))) (f ((↑i.2 : ℕ → α) i_1)) ≤ ENNReal.ofReal (f b - f a)
⊢ eVariationOn f (s ∩ Icc a b) ≤ ENNReal.ofReal (f b - f a)

Tactic:
apply iSup_le _

Premises used: iSup_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)))

Tactic:
Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
refine : ∀ (i : ℕ) (hi : i ∈ Finset.range n), edist (f (u (i + 1))) (f (u i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)))

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i ∈ Finset.range n
⊢ i < n

Tactic:
simp only [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i < n
rw : 0 ≤ f (u (i + 1)) - f (u i)
⊢ edist (f (u (i + 1))) (f (u i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))

Tactic:
rw [edist_dist, Real.dist_eq, abs_of_nonneg]

Premises used: edist_dist, Real.dist_eq, abs_of_nonneg
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i < n
⊢ 0 ≤ f (u (i + 1)) - f (u i)

Tactic:
sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))

Premises used: sub_nonneg_of_le, Nat.le_succ, And.left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i < n
⊢ 0 ≤ f (u (i + 1)) - f (u i)

Tactic:
exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))

Premises used: sub_nonneg_of_le, Nat.le_succ, And.left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
rw : ∀ i ∈ Finset.range n, 0 ≤ f (u (i + 1)) - f (u i)
⊢ ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
    ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i)))

Tactic:
rw [ENNReal.ofReal_sum_of_nonneg]

Premises used: ENNReal.ofReal_sum_of_nonneg
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
_ : i ∈ Finset.range n → 0 ≤ f (u (i + 1)) - f (u i)
⊢ i ∈ Finset.range n → 0 ≤ f (u (i + 1)) - f (u i)

Tactic:
_
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
h : i ∈ Finset.range n
⊢ 0 ≤ f (u (i + 1)) - f (u i)

Tactic:
sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))

Premises used: sub_nonneg_of_le, Nat.le_succ, And.left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
h : i ∈ Finset.range n
⊢ 0 ≤ f (u (i + 1)) - f (u i)

Tactic:
exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))

Premises used: sub_nonneg_of_le, Nat.le_succ, And.left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
rw rw₁ : ENNReal.ofReal (f (u n) - f (u 0)) = ENNReal.ofReal (f (u n) - f (u 0))
⊢ ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) = ENNReal.ofReal (f (u n) - f (u 0))

Tactic:
rw [Finset.sum_range_sub fun i => f (u i)]

Premises used: Finset.sum_range_sub
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
h : f (u n) - f (u 0) ≤ f b - f a
⊢ ENNReal.ofReal (f (u n) - f (u 0)) ≤ ENNReal.ofReal (f b - f a)

Tactic:
apply ENNReal.ofReal_le_ofReal

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ f (u n) - f (u 0) ≤ f b - f a

Tactic:
sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)

Premises used: And.right, And.left, sub_le_sub, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ f (u n) - f (u 0) ≤ f b - f a

Tactic:
exact sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)

Premises used: And.right, And.left, sub_le_sub, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)))
i₁ :
  ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
    ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i)))
i₂ : ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) = ENNReal.ofReal (f (u n) - f (u 0))
i₃ : ENNReal.ofReal (f (u n) - f (u 0)) ≤ ENNReal.ofReal (f b - f a)
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).1,
      edist
        (f
          ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) i)) ≤
    ENNReal.ofReal (f b - f a)

Tactic:
calc
    (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
        ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) := by
      refine Finset.sum_congr rfl fun i hi => ?_
      simp only [Finset.mem_range] at hi
      rw [edist_dist, Real.dist_eq, abs_of_nonneg]
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) := by
      rw [ENNReal.ofReal_sum_of_nonneg]
      intro i _
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (f (u n) - f (u 0)) := by rw [Finset.sum_range_sub fun i => f (u i)]
    _ ≤ ENNReal.ofReal (f b - f a) := by
      apply ENNReal.ofReal_le_ofReal
      exact sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)

Premises used: ENNReal.ofReal, HSub.hSub, Finset.range, HAdd.hAdd, EDist.edist, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
⊢ LocallyBoundedVariationOn f s

Tactic:
fun _ _ as bs =>
  ((hf.eVariationOn_le as bs).trans_lt ENNReal.ofReal_lt_top).ne

Premises used: LocallyBoundedVariationOn, ENNReal.ofReal_lt_top, MonotoneOn.eVariationOn_le, LE.le.trans_lt, LT.lt.ne, BoundedVariationOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
hs : (s ∩ {a}).Subsingleton
⊢ (if a ≤ a then (eVariationOn f (s ∩ Icc a a)).toReal else -(eVariationOn f (s ∩ Icc a a)).toReal) = 0

Tactic:
rw [if_pos le_rfl, Icc_self, eVariationOn.subsingleton, ENNReal.toReal_zero]

Premises used: Set.Icc_self, le_rfl, if_pos, ENNReal.toReal_zero, eVariationOn.subsingleton
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ (s ∩ {a}).Subsingleton

Tactic:
fun x hx y hy => hx.2.trans hy.2.symm

Premises used: And.right, Set.Subsingleton, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ (s ∩ {a}).Subsingleton

Tactic:
exact fun x hx y hy => hx.2.trans hy.2.symm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : a ≤ b
⊢ 0 ≤ variationOnFromTo f s a b

Tactic:
simp only [variationOnFromTo, if_pos h, ENNReal.toReal_nonneg]

Premises used: ENNReal.toReal_nonneg, if_pos, variationOnFromTo
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
inl : ∀ (ab : a < b), variationOnFromTo f s a b = -variationOnFromTo f s b a
inr : variationOnFromTo f s a a = -variationOnFromTo f s a a
inr₁ : ∀ (ba : b < a), variationOnFromTo f s a b = -variationOnFromTo f s b a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
rcases lt_trichotomy a b with (ab | rfl | ba)

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ab : a < b
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
simp only [variationOnFromTo, if_pos ab.le, if_neg ab.not_ge, neg_neg]

Premises used: neg_neg, LT.lt.le, if_pos, variationOnFromTo, LT.lt.not_ge, if_neg
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ variationOnFromTo f s a a = -variationOnFromTo f s a a

Tactic:
simp only [variationOnFromTo.self, neg_zero]

Premises used: neg_zero, variationOnFromTo.self
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ba : b < a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
simp only [variationOnFromTo, if_pos ba.le, if_neg ba.not_ge]

Premises used: LT.lt.le, if_pos, variationOnFromTo, LT.lt.not_ge, if_neg
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
rw : -variationOnFromTo f s b a ≤ 0
⊢ variationOnFromTo f s a b ≤ 0

Tactic:
rw [variationOnFromTo.eq_neg_swap]

Premises used: variationOnFromTo.eq_neg_swap
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
⊢ -variationOnFromTo f s b a ≤ 0

Tactic:
neg_nonpos_of_nonneg (variationOnFromTo.nonneg_of_le f s h)

Premises used: neg_nonpos_of_nonneg, variationOnFromTo.nonneg_of_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
⊢ -variationOnFromTo f s b a ≤ 0

Tactic:
exact neg_nonpos_of_nonneg (variationOnFromTo.nonneg_of_le f s h)

Premises used: neg_nonpos_of_nonneg, variationOnFromTo.nonneg_of_le
-- 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
a b : α
pos : ∀ (hab : a ≤ b), |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
neg : ∀ (hab : ¬a ≤ b), |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

Tactic:
by_cases hab : a ≤ 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
a b : α
hab : a ≤ b
pos : (eVariationOn f (s ∩ Icc a b)).toReal ≤ (eVariationOn f s).toReal
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

Tactic:
simp only [variationOnFromTo, hab, ↓reduceIte, ENNReal.abs_toReal]

Premises used: variationOnFromTo, reduceIte, ENNReal.abs_toReal
-- 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
a b : α
hab : a ≤ b
⊢ (eVariationOn f (s ∩ Icc a b)).toReal ≤ (eVariationOn f s).toReal

Tactic:
ENNReal.toReal_mono hf (eVariationOn.mono _ inter_subset_left)

Premises used: Set.inter_subset_left, eVariationOn.mono, ENNReal.toReal_mono