-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem edist_le (f : α → E) {s : Set α} {x y : α} (hx : x ∈ s) (hy : y ∈ s) :
    edist (f x) (f y) ≤ eVariationOn f s

Proof state:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α}, x ∈ s → y ∈ s → 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_le hxy)

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α}, x ∈ s → y ∈ s → y ≤ x → edist (f x) (f y) ≤ eVariationOn f s
hxy : ¬y ≤ x
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
rw [edist_comm]

Result:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α}, x ∈ s → y ∈ s → y ≤ x → edist (f x) (f y) ≤ eVariationOn f s
hxy : ¬y ≤ x
⊢ edist (f y) (f x) ≤ eVariationOn f s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
have hu : Monotone u := monotone_nat_of_le_succ fun
| 0 => hxy
| (_ + 1) => le_rfl

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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
⊢ edist (f x) (f y) ≤ eVariationOn f s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
have us : ∀ i, u i ∈ s := fun
| 0 => hy
| (_ + 1) => hx

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

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

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
wlog hxy : y ≤ x generalizing x y

Result:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α}, x ∈ s → y ∈ s → y ≤ x → edist (f x) (f y) ≤ eVariationOn f s
hxy : ¬y ≤ x
⊢ edist (f x) (f y) ≤ eVariationOn f s

α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
⊢ edist (f x) (f y) ≤ eVariationOn f s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
let u : ℕ → α := fun n => if n = 0 then y else x

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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
⊢ edist (f x) (f y) ≤ eVariationOn f s