Lean IsColimit over a Quot: put the descended map in its own def

When building IsColimit for a cocone whose point is a quotient (e.g. desc s := ↾Quot.lift f (by ...) or a custom π₀.lift f hf), proofs of fac/uniq that restate the lift with _ for the proof argument fail with "don't know how to synthesize placeholder for argument hf". Define the descended function as a separate def descFun (s : Cocone X) with an rfl @[simp] descFun_mk lemma, and use desc s := ↾descFun s. In the TypeCat-based Mathlib (morphisms of types via ConcreteCategory.hom), congr_fun (congrArg ConcreteCategory.hom h) x fails to typecheck; use ConcreteCategory.congr_hom h x. Also Functor.map_id under open CategoryTheory can resolve to the root monad lemma, so write CategoryTheory.Functor.map_id.