awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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))) =
    eVariationOn f (s ∩ Icc (E 0) (E n)) + 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 + 1)))
have neg₁ : E 0 ≤ E n
Tactic: rw [← Icc_add_Icc (b := E n)]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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))) =
    eVariationOn f (s ∩ Icc (E 0) (E n)) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))
neg₁ : E 0 ≤ E n
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
have neg₂ : E n ≤ E (n + 1)
Tactic: rw [← Icc_add_Icc (b := E n)]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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))) =
    eVariationOn f (s ∩ Icc (E 0) (E n)) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))
neg₁ : E 0 ≤ E n
neg₂ : 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 + 1)))
have neg₃ : E n ∈ s
Tactic: rw [← Icc_add_Icc (b := E n)]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ E i ∈ s
have a₁ : i < n + 1
Tactic: apply hn
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 ∈ 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)))
have 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)))
Tactic: rw [← ih (by intros; apply hn <;> omega), Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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)))
⊢ ∑ 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)))
have 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)))
Tactic: rw [← ih (by intros; apply hn <;> omega), Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ E 0 ≤ E n
have neg : 0 ≤ n
Tactic: apply hE
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ E n ≤ E (n + 1)
have neg : n ≤ n + 1
Tactic: apply hE
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ E n ∈ s
have neg : 0 < n
Tactic: apply hn
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 n ∈ s
have neg₁ : n < n + 1
Tactic: apply hn
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
have 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))
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
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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))
⊢ ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
have 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)))
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
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 0 ≤ I i ∧ I i ≤ I n
have left : I 0 ≤ I i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ I 0 ≤ I i ∧ I i ≤ I n
have right : I i ≤ I n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 0 ≤ I i
have left : 0 ≤ i
Tactic: apply hI
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 i ≤ I n
have right : i ≤ n
Tactic: apply hI
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n : ℕ
⊢ ∑ i ∈ Finset.range n, eVariationOn f (Icc (I i) (I (i + 1))) = eVariationOn f (Icc (I 0) (I n))
have h : ∀ (i : ℕ) (hi : i ∈ Finset.range n), Icc (I i) (I (i + 1)) = Icc (I 0) (I n) ∩ Icc (I i) (I (i + 1))
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
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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))
⊢ ∑ i ∈ Finset.range n, eVariationOn f (Icc (I i) (I (i + 1))) = eVariationOn f (Icc (I 0) (I n))
have h₁ : Icc (I 0) (I n) = Icc (I 0) (I n) ∩ 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
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ Icc (I i) (I (i + 1)) = Icc (I 0) (I n) ∩ Icc (I i) (I (i + 1))
have h : Icc (I i) (I (i + 1)) ⊆ Icc (I 0) (I n)
Tactic: simp only [right_eq_inter]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ Icc (I i) (I (i + 1)) ⊆ Icc (I 0) (I n)
have h : I 0 ≤ I i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ Icc (I i) (I (i + 1)) ⊆ Icc (I 0) (I n)
have h₁ : I (i + 1) ≤ I n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 0 ≤ I i
have h : 0 ≤ i
Tactic: apply hI
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
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
⊢ 0 ≤ i
have hi₁ : i < n
Tactic: rw [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 (i + 1) ≤ I n
have h : i + 1 ≤ n
Tactic: apply hI
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
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 + 1 ≤ n
have hi₁ : i < n
Tactic: rw [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
have 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
Tactic: refine iSup_le ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ ∑ 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
have rw : ∑ j ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).1,
    edist
      ((f ∘ φ)
        ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).2 : ℕ → β)
          ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).1 - 1 - j + 1)))
      ((f ∘ φ)
        ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).2 : ℕ → β)
          ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).1 - 1 - j))) ≤
  eVariationOn f s
Tactic: rw [← Finset.sum_range_reflect]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
have refine : ∀ (x : ℕ) (hx : x ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).1),
  edist
      ((f ∘ φ)
        ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).2 : ℕ → β)
          ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).1 - 1 - x + 1)))
      ((f ∘ φ)
        ((↑(n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).2 : ℕ → β)
          ((n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).1 - 1 - x))) =
    edist
      (f
        ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) (fun (i : ℕ) ↦ φ (u (n - i))) sorry).2 :
            ℕ → α)
          (x + 1)))
      (f
        ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) (fun (i : ℕ) ↦ φ (u (n - i))) sorry).2 :
            ℕ → α)
          x))
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
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
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
⊢ 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))
have hx₁ : x < (n, Subtype.mk (p := fun (u : ℕ → β) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) u sorry).1
Tactic: rw [Finset.mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ 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))
have dsimp : edist (f (φ (u (n - 1 - x + 1)))) (f (φ (u (n - 1 - x)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
Tactic: dsimp only [Subtype.coe_mk, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ edist (f (φ (u (n - 1 - x + 1)))) (f (φ (u (n - 1 - x)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
have rw : edist (f (φ (u (n - 1 - x)))) (f (φ (u (n - 1 - x + 1)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
Tactic: rw [edist_comm]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ edist (f (φ (u (n - 1 - x)))) (f (φ (u (n - 1 - x + 1)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
have e_a : n - 1 - x = n - (x + 1)
Tactic: congr 4
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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)
⊢ edist (f (φ (u (n - 1 - x)))) (f (φ (u (n - 1 - x + 1)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
have e_a₁ : n - 1 - x + 1 = n - x
Tactic: congr 4
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)
have apply : eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
Tactic: apply le_antisymm (comp_le_of_monotoneOn f φ hφ (mapsTo_image φ t))
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
have inl : IsEmpty β → eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
have inr : Nonempty β → eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
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
⊢ eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
have ψφs : EqOn (φ ∘ ψ) id (φ '' t)
Tactic: have ψφs : EqOn (φ ∘ ψ) id (φ '' t) := (surjOn_image φ t).rightInvOn_invFunOn