refactor(combinatorics/simple_graph/matching): change definition of matching (#5210)
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 <067de2d7f4f5809454de1022e9c3aab9efe72888@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib