Commit 2022-11-15 12:38 2985fa3c

feat(combinatorics/simple_graph/prod): add finset lemma and remove unecessary decidable_eq (#17461) Now that [fintype (G.neighbor_set x.1)] [fintype (H.neighbor_set x.2)] alone implies fintype ((G □ H).neighbor_set x) without additional decidable_eq arguments, there is no real need to supply the latter argument to lemmas about (G □ H).neighbor_finset. The new simple_graph.box_prod_neighbor_finset lemma unfortunately isn't true by refl, but the new fintype instance now at least has the right asymptotic complexity in computation.