mathlib3

36ce13fe - chore(finset/nat/antidiagonal): simplify some proofs (#3225)

chore(finset/nat/antidiagonal): simplify some proofs (#3225) Replace some proofs with `rfl`, and avoid `multiset.to_finset` when there is a `nodup` available. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>