awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
⊢ eVariationOn f (s ∩ Icc a b) ≤ ENNReal.ofReal (f b - f a)
have apply : ∀ (i : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b }),
  ∑ i_1 ∈ Finset.range i.1, edist (f ((↑i.2 : ℕ → α) (i_1 + 1))) (f ((↑i.2 : ℕ → α) i_1)) ≤ ENNReal.ofReal (f b - f a)
Tactic: apply iSup_le _
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)))
have refine : ∀ (i : ℕ) (hi : i ∈ Finset.range n), edist (f (u (i + 1))) (f (u i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))
Tactic: refine Finset.sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i ∈ Finset.range n
⊢ edist (f (u (i + 1))) (f (u i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))
have hi₁ : i < n
Tactic: simp only [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i < n
⊢ edist (f (u (i + 1))) (f (u i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))
have rw : 0 ≤ f (u (i + 1)) - f (u i)
Tactic: rw [edist_dist, Real.dist_eq, abs_of_nonneg]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
    ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i)))
have rw : ∀ i ∈ Finset.range n, 0 ≤ f (u (i + 1)) - f (u i)
Tactic: rw [ENNReal.ofReal_sum_of_nonneg]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) = ENNReal.ofReal (f (u n) - f (u 0))
have rw : ENNReal.ofReal (f (u n) - f (u 0)) = ENNReal.ofReal (f (u n) - f (u 0))
Tactic: rw [Finset.sum_range_sub fun i => f (u i)]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ENNReal.ofReal (f (u n) - f (u 0)) ≤ ENNReal.ofReal (f b - f a)
have h : f (u n) - f (u 0) ≤ f b - f a
Tactic: apply ENNReal.ofReal_le_ofReal
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).1,
      edist
        (f
          ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) i)) ≤
    ENNReal.ofReal (f b - f a)
have i : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
  (∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)))
Tactic: calc
    (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
        ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) := by
      refine Finset.sum_congr rfl fun i hi => ?_
      simp only [Finset.mem_range] at hi
      rw [edist_dist, Real.dist_eq, abs_of_nonneg]
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) := by
      rw [ENNReal.ofReal_sum_of_nonneg]
      intro i _
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (f (u n) - f (u 0)) := by rw [Finset.sum_range_sub fun i => f (u i)]
    _ ≤ ENNReal.ofReal (f b - f a) := by
      apply ENNReal.ofReal_le_ofReal
      exact sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)))
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).1,
      edist
        (f
          ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) i)) ≤
    ENNReal.ofReal (f b - f a)
have i₁ : ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
  ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i)))
Tactic: calc
    (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
        ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) := by
      refine Finset.sum_congr rfl fun i hi => ?_
      simp only [Finset.mem_range] at hi
      rw [edist_dist, Real.dist_eq, abs_of_nonneg]
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) := by
      rw [ENNReal.ofReal_sum_of_nonneg]
      intro i _
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (f (u n) - f (u 0)) := by rw [Finset.sum_range_sub fun i => f (u i)]
    _ ≤ ENNReal.ofReal (f b - f a) := by
      apply ENNReal.ofReal_le_ofReal
      exact sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)))
i₁ :
  ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
    ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i)))
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).1,
      edist
        (f
          ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) i)) ≤
    ENNReal.ofReal (f b - f a)
have i₂ : ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) = ENNReal.ofReal (f (u n) - f (u 0))
Tactic: calc
    (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
        ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) := by
      refine Finset.sum_congr rfl fun i hi => ?_
      simp only [Finset.mem_range] at hi
      rw [edist_dist, Real.dist_eq, abs_of_nonneg]
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) := by
      rw [ENNReal.ofReal_sum_of_nonneg]
      intro i _
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (f (u n) - f (u 0)) := by rw [Finset.sum_range_sub fun i => f (u i)]
    _ ≤ ENNReal.ofReal (f b - f a) := by
      apply ENNReal.ofReal_le_ofReal
      exact sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)))
i₁ :
  ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
    ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i)))
i₂ : ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) = ENNReal.ofReal (f (u n) - f (u 0))
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).1,
      edist
        (f
          ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b) u ⋯).2 : ℕ → α) i)) ≤
    ENNReal.ofReal (f b - f a)
have i₃ : ENNReal.ofReal (f (u n) - f (u 0)) ≤ ENNReal.ofReal (f b - f a)
Tactic: calc
    (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
        ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) := by
      refine Finset.sum_congr rfl fun i hi => ?_
      simp only [Finset.mem_range] at hi
      rw [edist_dist, Real.dist_eq, abs_of_nonneg]
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) := by
      rw [ENNReal.ofReal_sum_of_nonneg]
      intro i _
      exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
    _ = ENNReal.ofReal (f (u n) - f (u 0)) := by rw [Finset.sum_range_sub fun i => f (u i)]
    _ ≤ ENNReal.ofReal (f b - f a) := by
      apply ENNReal.ofReal_le_ofReal
      exact sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)
