Rewrite does not always work?

Stream: new members

[Arnoud van der Leer]

Hi, I sometimes encounter error messages like

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  X.map (SimplexCategory.δ 2).op (uliftYonedaEquiv (hom_inv_id ≫ g))
in the target expression
  X.map (SimplexCategory.δ 2).op (uliftYonedaEquiv (hom_inv_id ≫ g)) = f

whilst formalizing. What kind of things can I look for to resolve things like this?
In this case, I have a workaround in the form of apply (...).trans, but that does not solve the underlying problem.
(Also: is there a channel for this kind of question? Should I ask these on stackexchange instead? Because I would expect that after about N questions in this channel (for some N : ℕ), I do no longer qualify as a "new" member)

[Arnoud van der Leer]

Fairly close to the last one, I encounter a similar error:

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  uliftYonedaEquiv.symm f
in the target expression
  uliftYoneda.{0, 0, 0}.map (SimplexCategory.δ 2).op.unop ≫ hom_inv_id ≫ g = uliftYonedaEquiv.symm f

[Lun Song]

This is often due to different implicit arguments or instances. You can check whether their full forms (including implicit arguments) are the same

[Arnoud van der Leer]

How do I see their full form?

[Kevin Buzzard]

set_option pp.all true. Alternatively try erw or convert

[Arnoud van der Leer]

Yup. Probably the implicits.

[Arnoud van der Leer]

Thanks!

[Ruben Van de Velde]

And for your other question: I think this kind of question is still on topic for this stream

[Arnoud van der Leer]

Okay. Then I will keep posting questions here ^^

[Jovan Gerbscheid]

To debug such a failing unification, I find using set_option trace.Meta.isDefEq true in the most convenient tool.