This is just a lake project that requires both lean-minimizer and Mathlib. It's a convenient place to run minimizations of examples involving Mathlib.