Like Henry, I am not an expert---although I've played around with formal proof assistants.

First, one has to take into account if the background material is already formalized. This can make a big difference. If it is not already formalized then you may need to select a different proof that is more computational and avoids tricks that venture into other territory. (If the proof you are formalizing is fairly new, you may need to do that work yourself which obviously takes time and creativity.) Alternately, one needs to formalize this background material (which can be satisfying, but also takes time).

Second, it matters if you are going for building a beautiful library of math or just trying to hack together some proof until the computer says "proved". In the former case, you may actually spend a few weeks thinking about how you want to set up the whole structure. (As an example, would you define a ring as an Abelian group with multiplication, or would you define it from scratch? If you define it as an Abelian group, then you could also use all the theorems you proved for Abelian groups for rings as well.)

Last, it takes some time to get into the swing of using a proof assistant, but after that, it is fairly mechanical. Nonetheless, there will be a number of times when you think to yourself "this is obvious, but I guess the computer doesn't know that". Then you have to figure out how to convince the computer that it is true, usually by breaking the proof into some trivial logic. However, as with all things, with experience this happens less and less.

I am sorry I can't give you a rate like "one day per page", mostly from my lack of experience.