simpNF and MulOpposite

Stream: mathlib4

[Antoine Labelle]

In #1001, the simpNF linter gives me the following error:

#check smul_eq_mul_unop /- Left-hand side simplifies from
  a • a'
to
  a * a'
using
  simp only [smul_eq_mul]
Try to change the left-hand side to the simplified term!
 -/

Here is the relevant lemma:

@[simp, to_additive]
theorem MulOpposite.smul_eq_mul_unop [Mul α] {a : αᵐᵒᵖ} {a' : α} : a • a' = a' * a.unop :=
  rfl

That seems very weird to me because a has type αᵐᵒᵖ while a' has type α, so the multiplication a * a' shouldn't be defined (and indeed if I try replacing a • a' by a * a' I get an error failed to synthesize instance HMul αᵐᵒᵖ α ?m.5162 as I would expect). What is going on here?

[Jireh Loreaux]

Well, αᵐᵒᵖ is a type synonym for α, so I imagine that in a * a' that a : α. You should be able to see it with whatever the mathlib4 equivalent of set_option pp.all true is.

[Antoine Labelle]

Well a : αᵐᵒᵖ definitely shouldn't be interpreted as an element of α when interpreting a • a', because, despite being type synonyms αᵐᵒᵖ and α both have a scalar action on α and these are two different actions (left and right multiplication).