I think diagrams for chunked sets are concave not convex? (I looked it up after I said convex previously – Concave function - Wikipedia – outside of polygons, this terminology always confuses me)
Playing around at https://github.com/ajtowns/lean4-clump/tree/master/Clump . Copying the text of those files into https://live.lean-lang.org/ seems to work, without needing to install anything.