-- Mathlib/Topology/UnitInterval.lean
/-- `Set.projIcc` is a contraction. -/
lemma _root_.Set.abs_projIcc_sub_projIcc : (|projIcc a b h c - projIcc a b h d| : α) ≤ |c - d|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ b ⊓ c - b ⊓ d ≤ c - d

Tactic:
refine ((le_abs_self _).trans <| abs_min_sub_min_le_max _ _ _ _).trans (max_le ?_ ?_)

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |b - b| ≤ c - d

case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |c - d| ≤ c - d

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : a ≤ b
this : ∀ {c d : α}, d ≤ c → |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |↑(projIcc a b h d) - ↑(projIcc a b h c)| ≤ |d - c|

Tactic:
exact this (le_of_not_le hdc)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : a ≤ b
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

Tactic:
wlog hdc : d ≤ c generalizing c d

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : a ≤ b
this : ∀ {c d : α}, d ≤ c → |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : d ≤ c
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : a ≤ b
this : ∀ {c d : α}, d ≤ c → |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

Tactic:
rw [abs_sub_comm, abs_sub_comm c]

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : a ≤ b
this : ∀ {c d : α}, d ≤ c → |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |↑(projIcc a b h d) - ↑(projIcc a b h c)| ≤ |d - c|

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |b - b| ≤ c - d

Tactic:
rwa [sub_self, abs_zero]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |c - d| ≤ c - d

Tactic:
exact (abs_eq_self.mpr hdc).le

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : d ≤ c
⊢ (fun a_1 => ↑a_1) (projIcc a b h c) - (fun a_1 => ↑a_1) (projIcc a b h d) ≤ c - d

Tactic:
rw [← sub_nonneg] at hdc

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ (fun a_1 => ↑a_1) (projIcc a b h c) - (fun a_1 => ↑a_1) (projIcc a b h d) ≤ c - d

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : d ≤ c
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

Tactic:
rw [abs_eq_self.2 (sub_nonneg.2 hdc), abs_eq_self.2 (sub_nonneg.2 <| monotone_projIcc h hdc)]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : d ≤ c
⊢ (fun a_1 => ↑a_1) (projIcc a b h c) - (fun a_1 => ↑a_1) (projIcc a b h d) ≤ c - d

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ (fun a_1 => ↑a_1) (projIcc a b h c) - (fun a_1 => ↑a_1) (projIcc a b h d) ≤ c - d

Tactic:
refine (max_sub_max_le_max _ _ _ _).trans (max_le (by rwa [sub_self]) ?_)

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ b ⊓ c - b ⊓ d ≤ c - d

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ a - a ≤ c - d

Tactic:
rwa [sub_self]

Result:
no goals