Slow `refine` for `ZMod`

Stream: mathlib4

[Gareth Ma]

import Mathlib.Tactic

set_option profiler true
set_option trace.profiler true

open ZMod

/- 12.2s -/
example : addOrderOf (3 : ZMod 1200) = 400 := by
  change addOrderOf ↑3 = 400

/- 0.01s -/
example : (3 : ZMod 12000) = ↑3 := rfl

[Gareth Ma]

Relevant example:

/-
tactic execution of Mathlib.Tactic.convert took 6.26s
type checking took 5.77s
-/
example : addOrderOf (3 : ZMod 12000) = 4000 := by
  convert addOrderOf_coe' _ _
  -- simp

What's happening with type checking? :thinking:

[Alex J. Best]

import Mathlib.Tactic

set_option profiler true
set_option trace.profiler true

open ZMod

example : addOrderOf (3 : ZMod 12000) = 4000 := by
  convert addOrderOf_coe' _ _
  simp

takes 0.1s in the web editor

[Gareth Ma]

Uhhh I must have messed something up then. Is the first example still there though?

[Gareth Ma]

Is there any progress on this?