awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
i : ℕ
h : 0 < i
h_1 : i < n
a : 0 < i
a₁ : i < n + 1
⊢ E i ∈ s

Tactic:
apply hn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
i : ℕ
h : 0 < i
h_1 : i < n
⊢ 0 < i

Tactic:
omega
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
i : ℕ
h : 0 < i
h_1 : i < n
⊢ i < n + 1

Tactic:
omega
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
neg :
  ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) =
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))
neg₁ neg₂ :
  ∑ x ∈ Finset.range n, eVariationOn f (s ∩ Icc (E x) (E (x + 1))) + eVariationOn f (s ∩ Icc (E n) (E (n + 1))) =
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) =
    eVariationOn f (s ∩ Icc (E 0) (E n)) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))

Tactic:
rw [← ih (by intros; apply hn <;> omega), Finset.sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
neg : 0 ≤ n
⊢ E 0 ≤ E n

Tactic:
apply hE
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ 0 ≤ n

Tactic:
lia
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
neg : n ≤ n + 1
⊢ E n ≤ E (n + 1)

Tactic:
apply hE
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ n ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
neg : 0 < n
neg₁ : n < n + 1
⊢ E n ∈ s

Tactic:
apply hn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ 0 < n

Tactic:
omega
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ n < n + 1

Tactic:
omega
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s
zero :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < 0 → E i ∈ s),
    ∑ i ∈ Finset.range 0, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E 0))
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
        ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n)))
    (hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s),
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
⊢ ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))

Tactic:
induction n with
  | zero => simp [eVariationOn.subsingleton f Subsingleton.inter_singleton]
  | succ n ih =>
    by_cases hn₀ : n = 0
    · simp [hn₀]
    rw [← Icc_add_Icc (b := E n)]
    · rw [← ih (by intros; apply hn <;> omega), Finset.sum_range_succ]
    · apply hE; lia
    · apply hE; lia
    · apply hn <;> omega

Premises used: eVariationOn.subsingleton, Set.Subsingleton.inter_singleton, eVariationOn.Icc_add_Icc, Finset.sum_range_succ
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
h : 0 < i
h_1 : i < n
left : I 0 ≤ I i
right : I i ≤ I n
⊢ I 0 ≤ I i ∧ I i ≤ I n

Tactic:
constructor
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
h : 0 < i
h_1 : i < n
left : 0 ≤ i
⊢ I 0 ≤ I i

Tactic:
apply hI
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
h : 0 < i
h_1 : i < n
⊢ 0 ≤ i

Tactic:
lia
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
h : 0 < i
h_1 : i < n
right : i ≤ n
⊢ I i ≤ I n

Tactic:
apply hI
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
h : 0 < i
h_1 : i < n
⊢ i ≤ n

Tactic:
lia
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n : ℕ
h : ∀ (i : ℕ) (hi : i ∈ Finset.range n), Icc (I i) (I (i + 1)) = Icc (I 0) (I n) ∩ Icc (I i) (I (i + 1))
h₁ : Icc (I 0) (I n) = Icc (I 0) (I n) ∩ Icc (I 0) (I n)
⊢ ∑ i ∈ Finset.range n, eVariationOn f (Icc (I i) (I (i + 1))) = eVariationOn f (Icc (I 0) (I n))

Tactic:
convert!
      sum f hI (s := Icc (I 0) (I n)) (n := n)
        (hn := by intros; rw [mem_Icc]; constructor <;> (apply hI; lia))
    with i hi

Premises used: eVariationOn.sum
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i ∈ Finset.range n
h : Icc (I i) (I (i + 1)) ⊆ Icc (I 0) (I n)
⊢ Icc (I i) (I (i + 1)) = Icc (I 0) (I n) ∩ Icc (I i) (I (i + 1))

Tactic:
simp only [right_eq_inter]

Premises used: Set.right_eq_inter
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i ∈ Finset.range n
h : I 0 ≤ I i
h₁ : I (i + 1) ≤ I n
⊢ Icc (I i) (I (i + 1)) ⊆ Icc (I 0) (I n)

Tactic:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i ∈ Finset.range n
h : 0 ≤ i
⊢ I 0 ≤ I i

Tactic:
apply hI
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i ∈ Finset.range n
⊢ i < n

Tactic:
rw [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i < n
⊢ 0 ≤ i

Tactic:
lia
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i ∈ Finset.range n
h : i + 1 ≤ n
⊢ I (i + 1) ≤ I n

Tactic:
apply hI
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i < n
⊢ i + 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n : ℕ
⊢ Icc (I 0) (I n) = Icc (I 0) (I n) ∩ Icc (I 0) (I n)

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : MonotoneOn φ t
φst : MapsTo φ t s
⊢ eVariationOn (f ∘ φ) t ≤ eVariationOn f s

Tactic:
iSup_le fun ⟨n, u, hu, ut⟩ =>
    le_iSup_of_le ⟨n, φ ∘ u, fun x y xy => hφ (ut x) (ut y) (hu xy), fun i => φst (ut i)⟩ le_rfl

Premises used: _private.0.eVariationOn.comp_le_of_monotoneOn.match_1, le_rfl, Function.comp, Prod.mk, LE.le, eVariationOn, Prod.fst, Subtype.mk, Finset.range, HAdd.hAdd, le_iSup_of_le, And.intro, iSup_le, EDist.edist, OfNat.ofNat, Subtype.val, Prod.snd, Finset.sum
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
⊢ eVariationOn (f ∘ φ) t ≤ eVariationOn f s

Tactic:
iSup_le ?_

Premises used: eVariationOn, iSup_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
refine :
  ∀ (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:
refine 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
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
rw :
  ∑ j ∈ 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 : ℕ → β)
            ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - j + 1)))
        ((f ∘ φ)
          ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → β)
            ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - j))) ≤
    eVariationOn f s
