case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max a b - max c d ≤ max (abs (a - c)) (abs (b - d))

case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max c d - max a b ≤ max (abs (a - c)) (abs (b - d))
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ abs (max a b - max c d) ≤ max (abs (a - c)) (abs (b - d))
refine' abs_sub_le_iff.2 ⟨_, _⟩
no goals
case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max a b - max c d ≤ max (abs (a - c)) (abs (b - d))
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max c d - max a b ≤ max (abs (c - a)) (abs (d - b))
case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max c d - max a b ≤ max (abs (a - c)) (abs (b - d))
rw [abs_sub_comm a c, abs_sub_comm b d]
no goals
case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max c d - max a b ≤ max (abs (c - a)) (abs (d - b))
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))