feat: port CategoryTheory.Sites.DenseSubsite (#3985)

Mostly straightforward. Had to fight with `simp` once and the typeclass inference system a couple of times.

Author: kbuzzard

Mathlib.lean

@@ -675,6 +675,7 @@ import Mathlib.CategoryTheory.SingleObj
 import Mathlib.CategoryTheory.Sites.Adjunction
 import Mathlib.CategoryTheory.Sites.CoverLifting
 import Mathlib.CategoryTheory.Sites.CoverPreserving
+import Mathlib.CategoryTheory.Sites.DenseSubsite
 import Mathlib.CategoryTheory.Sites.Grothendieck
 import Mathlib.CategoryTheory.Sites.LeftExact
 import Mathlib.CategoryTheory.Sites.Limits