Which tactic can solve it automatically?

Stream: general

[Jiatong Yang]

example (a b c : ℝ) (hc : c ≤ 0) (hab :  a ≤ b) : b*c ≤ a*c :=
begin
  exact mul_mono_nonpos hc hab,
end

[Heather Macbeth]

The little-known left/right option of docs#tactic.interactive.mono:

import data.real.basic

example (a b c : ℝ) (hc : c ≤ 0) (hab :  a ≤ b) : b*c ≤ a*c :=
by mono left

[Heather Macbeth]

Actually, you don't need the options, mono is ok.