mathlib3

a7aa2c87 - feat(data/finset/sigma): A way to lift `finset`-valued functions to a sigma type (#10958)

feat(data/finset/sigma): A way to lift `finset`-valued functions to a sigma type (#10958) This defines `finset.sigma_lift : (Π i, α i → β i → finset (γ i)) → Σ i, α i → Σ i, β i → finset (Σ i, γ i)` as the function which returns the finset corresponding to the first coordinate of `a b : Σ i, α i` if they have the same, or the empty set else. Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>