chore(PresheafedSpace): remove mk_coe and some comments from porting (

#21382)

My experience with `SimpVarHead` is that declarations flagged are something that Lean can handle with eta-reduction/expansion. Either way, this declaration is not used in mathlib and the commented out code doesn't seem to be missed.

Mathlib/Geometry/RingedSpace/PresheafedSpace.lean

@@ -59,11 +59,6 @@ attribute [coe] PresheafedSpace.carrier
 
 instance : CoeSort (PresheafedSpace C) Type* where coe X := X.carrier
 
-theorem mk_coe (carrier) (presheaf) :
-    (({ carrier
-        presheaf } : PresheafedSpace C) : TopCat) = carrier :=
-  rfl
-
 instance (X : PresheafedSpace C) : TopologicalSpace X :=
   X.carrier.str