mathlib3

671284e3 - feat(control/equiv_functor/instances): allow equiv_rw on finset (#2997)

feat(control/equiv_functor/instances): allow equiv_rw on finset (#2997) Allows moving `finset` over an `equiv` using `equiv_rw`, as requested by @jcommelin. e.g. ``` import data.finset import tactic.equiv_rw example (σ τ : Type) (e : σ ≃ τ) : finset σ ≃ finset τ := by { equiv_rw e, refl, } ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com>