-- 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
s : Set α
a : α
⊢ (if a ≤ a then (eVariationOn f (s ∩ Icc a a)).toReal else -(eVariationOn f (s ∩ Icc a a)).toReal) = 0
have hs : (s ∩ {a}).Subsingleton
Tactic: rw [if_pos le_rfl, Icc_self, eVariationOn.subsingleton, ENNReal.toReal_zero]
-- 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
s : Set α
a b : α
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a
have inl : ∀ (ab : a < b), variationOnFromTo f s a b = -variationOnFromTo f s b a
Tactic: rcases lt_trichotomy a b with (ab | rfl | ba)
-- 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
s : Set α
a b : α
inl : ∀ (ab : a < b), variationOnFromTo f s a b = -variationOnFromTo f s b a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a
have inr : variationOnFromTo f s a a = -variationOnFromTo f s a a
Tactic: rcases lt_trichotomy a b with (ab | rfl | ba)
Cleared hypotheses: b
-- 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
s : Set α
a b : α
inl : ∀ (ab : a < b), variationOnFromTo f s a b = -variationOnFromTo f s b a
inr : variationOnFromTo f s a a = -variationOnFromTo f s a a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a
have inr₁ : ∀ (ba : b < a), variationOnFromTo f s a b = -variationOnFromTo f s b a
Tactic: rcases lt_trichotomy a b with (ab | rfl | ba)
-- 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
s : Set α
a b : α
h : b ≤ a
⊢ variationOnFromTo f s a b ≤ 0
have rw : -variationOnFromTo f s b a ≤ 0
Tactic: rw [variationOnFromTo.eq_neg_swap]
-- 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
s : Set α
hf : BoundedVariationOn f s
a b : α
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
have pos : ∀ (hab : a ≤ b), |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
Tactic: by_cases hab : a ≤ b
-- 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
s : Set α
hf : BoundedVariationOn f s
a b : α
pos : ∀ (hab : a ≤ b), |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
have neg : ∀ (hab : ¬a ≤ b), |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
Tactic: by_cases hab : a ≤ b
-- 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
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : a ≤ b
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
have pos : (eVariationOn f (s ∩ Icc a b)).toReal ≤ (eVariationOn f s).toReal
Tactic: simp only [variationOnFromTo, hab, ↓reduceIte, ENNReal.abs_toReal]
-- 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
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : ¬a ≤ b
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
have neg : (eVariationOn f (s ∩ Icc b a)).toReal ≤ (eVariationOn f s).toReal
Tactic: simp only [variationOnFromTo, hab, ↓reduceIte, abs_neg, ENNReal.abs_toReal]
-- 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
s : Set α
a b : α
h : b ≤ a
⊢ variationOnFromTo f s a b = -(eVariationOn f (s ∩ Icc b a)).toReal
have rw : -variationOnFromTo f s b a = -(eVariationOn f (s ∩ Icc b a)).toReal
Tactic: rw [variationOnFromTo.eq_neg_swap, neg_inj, variationOnFromTo.eq_of_le f s h]
-- 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
s : Set α
a b : α
h : b ≤ a
rw : -variationOnFromTo f s b a = -(eVariationOn f (s ∩ Icc b a)).toReal
⊢ variationOnFromTo f s a b = -(eVariationOn f (s ∩ Icc b a)).toReal
have rw₁ : variationOnFromTo f s b a = (eVariationOn f (s ∩ Icc b a)).toReal
Tactic: rw [variationOnFromTo.eq_neg_swap, neg_inj, variationOnFromTo.eq_of_le f s h]
-- 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
s : Set α
a b : α
h : b ≤ a
rw : -variationOnFromTo f s b a = -(eVariationOn f (s ∩ Icc b a)).toReal
rw₁ : variationOnFromTo f s b a = (eVariationOn f (s ∩ Icc b a)).toReal
⊢ variationOnFromTo f s a b = -(eVariationOn f (s ∩ Icc b a)).toReal
have rw₂ : (eVariationOn f (s ∩ Icc b a)).toReal = (eVariationOn f (s ∩ Icc b a)).toReal
Tactic: rw [variationOnFromTo.eq_neg_swap, neg_inj, variationOnFromTo.eq_of_le f s h]
-- 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
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a b + variationOnFromTo f s b c = variationOnFromTo f s a c
have symm : variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c
Tactic: symm
-- 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
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c
have refine_1 : ∀ {a b : α},
  (fun (x : α) ↦ x ∈ s) a → (fun (x : α) ↦ x ∈ s) b → variationOnFromTo f s a b + variationOnFromTo f s b a = 0
Tactic: refine additive_of_total (· ≤ · : α → α → Prop) (variationOnFromTo f s) (· ∈ s) ?_ ?_ ha hb hc
-- 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
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
refine_1 :
  ∀ {a b : α},
    (fun (x : α) ↦ x ∈ s) a → (fun (x : α) ↦ x ∈ s) b → variationOnFromTo f s a b + variationOnFromTo f s b a = 0
