conv α is a tactic for discharging goals of the form
lhs ~ rhs for some relation
~ (usually equality) and fixed lhs, rhs.
Known in the literature as a __conversion__ tactic.
So for example, if one had the lemma
p : x = y, then the conversion for
p would be one that solves
dsimp the LHS.