{M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        (c : Con M) → (f : N →* M) → (Con.comap ⇑f ⋯ c).Quotient ≃* ↥(MonoidHom.mrange (c.mk'.comp f))