mathlib

28702123 - chore(data/sym2): golf decidability proofs (#5940)

chore(data/sym2): golf decidability proofs (#5940) This golfs the decidable instances, and removes a redundant one (`from_rel.decidable_as_set` is automatically inferred from `from_rel.decidable_pred`)