-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
h₁ :
  ∀ (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)
⊢ ∑
      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)
have h₂ : ∀ (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 sorry))),
      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 sorry))) :
              ℕ → α)
            (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 sorry))) :
              ℕ → α)
            i)) ≤
    eVariationOn f (s ∩ Iio a)
Tactic: rcases this.eq_or_lt with hn | hn