type error

Stream: new members

[vxctyxeha]

what is the difference between two sentence,why the seconde failed to synthesize
HMul (Equiv.Perm ℕ) (Equiv.Perm ℕ) ↥A₅

import Mathlib
open Equiv.Perm
open Fin

abbrev S₅ := Equiv.Perm (Fin 5)
abbrev A₅ := alternatingGroup (Fin 5)


theorem a5_commutator_representatives1 :
  ⁅(c[0, 1] : S₅), (c[0, 1] : S₅)⁆ = (1 :  A₅) :=by
      decide
theorem a5_commutator_representatives :
  ⁅(c[0, 1, 2, 3] : S₅), (c[0, 2] : S₅)⁆ = (c[0, 2] * c[1, 3] :A₅) :=by
    decide

[Edward van de Meent]

lean doesn't know how to turn the product of any two permutations into an element of A5. this is the error you're seeing. in the first sentence, however, you only ask lean to recognise that A5 has a unit element, which is easy enough for lean since there is a Group instance.

[Edward van de Meent]

also, note that lean coerces the 1 : A₅ to S₅ anyway, so there is very little point specifying that it is in A₅