cases' hx.1 with x_ge_a x_ge_b <;> cases' hx.2 with x_le_a x_le_b
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
⊢ |x| ≤ max |a| |b|
case inl.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|

case inl.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|

case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|

case inr.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|