-- 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
hn : u n = a
h₁ :
  ∀ (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)
⊢ ∑
      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₂ : ∀ (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),
  ∑
      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
                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 + 1)
                    (Subtype.mk (p := fun (u : ℕ → α) ↦
                      StrictMonoOn u (Iic (n + 1)) ∧ ∀ i ∈ Iic (n + 1), 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 + 1)
                    (Subtype.mk (p := fun (u : ℕ → α) ↦
                      StrictMonoOn u (Iic (n + 1)) ∧ ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a) u sorry))) :
              ℕ → α)
            i)) ≤
    eVariationOn f (s ∩ Iio a)
Tactic: cases n with
  | zero => simp
  | succ n =>
    simp only [Finset.range_add_one, Finset.mem_range, lt_self_iff_false, not_false_eq_true,
      Finset.sum_insert, ge_iff_le]
    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)
    apply le_of_tendsto this
    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])
    filter_upwards [this] with b hb
    let v i := if i ≤ n then u i else b
    calc 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)) := by
      simp only [Finset.range_add_one, Finset.mem_range, lt_self_iff_false, not_false_eq_true,
        Finset.sum_insert]
      congr 1 <;> grind [Finset.sum_congr]
    _ ≤ eVariationOn f (s ∩ Iio a) :=
      sum_le_of_monotoneOn_Iic (by grind [MonotoneOn, StrictMonoOn]) (by grind [StrictMonoOn])
Cleared hypotheses: n, u_mono, u_mem, this, hn