mathlib

cea83e19 - feat(data/finmap): add an equivalence with pairs `(keys, lookup)` (#18151)

feat(data/finmap): add an equivalence with pairs `(keys, lookup)` (#18151) A non-dependent version of the equivalence requested [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Proving.20equality.20of.20sigma.20types).