mathlib3

46fb0d8b - feat(big_operators/intervals): lemma on dependent double sum (#6361)