Comment by cma

Many of the statements were already there and looked over by the community in lean prior to the work though, the statement can get formalized before the proof of it.