rw [(by linarith : x = a)]
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.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |a| ≤ max |a| |b|