Intermediate `have` speeds up elaboration

Stream: general

[Oliver Nash]

I am surprised by the difference in elaboration speed in smooth.div_slow and smooth.div_fast in the below:

import geometry.manifold.algebra.lie_group

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
          {H : Type*} [topological_space H]
          {E : Type*} [normed_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H}
          {G : Type*} [topological_space G] [charted_space H G] [group G] [lie_group I G]
          {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
          {H' : Type*} [topological_space H'] {I' : model_with_corners 𝕜 E' H'}
          {M : Type*} [topological_space M] [charted_space H' M]

set_option profiler true

@[to_additive]
lemma smooth.div_slow {f g : M → G} -- elaboration of smooth.div took 6.38s
  (hf : smooth I' I f) (hg : smooth I' I g) : smooth I' I (f / g) :=
begin
  rw div_eq_mul_inv,
  exact (smooth_mul I).comp (hf.prod_mk hg.inv),
end

lemma smooth.div_fast {f g : M → G} -- elaboration of smooth.div took 79.1ms
  (hf : smooth I' I f) (hg : smooth I' I g) : smooth I' I (f / g) :=
begin
  rw div_eq_mul_inv,
  have h := (smooth_mul I).comp (hf.prod_mk hg.inv),
  exact h,
end

[Oliver Nash]

By introducing a pointless intermediate have, elaboration speeds up by a factor of 80! Is there an explanation for this and/or a guide for how to deal with this?

[Kevin Buzzard]

Does exact ((smooth_mul I).comp (hf.prod_mk hg.inv) : _) make it fast?

[Oliver Nash]

Yes!

[Oliver Nash]

131ms elaboration time.

[Kevin Buzzard]

I've seen this trick before :-)

[Oliver Nash]

This is black magic to me. I'd love if there was a thread I could read about it somewhere.

[Johan Commelin]

@Oliver Nash When you do exact some_expr, Lean will check that this expression has the expected type.

[Kevin Buzzard]

The exact version attempts to elaborate (smooth_mul I).comp (hf.prod_mk hg.inv) with the type of the goal, which apparently gets the elaborator confused. The have h version elaborates it with whatever type comes out, and then the exact attempts to make that type equal to the goal, which sometimes produces very different results!

[Eric Wieser]

Adding the : _) means roughly "elaborate this expression as much as possible before continuing"

[Johan Commelin]

But with have or the (some_expr : _) variant, you ask Lean to infer the type, and then check this type is defeq to what Lean expects.

[Johan Commelin]

And the order in which the infer and check happen, matters a lot for speed.

[Oliver Nash]

OK I more or less understand. Library note?

[Oliver Nash]

I should also say: thanks. I didn't expect a barrage of such helpful answers so quickly :-)

[Johan Commelin]

I wouldn't be enough of an expert to write more than the two lines I just wrote. But someone who actually understands type theory and Lean can maybe help us out (-;

[Oliver Nash]

Maybe I'll create a library note PR and tag someone on GH so that they can actually fill it in with a bit more?