mathlib3

1cb8e142 - add weak dual namespace fixes + extra lemmas