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.