rw [(by linarith : x = 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|
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
⊢ |b| ≤ max |a| |b|