Slow inference of `CoeFun` for `MulHom`

Stream: mathlib4

[Emilie (Shad Amethyst)]

I'm noticing a significant slowdown in my proofs, caused by each MulAction.conj g written taking 200ms to elaborate, as lean struggles to find the CoeFun instance for MulAction.conj. As an example, the following theorem takes 2s on my machine to elab, but only 0.1s when adding a local instance as hint:

import Mathlib.Algebra.Group.Aut
import Mathlib.Data.Set.Pointwise.SMul
-- Seems to import enough things to cause a slowdown:
import Mathlib.GroupTheory.Exponent

open Pointwise

variable {G : Type*} [Group G]
variable (H : Subgroup G)

-- Uncomment the following to get a 20x speedup:
-- private instance {α β : Type*} [Monoid α] [Monoid β]: CoeFun (α →* β) fun _ => α → β := inferInstance

set_option trace.profiler true in
set_option profiler true in
theorem slow (g : G) : MulAut.conj g • H = H := by
  have h₁ := MulAut.conj g
  have h₂ := MulAut.conj g ^ 2
  have h₃ := MulAut.conj g ^ 3
  have h₄ := MulAut.conj g ^ 4
  have h₅ := MulAut.conj g ^ 5
  have h₆ := MulAut.conj g ^ 6
  have h₇ := MulAut.conj g ^ 7

  sorry

Should this instance hint be added to MulHom?

[Ruben Van de Velde]

I think this is what #8386 aims to fix

[Kevin Buzzard]

@Emilie (Shad Amethyst) you could check to see if #8386 does fix your problem, and if it does then add a note on the PR saying "hey this PR fixed my problem".

[Emilie (Shad Amethyst)]

I'll do that then, yeah; that PR also solves another issue that I have, which is that it's hard to compose together function classes like InfHomClass and MulActionHom — the usual way is to content oneself by choosing one bundled form