∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  ModuleCat.RestrictionCoextensionAdj.counit' f =
    { app := fun X => ModuleCat.ofHom { toFun := fun g => g.toFun 1, map_add' := ⋯, map_smul' := ⋯ }, naturality := ⋯ }