Commit 2020-06-10 12:49 671284e3

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, }