reassociate to prune goals?

Stream: maths

[Jakob von Raumer]

Is there a tactic for categories similar to slice_lhs which prunes away components of morphisms that already match up on both sides? I'd assume that's sometimes more efficient than just modifying small subterms until _everything_ matches up on both sides? /cc @Scott Morrison @Markus Himmel

[Bhavik Mehta]

congr can sometimes do things like this. Personally I tend to avoid slice_lhs these days, usually you can find pure rewrite proofs which are much shorter without it. A particular trick which is super useful is to use assoc in the forward direction as much as you can, and then use reassociated versions of lemmas where needed

[Jakob von Raumer]

congr often misfires though. Reassociating and applying whisker_eq also does the trick, I noticed. Using reassociated lemmas is a good point, maybe I can use that to golf this monster a bit...

[Bhavik Mehta]

You can use congr' 1 or variants to refine it better as well