mathlib

2985fa3c - feat(combinatorics/simple_graph/prod): add finset lemma and remove unecessary `decidable_eq` (#17461)

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.