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$? 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.

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$$
