mathlib

690643ab - fix(tactic/equiv_rw): don't use `subst` unnecessarily (#2334)

fix(tactic/equiv_rw): don't use `subst` unnecessarily (#2334) This removes an unnecessary `subst` from the algorithm in `equiv_rw`, which was responsible for inserting `eq.rec`'s in data terms.