mathlib3

8430207e - feat(combinatorics/simple_graph/prod): add `locally_finite` instance for the box product of `locally_finite` graphs, plus two related lemmas (#16431)

feat(combinatorics/simple_graph/prod): add `locally_finite` instance for the box product of `locally_finite` graphs, plus two related lemmas (#16431) Co-authored-by: Chris Birkbeck <c.birkbeck@ucl.ac.uk> Co-authored-by: mcdoll <moritz.doll@googlemail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: negiizhao <egresf@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Kevin Wilson <khwilson@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk> Co-authored-by: jakelev <levinson.jake@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Michael Stoll <Michael.Stoll@uni-bayreuth.de> Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com> Co-authored-by: Rémy Degenne <Remydegenne@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>