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 p.
Applies the conversion c. Returns (rhs,p) where p : r lhs rhs. Throws away the return value of c.
⊢ lhs = rhs ~~> ⊢ lhs' = rhs using h : lhs = lhs'.
Change lhs to something definitionally equal to it.
def
conv.dsimp
(s : option simp_lemmas := none)
(u : list name := list.nil)
(cfg : tactic.dsimp_config := {md := reducible, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}) :
dsimp the LHS.
Take the target equality f x y = X and try to apply the congruence lemma for f to it (namely x = x' → y = y' → f x y = f x' y').