mathlib3

da9b530b - Apply name changes and remove redundant instances