How to humanly verify $ba^5ba=b^2a^4$ in the group with presentation $\langle a,b : a^7=1, b^3=1, ba^2=ab \rangle$?

Question

The group with presentation $\langle a,b : a^7=1, b^3=1, ba^2=ab \rangle$ is isomorphic to $\mathbb{Z}_7 \rtimes \mathbb{Z}_3$ (ref.).

Q: How can I (as a human) verify that $ba^5ba=b^2a^4$ in this group?

Attempting to do this by hand became tedious quickly, although it's more than possible I didn't look in the right direction.

(Perhaps there software that automatically generates a human-readable proof?)

---

I can verify this identity on the computer: If I understand correctly, this presentation is used for this group for $\mathbb{Z}_7 \rtimes \mathbb{Z}_3$ in GAP. To check this:

gap> G:=SmallGroup(21,1);;        
gap> StructureDescription(G);
"C7 : C3"
gap> P:=PresentationViaCosetTable(G);;
gap> TzPrintRelators(P);   
#I  1. f1^3
#I  2. f1*f2^2*f1^-1*f2^-1

Here we have $a$ given by f2 and $b$ given by f1. (I add in the relation $a^7=1$; it makes no difference.) After setting the variables

gap> a:=GeneratorsOfGroup(G)[2];
f2
gap> b:=GeneratorsOfGroup(G)[1];
f1

we can then check b*a^5*b*a=b^2*a^4; is true. But it doesn't show me how it works, so it's not too helpful.

Answer 1

Use $ab=ba^2$ systematically on the left hand side, and $a^7=1$ when it helps, and move the second $b$ to the "front" as follows:

$$ba^5ba=ba^4ba^3=ba^3ba^5=ba^2b=baba^2=b^2a^4$$

Note that you could short cut this by noticing $a^rb=ba^{2r}$ so that you could write immediately $$ba^5ba=b^2a^{11}=b^2a^4$$