refactor(combinatorics/simple_graph/matching): change definition of matching (#5210)
Refactored definition of matching per @eric-wieser's [suggestion](https://github.com/leanprover-community/mathlib/pull/5156#discussion_r535102524) and @kmill's [suggestion](https://github.com/leanprover-community/mathlib/pull/5156#discussion_r535745112), for the purpose of using `matching.sub_edges` instead of `matching.prop.sub_edges`
Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>