⊢ variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c
have refine_2 : ∀ {a b c : α},
  (fun (x1 x2 : α) ↦ x1 ≤ x2) a b →
    (fun (x1 x2 : α) ↦ x1 ≤ x2) b c →
      (fun (x : α) ↦ x ∈ s) a →
        (fun (x : α) ↦ x ∈ s) b →
          (fun (x : α) ↦ x ∈ s) c → variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c
Tactic: refine additive_of_total (· ≤ · : α → α → Prop) (variationOnFromTo f s) (· ∈ s) ?_ ?_ ha hb hc
-- 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
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y z : α
xy : x ≤ y
yz : y ≤ z
xs : x ∈ s
ys : y ∈ s
zs : z ∈ s
⊢ variationOnFromTo f s x z = variationOnFromTo f s x y + variationOnFromTo f s y z
have refine_2 : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + variationOnFromTo f s y z
Tactic: rw [variationOnFromTo.eq_of_le f s xy, variationOnFromTo.eq_of_le f s yz,
      variationOnFromTo.eq_of_le f s (xy.trans yz),
      ← ENNReal.toReal_add (hf x y xs ys) (hf y z ys zs), eVariationOn.Icc_add_Icc f xy yz ys]
-- 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
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y z : α
xy : x ≤ y
yz : y ≤ z
xs : x ∈ s
ys : y ∈ s
zs : z ∈ s
refine_2 : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + variationOnFromTo f s y z
⊢ variationOnFromTo f s x z = variationOnFromTo f s x y + variationOnFromTo f s y z
have refine_2₁ : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
Tactic: rw [variationOnFromTo.eq_of_le f s xy, variationOnFromTo.eq_of_le f s yz,
      variationOnFromTo.eq_of_le f s (xy.trans yz),
      ← ENNReal.toReal_add (hf x y xs ys) (hf y z ys zs), eVariationOn.Icc_add_Icc f xy yz ys]
-- 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
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y z : α
xy : x ≤ y
yz : y ≤ z
xs : x ∈ s
ys : y ∈ s
zs : z ∈ s
refine_2 : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + variationOnFromTo f s y z
refine_2₁ : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
⊢ variationOnFromTo f s x z = variationOnFromTo f s x y + variationOnFromTo f s y z
have refine_2₂ : (eVariationOn f (s ∩ Icc x z)).toReal = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
Tactic: rw [variationOnFromTo.eq_of_le f s xy, variationOnFromTo.eq_of_le f s yz,
      variationOnFromTo.eq_of_le f s (xy.trans yz),
      ← ENNReal.toReal_add (hf x y xs ys) (hf y z ys zs), eVariationOn.Icc_add_Icc f xy yz ys]
-- 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
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y z : α
xy : x ≤ y
yz : y ≤ z
xs : x ∈ s
ys : y ∈ s
zs : z ∈ s
refine_2 : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + variationOnFromTo f s y z
refine_2₁ : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
refine_2₂ :
  (eVariationOn f (s ∩ Icc x z)).toReal = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
⊢ variationOnFromTo f s x z = variationOnFromTo f s x y + variationOnFromTo f s y z
have refine_2₃ : (eVariationOn f (s ∩ Icc x z)).toReal = (eVariationOn f (s ∩ Icc x y) + eVariationOn f (s ∩ Icc y z)).toReal
Tactic: rw [variationOnFromTo.eq_of_le f s xy, variationOnFromTo.eq_of_le f s yz,
      variationOnFromTo.eq_of_le f s (xy.trans yz),
      ← ENNReal.toReal_add (hf x y xs ys) (hf y z ys zs), eVariationOn.Icc_add_Icc f xy yz ys]
-- 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
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y z : α
xy : x ≤ y
yz : y ≤ z
xs : x ∈ s
ys : y ∈ s
zs : z ∈ s
refine_2 : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + variationOnFromTo f s y z
refine_2₁ : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
refine_2₂ :
  (eVariationOn f (s ∩ Icc x z)).toReal = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
refine_2₃ : (eVariationOn f (s ∩ Icc x z)).toReal = (eVariationOn f (s ∩ Icc x y) + eVariationOn f (s ∩ Icc y z)).toReal
⊢ variationOnFromTo f s x z = variationOnFromTo f s x y + variationOnFromTo f s y z
have refine_2₄ : (eVariationOn f (s ∩ Icc x z)).toReal = (eVariationOn f (s ∩ Icc x z)).toReal
Tactic: rw [variationOnFromTo.eq_of_le f s xy, variationOnFromTo.eq_of_le f s yz,
      variationOnFromTo.eq_of_le f s (xy.trans yz),
      ← ENNReal.toReal_add (hf x y xs ys) (hf y z ys zs), eVariationOn.Icc_add_Icc f xy yz ys]
-- 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
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
⊢ edist (f a) (f b) = 0
have inr : ∀
  (this :
    ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_2 : PseudoEMetricSpace E] {f : α → E} {s : Set α}
      (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : variationOnFromTo f s a b = 0)
      (h' : a ≤ b), edist (f a) (f b) = 0)
  (h' : ¬a ≤ b), edist (f a) (f b) = 0
Tactic: wlog h' : a ≤ b