refactor: name the default SizeOf instance (#5981)

This PR names the default SizeOf instance `instSizeOfDefault`

I regularly have to debug termination checking failures where I end up
hovering over some termination measure, and seeing `instSizeOfDefault`
is more likely to tell me that the default instance is used than
`instSizeOf`.

src/Init/SizeOf.lean

@@ -41,7 +41,11 @@ for every element of `α`.
 protected def default.sizeOf (α : Sort u) : α → Nat
   | _ => 0
 
-instance (priority := low) (α : Sort u) : SizeOf α where
+/--
+Every type `α` has a low priority default `SizeOf` instance that just returns `0`
+for every element of `α`.
+-/
+instance (priority := low) instSizeOfDefault (α : Sort u) : SizeOf α where
   sizeOf := default.sizeOf α
 
 @[simp] theorem sizeOf_default (n : α) : sizeOf n = 0 := rfl