could the simp tactic simplify along equiv?

Stream: general

[Joël Riou]

The simp tactic works very well for rewriting terms and replacing a Prop by an equivalent Prop, but when the goal is a certain type B and we have an equivalence some_equiv : A ≃ B, would not that make sense if simp only [some_equiv] was able to do apply some_equiv.inv_fun?
(I have no idea about how tactics are implemented, whether this is feasible or not, or whether it would cause other problems.)

import data.equiv.basic

def A := ℕ × ℤ
def B := ℤ × ℕ

@[simps]
def some_equiv : A ≃ B := equiv.prod_comm _ _

example (b : B) : A :=
begin
  apply some_equiv.inv_fun,
  exact b,
end

example (b : B) : A :=
begin
  simp only [some_equiv], /- could the simp tactic be extended to make this work? -/
  exact b,
end

[Fabian Glöckle]

take a look at the transport tactic

[Gabriel Ebner]

Or rather equiv_rw (transport is a wrapper around that to transport algebraic structures).

[Joël Riou]

Thanks very much! Then, in this case equiv_rw some_equiv would do the job :-)