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.
def
conv.dsimp
:
(option simp_lemmas := option.none) → (list name := list.nil) → (tactic.dsimp_config := {md := tactic.transparency.reducible, max_steps := simp.default_max_steps, canonize_instances := bool.tt, single_pass := bool.ff, fail_if_unchanged := bool.tt, eta := bool.tt, zeta := bool.tt, beta := bool.tt, proj := bool.tt, iota := bool.tt, unfold_reducible := bool.ff, memoize := bool.tt}) → conv unit
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').