mathlib3

113568c9 - refactor(archive/100-theorems-list/02_cubing_a_cube): review API (#16898)

refactor(archive/100-theorems-list/02_cubing_a_cube): review API (#16898) * reuse lemmas about `set.pi`; * fix some `def`/`lemma`; * use `nontrivial` and `set.nontrivial` instead of `2 ≤ cardinal.mk ι`; * redefine `correct` as a `structure`.