feat(combinatorics/simple_graph/basic): Graph construction from edges (#16691)
feat(combinatorics/simple_graph/basic): Graph construction from edges (#16691)

This PR adds ways to construct a `simple_graph` from the `set` or `finset` of edges. It can further simplify the addition/deletion of edges from a graph. It also enables the induction on the edges of the graph using finset induction.





Co-authored-by: Kyle Miller <04892e540c93233cb5dfa2674fa5218f82feced5@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib