Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
⊢ eVariationOn f (s ∩ Iic a) = eVariationOn f (s ∩ Iio a) + edist (f a) l

Tactic:
refine le_antisymm ?_ ?_
  · rw [eVariationOn_eq_strictMonoOn]
    apply iSup_le
    rintro ⟨n, u, u_mono, u_mem⟩
    have : u n ≤ a := (u_mem n (by simp)).2
    rcases this.eq_or_lt with hn | hn; swap
    · exact (sum_le_of_monotoneOn_Iic u_mono.monotoneOn (by grind [StrictMonoOn])).trans le_self_add
    cases n with
    | zero => simp
    | succ n =>
      have : Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
          (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l)) :=
        (Tendsto.edist tendsto_const_nhds h'f).const_add _
      apply ge_of_tendsto this
      have : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a :=
        inter_mem_nhdsWithin_inter self_mem_nhdsWithin (Ioo_mem_nhdsLT (by grind [StrictMonoOn]))
      filter_upwards [this] with y hy
      let v i := if i ≤ n then u i else if i = n + 1 then y else a
      have A : ∑ i ∈ Finset.range (n + 1), edist (f (u (i + 1))) (f (u i))
          ≤ ∑ i ∈ Finset.range (n + 2), edist (f (v (i + 1))) (f (v i)) := by
        simp only [Finset.sum_range_succ, add_assoc]
        gcongr with i h
        · grind
        · grw [add_comm (edist _ _), ← edist_triangle]
          grind
      have B : ∑ i ∈ Finset.range (n + 2), edist (f (v (i + 1))) (f (v i)) ≤
            eVariationOn f (s ∩ Iio a) + edist (f a) (f y) := by
        rw [Finset.sum_range_succ]
        gcongr
        · apply sum_le_of_monotoneOn_Iic <;> grind [MonotoneOn, StrictMonoOn]
        · grind
      exact A.trans B
  · obtain ⟨b, hb⟩ : (s ∩ Iio a).Nonempty := by contrapose! h; simp [h]
    have : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a }) :=
      ⟨0, ⟨fun i ↦ b, by grind [StrictMonoOn]⟩⟩
    rw [eVariationOn_eq_strictMonoOn, ENNReal.iSup_add]
    apply iSup_le
    rintro ⟨n, u, u_mono, u_mem⟩
    have : Tendsto (fun y ↦ ∑ i ∈ Finset.range n,
        edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
        (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) l)) :=
      (Tendsto.edist tendsto_const_nhds h'f).const_add _
    apply le_of_tendsto this
    have : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a :=
      inter_mem_nhdsWithin_inter self_mem_nhdsWithin (Ioo_mem_nhdsLT (by grind [StrictMonoOn]))
    filter_upwards [this, self_mem_nhdsWithin] with y hy h'y
    let v i := if i ≤ n then u i else if i = n + 1 then y else a
    have A : ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) + edist (f a) (f y)
        ≤ ∑ i ∈ Finset.range (n + 2), edist (f (v (i + 1))) (f (v i)) := by
      simp only [Finset.sum_range_succ, add_assoc]
      gcongr with i h
      · grind
      · exact le_add_left (by grind)
    have B : ∑ i ∈ Finset.range (n + 2), edist (f (v (i + 1))) (f (v i)) ≤
        eVariationOn f (s ∩ Iic a) :=
      sum_le_of_monotoneOn_Iic (by grind [MonotoneOn, StrictMonoOn]) (by grind)
    exact A.trans B

Goal state after: