exact_mod_cast unification leaves extra goal

[PatrickMassot]

import data.complex.basic

example : (((real.sqrt 2) / 2) : ℂ).im = 0 :=
begin
  exact_mod_cast complex.of_real_im _,
end

is expected to close the goal, but actually creates a new goal asking for a real number (any real number, not necessarily (real.sqrt 2 / 2) which is relevant here). Note that exact_mod_cast complex.of_real_im (real.sqrt 2 / 2) does work.

See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Exponential.20form.20of.20a.20complex.20number/near/214770391

[digama0]

Did you notice that by exact_mod_cast complex.of_real_im 37 also works? I don't think there is anything wrong with exact_mod_cast - the _ is not determined by exact_mod_cast.

[robertylewis]

The problem is that norm_cast closes the goal on its own which I don't think was ever expected in exact_mod_cast. The (\u r).im = 0 norm_cast lemmas are a little pathological.

[digama0]

You can also use exact_mod_cast rfl (which also makes it clear that plain norm_cast works). I don't see anything about exact_mod_cast behavior that needs changing here.

[PatrickMassot]

Oh, it didn't occur to me that norm_cast could do the job by itself! I guess I'll close this then.