-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem add {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

Proof state:
case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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

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]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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

Tactic:
symm

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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

Proof state:
case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y : α
_xs : x ∈ s
_ys : y ∈ s
⊢ variationOnFromTo f s x y + variationOnFromTo f s y x = 0

Tactic:
simp only [variationOnFromTo.eq_neg_swap f s y x, Subtype.coe_mk, add_neg_cancel,
  forall_true_left]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ ∀ {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:
rintro x y z xy yz xs ys zs

Result:
case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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

Proof state:
case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ ∀ {a b : α}, (fun x => x ∈ s) a → (fun x => x ∈ s) b → variationOnFromTo f s a b + variationOnFromTo f s b a = 0

Tactic:
rintro x y _xs _ys

Result:
case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y : α
_xs : x ∈ s
_ys : y ∈ s
⊢ variationOnFromTo f s x y + variationOnFromTo f s y x = 0