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
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ StrictMonoOn u (Iic 0)

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
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
              (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) 0
                (Subtype.mk (p := fun (u : ℕ → α) ↦
                  StrictMonoOn u (Iic 0) ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℕ) (Iic 0) i → u i ∈ s) u ⋯))) :
          ℕ → α)
        (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
          (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) 0
            (Subtype.mk (p := fun (u : ℕ → α) ↦
              StrictMonoOn u (Iic 0) ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℕ) (Iic 0) i → u i ∈ s) u ⋯))) =
      u 0 ∧
    Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range 0, edist (f (u (x + 1))) (f (u x)))
      (∑
        i ∈
          Finset.range
            (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
              (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) 0
                (Subtype.mk (p := fun (u : ℕ → α) ↦
                  StrictMonoOn u (Iic 0) ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℕ) (Iic 0) i → u i ∈ s) u ⋯))),
        edist
          (f
            ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                    (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) 0
                      (Subtype.mk (p := fun (u : ℕ → α) ↦
                        StrictMonoOn u (Iic 0) ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℕ) (Iic 0) i → u i ∈ s) u ⋯))) :
                ℕ → α)
              (i + 1)))
          (f
            ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                    (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) 0
                      (Subtype.mk (p := fun (u : ℕ → α) ↦
                        StrictMonoOn u (Iic 0) ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℕ) (Iic 0) i → u i ∈ s) u ⋯))) :
                ℕ → α)
              i)))

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∃ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
    (↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
          (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) =
        u 0 ∧
      Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range 0, edist (f (u (x + 1))) (f (u x)))
        (∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
          edist
            (f
              ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
                (i + 1)))
            (f
              ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
                i)))

Tactic:
exact ⟨⟨0, ⟨u, by grind [StrictMonoOn], fun i hi ↦ u_mem _⟩⟩, by simp⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv :
  (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
        ℕ → α)
      (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
        (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) =
    u n
h'v :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
    (∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            i)))
hn : u n = u (n + 1)
succ :
  ∃ (a : ℕ) (a_1 : ℕ → α),
    a_1 a = u n ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
          (∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x)))
⊢ ∃ (a : ℕ) (a_1 : ℕ → α),
    a_1 a = u (n + 1) ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
          ∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x))

Tactic:
simp only [← hn, edist_self, add_zero]

Premises used: PseudoEMetricSpace.edist_self, add_zero
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv :
  (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
        ℕ → α)
      (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
        (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) =
    u n
h'v :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
    (∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            i)))
hn : u n = u (n + 1)
⊢ ∃ (a : ℕ) (a_1 : ℕ → α),
    a_1 a = u n ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
          (∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x)))

Tactic:
⟨m, v, hv, ⟨v_mono, v_mem⟩, h'v⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv :
  (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
        ℕ → α)
      (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
        (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) =
    u n
h'v :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
    (∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            i)))
hn : u n = u (n + 1)
⊢ ∃ (a : ℕ) (a_1 : ℕ → α),
    a_1 a = u n ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
          (∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x)))

Tactic:
exact ⟨m, v, hv, ⟨v_mono, v_mem⟩, h'v⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv :
  (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
        ℕ → α)
      (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
        (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) =
    u n
h'v :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
    (∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            i)))
hn : u n < u (n + 1)
⊢ (fun (i : ℕ) ↦ if i ≤ m then v i else u (n + 1)) (m + 1) = u (n + 1)

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv :
  (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
        ℕ → α)
      (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
        (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) =
    u n
h'v :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
    (∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            i)))
hn : u n < u (n + 1)
⊢ StrictMonoOn.{0, u_1} (β := α) (fun (i : ℕ) ↦ if i ≤ m then v i else u (n + 1)) (Iic (m + 1)) ∧
    ∀ i ≤ m + 1, (fun (i : ℕ) ↦ if i ≤ m then v i else u (n + 1)) i ∈ s

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
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv :
  (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
        ℕ → α)
      (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
        (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) =
    u n
h'v :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
    (∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            i)))
hn : u n < u (n + 1)
succ :
  ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
    ∑ x ∈ Finset.range (m + 1),
      edist (f ((fun (i : ℕ) ↦ if i ≤ m then v i else u (n + 1)) (x + 1)))
        (f ((fun (i : ℕ) ↦ if i ≤ m then v i else u (n + 1)) x))
⊢ ∃ (a : ℕ) (a_1 : ℕ → α),
    a_1 a = u (n + 1) ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
          ∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x))

Tactic:
refine ⟨m + 1, fun i ↦ if i ≤ m then v i else u (n + 1), by simp,
            by grind [StrictMonoOn], ?_⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv :
  (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
        ℕ → α)
      (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
        (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) =
    u n
h'v :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
    (∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            i)))
hn : u n < u (n + 1)
succ :
  ∑ x ∈ Finset.range m, edist (f (v (x + 1))) (f (v x)) + edist (f (u (n + 1))) (f (v m)) =
    ∑ x ∈ Finset.range m, edist (f (if x < m then v (x + 1) else u (n + 1))) (f (if x ≤ m then v x else u (n + 1))) +
      edist (f (u (n + 1))) (f (v m))
⊢ ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
    ∑ x ∈ Finset.range (m + 1),
      edist (f ((fun (i : ℕ) ↦ if i ≤ m then v i else u (n + 1)) (x + 1)))
        (f ((fun (i : ℕ) ↦ if i ≤ m then v i else u (n + 1)) x))

Tactic:
simp only [h'v, ← hv, Order.add_one_le_iff, Finset.sum_range_succ, lt_self_iff_false,
            ↓reduceIte, le_refl]

Premises used: le_refl, Order.add_one_le_iff, lt_self_iff_false, reduceIte, Finset.sum_range_succ