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

Tactic:
congr 1
-- 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)
⊢ ∀ x ∈ Finset.range m,
    edist (f (v (x + 1))) (f (v x)) =
      edist (f (if x < m then v (x + 1) else u (n + 1))) (f (if x ≤ m then v x else u (n + 1)))

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

Tactic:
exact Finset.sum_congr rfl (by grind)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
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 n ∧
      Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, 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:
have : ∃ p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s },
        (p.2 : ℕ → α) p.1 = u n ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
        ∑ i ∈ Finset.range p.1, edist (f ((p.2 : ℕ → α) (i + 1))) (f ((p.2 : ℕ → α) i)) := by
      induction n with
      | zero => exact ⟨⟨0, ⟨u, by grind [StrictMonoOn], fun i hi ↦ u_mem _⟩⟩, by simp⟩
      | succ n ih =>
        rcases ih with ⟨⟨m, v, v_mono, v_mem⟩, hv, h'v⟩
        simp only [Finset.sum_range_succ, Sigma.exists, Subtype.exists, mem_Iic, exists_and_left,
          exists_prop]
        rcases (u_mono (Nat.le_add_right n 1)).eq_or_lt with hn | hn
        · simp only [← hn, edist_self, add_zero]
          exact ⟨m, v, hv, ⟨v_mono, v_mem⟩, h'v⟩
        · refine ⟨m + 1, fun i ↦ if i ≤ m then v i else u (n + 1), by simp,
            by grind [StrictMonoOn], ?_⟩
          simp only [h'v, ← hv, Order.add_one_le_iff, Finset.sum_range_succ, lt_self_iff_false,
            ↓reduceIte, le_refl]
          congr 1
          exact Finset.sum_congr rfl (by grind)
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }
hp :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, 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)))
a :
  LE.le (α := ℝ≥0∞)
    (∑ 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)))
    (⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ 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)))
⊢ LE.le (α := ℝ≥0∞)
    (∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i)))
    (⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ 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:
rw [hp]
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }
hp :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, 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)))
⊢ LE.le (α := ℝ≥0∞)
    (∑ 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)))
    (⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ 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:
apply le_iSup _ p

Premises used: le_iSup
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a :
  ∀ (i : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
    ∑ i_1 ∈ Finset.range (i.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (f
            ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i_1 + 1)))
          (f
            ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              i_1)) ≤
      eVariationOn f s
⊢ ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ 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)) ≤
    eVariationOn f s

Tactic:
apply iSup_le

Premises used: iSup_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
⊢ MonotoneOn.{0, u_1} (β := α)
    (↑(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 }) n
            (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))) :
      ℕ → α)
    (Iic
      (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 }) n
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))))

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
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
⊢ ∀
    i ≤
      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 }) n
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯)),
    (↑(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 }) n
                (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))) :
          ℕ → α)
        i ∈
      s

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
⊢ ∑
      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 }) n
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, 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 }) n
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, 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 }) n
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))) :
              ℕ → α)
            i)) ≤
    eVariationOn f s

Tactic:
apply sum_le_of_monotoneOn_Iic (by grind [MonotoneOn, StrictMonoOn]) (by grind)

Premises used: eVariationOn.sum_le_of_monotoneOn_Iic
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
apply :
  ∀ (i : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }),
    ∑ i_1 ∈ Finset.range i.1, edist (f ((↑i.2 : ℕ → α) (i_1 + 1))) (f ((↑i.2 : ℕ → α) i_1)) ≤ eVariationOn f s
⊢ eVariationOn f t ≤ eVariationOn f s

Tactic:
apply iSup_le _

Premises used: iSup_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
n : ℕ
u : ℕ → α
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → α) i)) ≤
    eVariationOn f s

Tactic:
sum_le hu fun i => hst (ut i)

Premises used: eVariationOn.sum_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
n : ℕ
u : ℕ → α
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → α) i)) ≤
    eVariationOn f s

Tactic:
exact sum_le hu fun i => hst (ut i)

Premises used: eVariationOn.sum_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
t : Set α
ht : t ⊆ s
⊢ BoundedVariationOn f t

Tactic:
ne_top_of_le_ne_top h (eVariationOn.mono f ht)

Premises used: ne_top_of_le_ne_top, eVariationOn.mono, BoundedVariationOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
⊢ LocallyBoundedVariationOn f s

Tactic:
fun _ _ _ _ =>
  h.mono inter_subset_left

Premises used: LocallyBoundedVariationOn, Set.inter_subset_left, BoundedVariationOn.mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f g : α → E
s : Set α
h : EqOn f g s
⊢ eVariationOn f s = eVariationOn g s

Tactic:
grind [eVariationOn]

Premises used: eVariationOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
inr :
  ∀ (this : ∀ {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : y ≤ x), edist (f x) (f y) ≤ eVariationOn f s) (hxy : ¬y ≤ x),
    edist (f x) (f y) ≤ eVariationOn f s
wlog : ∀ {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : y ≤ x), edist (f x) (f y) ≤ eVariationOn f s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
wlog hxy : y ≤ x generalizing x y
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : y ≤ x), edist (f x) (f y) ≤ eVariationOn f s
hxy : ¬y ≤ x
inr : edist (f y) (f x) ≤ eVariationOn f s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : y ≤ x), edist (f x) (f y) ≤ eVariationOn f s
hxy : ¬y ≤ x
⊢ edist (f y) (f x) ≤ eVariationOn f s

Tactic:
this hy hx (le_of_not_ge hxy)

Premises used: le_of_not_ge
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : y ≤ x), edist (f x) (f y) ≤ eVariationOn f s
hxy : ¬y ≤ x
⊢ edist (f y) (f x) ≤ eVariationOn f s

Tactic:
exact this hy hx (le_of_not_ge hxy)

Premises used: le_of_not_ge
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
u : ℕ → α := fun (n : ℕ) ↦ if n = 0 then y else x
⊢ Monotone u

Tactic:
have hu : Monotone u := monotone_nat_of_le_succ fun
  | 0 => hxy
  | (_ + 1) => le_rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
u : ℕ → α := fun (n : ℕ) ↦ if n = 0 then y else x
hu : Monotone u
⊢ ∀ (i : ℕ), u i ∈ s

Tactic:
have us : ∀ i, u i ∈ s := fun
  | 0 => hy
  | (_ + 1) => hx
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
u : ℕ → α := fun (n : ℕ) ↦ if n = 0 then y else x
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
simpa only [Finset.sum_range_one] using sum_le (n := 1) hu us

Premises used: Finset.sum_range_one, eVariationOn.sum_le