mathlib3

b063c286 - fix(src/tactic/alias): Support `alias foo ↔ ..` as documented (#13743)

fix(src/tactic/alias): Support `alias foo ↔ ..` as documented (#13743) the current code and the single(!) use of this feature work only if you write `alias foo ↔ . .` which is very odd.