∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G},
  UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A)
      (MulOpposite.op b0) (MulOpposite.op a0) →
    UniqueMul A B a0 b0