⊢ ∑ 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:
rw [← Finset.sum_range_reflect]

Premises used: Finset.sum_range_reflect
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
⊢ ∑ j ∈ 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 : ℕ → β)
            ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - j + 1)))
        ((f ∘ φ)
          ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → β)
            ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - j))) ≤
    eVariationOn f s

Tactic:
(Finset.sum_congr rfl fun x hx => ?_).trans_le <| le_iSup_of_le
    ⟨n, fun i => φ (u <| n - i), fun x y xy => hφ (ut _) (ut _) (hu <| Nat.sub_le_sub_left xy n),
      fun i => φst (ut _)⟩
    le_rfl

Premises used: Nat.sub_le_sub_left, le_rfl, HSub.hSub, Prod.mk, Eq.trans_le, Subtype.mk, le_iSup_of_le, And.intro, Finset.sum_congr, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
refine :
  ∀ (x : ℕ) (hx : x ∈ 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 : ℕ → β)
            ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - x + 1)))
        ((f ∘ φ)
          ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → β)
            ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - x))) =
      edist
        (f
          ((↑(n,
                    Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) (fun (i : ℕ) ↦ φ (u (n - i)))
                      ⋯).2 :
              ℕ → α)
            (x + 1)))
        (f
          ((↑(n,
                    Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) (fun (i : ℕ) ↦ φ (u (n - i)))
                      ⋯).2 :
              ℕ → α)
            x))
⊢ ∑ j ∈ 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 : ℕ → β)
            ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - j + 1)))
        ((f ∘ φ)
          ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → β)
            ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - j))) ≤
    eVariationOn f s

Tactic:
refine (Finset.sum_congr rfl fun x hx => ?_).trans_le <| le_iSup_of_le
    ⟨n, fun i => φ (u <| n - i), fun x y xy => hφ (ut _) (ut _) (hu <| Nat.sub_le_sub_left xy n),
      fun i => φst (ut _)⟩
    le_rfl

Premises used: le_rfl, Eq.trans_le, le_iSup_of_le, Finset.sum_congr, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1
⊢ x < (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1

Tactic:
rw [Finset.mem_range] at hx

Premises used: Finset.mem_range
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1
dsimp : edist (f (φ (u (n - 1 - x + 1)))) (f (φ (u (n - 1 - x)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
⊢ edist
      ((f ∘ φ)
        ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → β)
          ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - x + 1)))
      ((f ∘ φ)
        ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).2 : ℕ → β)
          ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1 - 1 - x))) =
    edist
      (f
        ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) (fun (i : ℕ) ↦ φ (u (n - i))) ⋯).2 :
            ℕ → α)
          (x + 1)))
      (f
        ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) (fun (i : ℕ) ↦ φ (u (n - i))) ⋯).2 :
            ℕ → α)
          x))

Tactic:
dsimp only [Subtype.coe_mk, Function.comp_apply]

Premises used: Subtype.coe_mk, Function.comp_apply
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1
rw : edist (f (φ (u (n - 1 - x)))) (f (φ (u (n - 1 - x + 1)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
⊢ edist (f (φ (u (n - 1 - x + 1)))) (f (φ (u (n - 1 - x)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))

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
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1
e_a : n - 1 - x = n - (x + 1)
e_a₁ : n - 1 - x + 1 = n - x
⊢ edist (f (φ (u (n - 1 - x)))) (f (φ (u (n - 1 - x + 1)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))

Tactic:
congr 4
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1
⊢ n - 1 - x = n - (x + 1)

Tactic:
lia
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u ⋯).1
⊢ n - 1 - x + 1 = n - x

Tactic:
lia
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
apply : eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
⊢ eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)

Tactic:
apply le_antisymm (comp_le_of_monotoneOn f φ hφ (mapsTo_image φ t))

Premises used: Set.mapsTo_image, le_antisymm, eVariationOn.comp_le_of_monotoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
inl : IsEmpty β → eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
inr : Nonempty β → eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
⊢ eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
cases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
h : IsEmpty β
⊢ eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
simp [Set.eq_empty_of_isEmpty]

Premises used: Set.eq_empty_of_isEmpty
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
⊢ EqOn (φ ∘ ψ) id (φ '' t)

Tactic:
have ψφs : EqOn (φ ∘ ψ) id (φ '' t) := (surjOn_image φ t).rightInvOn_invFunOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
⊢ MapsTo ψ (φ '' t) t

Tactic:
have ψts : MapsTo ψ (φ '' t) t := (surjOn_image φ t).mapsTo_invFunOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
β : Type u_3
inst_2 : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
h : Nonempty β
ψ : (b : α) → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo ψ (φ '' t) t
⊢ MonotoneOn ψ (φ '' t)

Tactic:
have hψ : MonotoneOn ψ (φ '' t) := Function.monotoneOn_of_rightInvOn_of_mapsTo hφ ψφs ψts