slow elaboration with bundled homomorphisms

Stream: general

[Yury G. Kudryashov]

here adding by simpa only [] makes elaboration much faster. I have no idea why. Here is the code:

lemma function.injective.has_sum_iff {g : γ → β} (hg : injective g)
  (hf : ∀ x ∉ set.range g, f x = 0) :
  has_sum (f ∘ g) a ↔ has_sum f a :=
by simpa only [] using function.embedding.has_sum_iff ⟨g, hg⟩ hf

This is a part of #3371.

[Yury G. Kudryashov]

another example

[Sebastien Gouezel]

Did you know that you can remove the [] in by simpa only []?