feat(data/sym/sym2): Induction on `sym2` (#10189)
feat(data/sym/sym2): Induction on `sym2` (#10189)

A few basics about `sym2` that were blatantly missing.





leanprover-community/mathlib,leanprover-community/mathlib