There's a formula from vector calculus that seems terrible to deduce. This formula is:
$$\nabla\times (A\times B)=(B\cdot\nabla )A-(A\cdot \nabla)B+A (\nabla\cdot B)-B(\nabla\cdot A)$$
Deducing it by computing explicitly the left hand side and getting to the right hand side is feasible but seems complicated, verbose and coordinate dependent. Is it possible to get this from differential form calculus?
I mean, taking the curl of a vector field is equivalent as taking the exterior derivative of a one form. Taking the cross product of vector fields is equivalent to take the wedge product of one forms.
So we would be computing something like $d(\omega\wedge \eta)$ which we know how to compute. The problem is that $\omega \wedge \eta$ should be a $1$-form for all of this to work out.
I really don't know how to do it. Is it feasible? If so, how can we deduce this?
There's an easy way to prove it using Cartesian Tensor Notation! Look at (2.10): http://phys.columbia.edu/~cheung/courses/MMSP2014/PS/s14_sol01.pdf
I hope this is what you were looking for