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
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s ∩ Iic a
this : u n ≤ a
hn : u n < a
⊢ ∀
    i ≤
      Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
        (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a }) n
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a) u ⋯)),
    (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
              (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a }) n
                (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a) u ⋯))) :
          ℕ → α)
        i ∈
      s ∩ Iio a

Tactic:
grind [StrictMonoOn]

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

Tactic:
exact sum_le_of_monotoneOn_Iic u_mono.monotoneOn (by grind [StrictMonoOn])

Premises used: eVariationOn.sum_le_of_monotoneOn_Iic, StrictMonoOn.monotoneOn
-- 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 : ℕ → α
u_mono : StrictMonoOn u (Iic 0)
u_mem : ∀ (i : ℕ), Membership.mem (γ := Set ℕ) (Iic 0) i → u i ∈ s ∩ Iic a
this : u 0 ≤ a
hn : u 0 = a
⊢ ∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a }) 0
              (Subtype.mk (p := fun (u : ℕ → α) ↦
                StrictMonoOn u (Iic 0) ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℕ) (Iic 0) i → u i ∈ s ∩ Iic a) u ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
                    0
                    (Subtype.mk (p := fun (u : ℕ → α) ↦
                      StrictMonoOn u (Iic 0) ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℕ) (Iic 0) i → u i ∈ s ∩ Iic a) u
                      ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
                    0
                    (Subtype.mk (p := fun (u : ℕ → α) ↦
                      StrictMonoOn u (Iic 0) ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℕ) (Iic 0) i → u i ∈ s ∩ Iic a) u
                      ⋯))) :
              ℕ → α)
            i)) ≤
    eVariationOn f (s ∩ Iio a)

Tactic:
simp
-- 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 : u (n + 1) ≤ a
hn : u (n + 1) = a
h₁ :
  edist (f (u (n + 1))) (f (u n)) + ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Iio a)
⊢ ∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
              (n + 1)
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic (n + 1)) ∧ ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a) u
                ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
                    (n + 1)
                    (Subtype.mk (p := fun (u : ℕ → α) ↦
                      StrictMonoOn u (Iic (n + 1)) ∧ ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a) u ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iic a })
                    (n + 1)
                    (Subtype.mk (p := fun (u : ℕ → α) ↦
                      StrictMonoOn u (Iic (n + 1)) ∧ ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a) u ⋯))) :
              ℕ → α)
            i)) ≤
    eVariationOn f (s ∩ Iio a)

Tactic:
simp only [Finset.range_add_one, Finset.mem_range, lt_self_iff_false, not_false_eq_true,
      Finset.sum_insert, ge_iff_le]

Premises used: ge_iff_le, Finset.range_add_one, Finset.mem_range, lt_self_iff_false, Finset.sum_insert, not_false_eq_true
-- 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 : u (n + 1) ≤ a
hn : u (n + 1) = a
hf : Tendsto (fun (x : α) ↦ edist (f x) (f (u n))) (𝓝[s ∩ Iio a] a) (𝓝 (edist (f (u (n + 1))) (f (u n))))
⊢ 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))))

Tactic:
apply Tendsto.add_const

Premises used: Filter.Tendsto.add_const
-- 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 : u (n + 1) ≤ a
hn : u (n + 1) = a
apply : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 (f (u (n + 1))))
⊢ Tendsto (fun (x : α) ↦ edist (f x) (f (u n))) (𝓝[s ∩ Iio a] a) (𝓝 (edist (f (u (n + 1))) (f (u n))))

Tactic:
apply Tendsto.edist _ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.edist
-- 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 : u (n + 1) ≤ a
hn : u (n + 1) = a
rw : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 (f a))
⊢ Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 (f (u (n + 1))))

Tactic:
rw [hn]
-- 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 : u (n + 1) ≤ a
hn : u (n + 1) = a
apply : 𝓝[s ∩ Iio a] a ≤ 𝓝[s ∩ Iic a] a
⊢ Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 (f a))

Tactic:
apply h'.tendsto.mono_left

