To do

Finish porting to Lean 3
Replace suppose with assume when that change is in stable Lean
Replace let ... := ... in with obtain when it is added back to Lean 3
Consider replacing lemma with theorem if they remove it