Why is `coe_mk` no longer needed?

Stream: mathlib4

[Antoine Labelle]

I need help fixing the map_mul' field in conj in #1111. In the mathlib3 proof, the simp tactic uses mul_equiv.coe_mk to simplify a big mess where a mul_equiv defined explicitly is applied to an argument. In mathlib4, the lemma mul_equiv.coe_mk doesn't exist, in fact, there is a porting note saying that it is no longer needed. However the big mess doesn't get simplified by the simp anymore and the proof of map_mul' now fails. What is supposed to be the alternative to mul_equiv.coe_mk that makes this proof work?

[Antoine Labelle]

In fact the simp now gives the following error :

tactic 'simp' failed, nested error:
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

[Mario Carneiro]

if simp says that then you marked something as a simp lemma (globally or in the invocation) which is causing it to loop

[Antoine Labelle]

Hmm, well if I replace simp [mul_assoc]with simp only [mul_assoc, eq_self_iff_true, MulAut.mul_apply, mul_left_inj](which is what simp? [mul_assoc]generate in mathlib3 minus mul_equiv.coe_mk) I no longer have this deterministic timeout error but the big mess still doesn't get simplified.

[Kevin Buzzard]

Is it one of those situations where coe_mk used to be syntactic tautology but now we have funlike and it isn't?

[Kevin Buzzard]

If you add

@[simp] theorem _root_.MulEquiv.coe_mk {M N : Type _} [Mul M] [Mul N] (e : M ≃ N) (h) :
    ⇑(_root_.MulEquiv.mk e h) = e := by ext; rfl

then simp [MulAut] turns the goal into

⊢ a * b * x * (b⁻¹ * a⁻¹) = a * b * a⁻¹ * (a * x * a⁻¹) * (a * (b⁻¹ * a⁻¹))

[Kevin Buzzard]

I don't know why people are saying these simp lemmas aren't needed; since funlike I think they are.

[Kevin Buzzard]

@[simp] theorem _root_.MulEquiv.coe_mk_apply {M N : Type _} [Mul M] [Mul N] (e : M ≃ N) (h) (x):
    (_root_.MulEquiv.mk e h) x = e x := rfl

(_root_ just because you're in the MulAut namespace) and then

  map_mul' a b := by
    ext x
    simp only [mul_inv_rev, MulEquiv.coe_mk_apply, Equiv.coe_fn_mk, mul_apply, mul_assoc, inv_mul_cancel_left]

solves the goal.