Premises used: Filter.Tendsto.mono_left, ContinuousWithinAt.tendsto
-- 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 : u (n + 1) ≤ a
hn : u (n + 1) = a
⊢ s ∩ Iio a ⊆ s ∩ Iic a

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 α
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 : u (n + 1) ≤ a
hn : u (n + 1) = a
⊢ 𝓝[s ∩ Iio a] a ≤ 𝓝[s ∩ Iic a] a

Tactic:
exact nhdsWithin_mono _ (by grind)

Premises used: nhdsWithin_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 α
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 : u (n + 1) ≤ a
hn : u (n + 1) = a
⊢ 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))))

Tactic:
have : 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)))) := by
      apply Tendsto.add_const
      apply Tendsto.edist _ tendsto_const_nhds
      rw [hn]
      apply h'.tendsto.mono_left
      exact nhdsWithin_mono _ (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 α
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 :
  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))))
h₁ :
  ∀ᶠ (c : α) in 𝓝[s ∩ Iio a] a,
    edist (f c) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a)
⊢ edist (f (u (n + 1))) (f (u n)) + ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) ≤ eVariationOn f (s ∩ Iio a)

Tactic:
apply le_of_tendsto this

Premises used: le_of_tendsto
-- 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 :
  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))))
rw : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
⊢ s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a

Tactic:
rw [hn]
-- 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 :
  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))))
apply : Ioo (u n) a ∈ 𝓝[<] a
⊢ s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a

Tactic:
apply inter_mem_nhdsWithin_inter self_mem_nhdsWithin

Premises used: inter_mem_nhdsWithin_inter, 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 α
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 :
  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))))
⊢ u n < a

Tactic:
grind [StrictMonoOn]

Premises used: 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 : α → 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 :
  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))))
⊢ Ioo (u n) a ∈ 𝓝[<] a

Tactic:
exact Ioo_mem_nhdsLT (by grind [StrictMonoOn])

Premises used: Ioo_mem_nhdsLT
-- 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 :
  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))))
⊢ s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a

Tactic:
have : s ∩ Ioo (u n) (u (n + 1)) ∈ 𝓝[s ∩ Iio a] a := by
      rw [hn]
      apply inter_mem_nhdsWithin_inter self_mem_nhdsWithin
      exact Ioo_mem_nhdsLT (by grind [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 : α → 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
h₁ :
  ∀ (b : α) (hb : b ∈ s ∩ Ioo (u n) (u (n + 1))),
    edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a)
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Iio a] a,
    edist (f c) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f (s ∩ Iio a)

Tactic:
filter_upwards [this] with b hb
-- 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
simp :
  edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    edist (f (v (n + 1))) (f (v n)) + ∑ x ∈ Finset.range n, edist (f (v (x + 1))) (f (v x))
⊢ 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))

Tactic:
simp only [Finset.range_add_one, Finset.mem_range, lt_self_iff_false, not_false_eq_true,
        Finset.sum_insert]

Premises used: Finset.range_add_one, Finset.mem_range, lt_self_iff_false, Finset.sum_insert, not_false_eq_true
-- 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
e_a : edist (f b) (f (u n)) = edist (f (v (n + 1))) (f (v n))
e_a₁ :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ x ∈ Finset.range n, edist (f (v (x + 1))) (f (v x)))
⊢ edist (f b) (f (u n)) + ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    edist (f (v (n + 1))) (f (v n)) + ∑ x ∈ Finset.range n, edist (f (v (x + 1))) (f (v x))

Tactic:
congr 1
-- 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
⊢ edist (f b) (f (u n)) = edist (f (v (n + 1))) (f (v n))

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
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
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ x ∈ Finset.range n, edist (f (v (x + 1))) (f (v x)))

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
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
⊢ MonotoneOn v (Iic (n + 1))

Tactic:
grind [MonotoneOn, StrictMonoOn]

Premises used: MonotoneOn, 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 : α → 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
⊢ ∀ i ≤ n + 1, v i ∈ s ∩ Iio a

Tactic:
grind [StrictMonoOn]

Premises used: StrictMonoOn