Error: don't know how to synthesize placeholder

Stream: new members

[Vasily Ilin]

What is wrong here? I get "don't know how to synthesize placeholder" error.

example (a b c : ℝ) (hc : c ≤ 0) (hab :  a ≤ b) : b*c ≤ a*c :=
begin
  rw ← sub_nonneg,
  calc 0 ≤ (a-b)*c : mul_nonneg_of_nonpos_of_nonpos (by rwa sub_nonpos hab) hc,
     ... = a*c - b*c : by ring,
end

[Kevin Buzzard]

Can you post a #mwe? (All imports etc). It makes life easier for everyone else and it's the norm here.

[Vasily Ilin]

This is this file: https://github.com/leanprover-community/tutorials/blob/master/src/exercises/02_iff_if_and.lean. The only import is import data.real.basic as far as I can tell. So I guess the MWE is

import data.real.basic

example (a b c : ℝ) (hc : c ≤ 0) (hab :  a ≤ b) : b*c ≤ a*c :=
begin
  rw ← sub_nonneg,
  calc 0 ≤ (a-b)*c : mul_nonneg_of_nonpos_of_nonpos (by rwa sub_nonpos hab) hc,
     ... = a*c - b*c : by ring,
end

[Vasily Ilin]

Ah, it looks like it's the comma in calc... My bad!

[Vasily Ilin]

After deleting the comma and hab in rwas sub_nonpos hab everything works.

[Kevin Buzzard]

Yeah, sometimes the errors in calc mode can be pretty incomprehensible!