mathlib3

baaa85a6 - comment out lemmas that are not direct consequences of indep_k