conv is slow

Stream: general

[Kenny Lau]

import data.complex.exponential

set_option profiler true

-- elaboration of test took 5.55s
lemma test (x : ℝ) : real.cos (x + x) * 0 = real.cos x * 0 :=
begin
  conv in (real.cos x) {}
end

[Mario Carneiro]

irreducible all the things?

[Kenny Lau]

does irreducible solve everything?

[Gabriel Ebner]

It should become faster when you finish the proof. conv implicitly does refl at the end.

[Gabriel Ebner]

Also, which mathlib version are you using? It's quite a bit faster for me:

elaboration of test took 22.1ms