R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
        u 2 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
      u 2 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
        u 0 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
      u 0 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
        u 1 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0] =
    ![vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 2 -
          vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 1 +
        (v 1 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2 -
          v 2 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1),
      vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 0 -
          vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 2 +
        (v 2 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0 -
          v 0 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2),
      vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 1 -
          vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 0 +
        (v 0 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1 -
          v 1 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0)]
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ↑(↑crossProduct u) (↑(↑crossProduct v) w) =
    ↑(↑crossProduct (↑(↑crossProduct u) v)) w + ↑(↑crossProduct v) (↑(↑crossProduct u) w)
simp_rw [cross_apply, vec3_add]
no goals
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
        u 2 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
      u 2 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
        u 0 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
      u 0 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
        u 1 * vecCons (v 1 * w 2 - v 2 * w 1) ![v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0] =
    ![vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 2 -
          vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 1 +
        (v 1 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2 -
          v 2 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1),
      vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 0 -
          vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 2 +
        (v 2 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0 -
          v 0 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2),
      vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 1 -
          vecCons (u 1 * v 2 - u 2 * v 1) ![u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 0 +
        (v 0 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1 -
          v 1 * vecCons (u 1 * w 2 - u 2 * w 1) ![u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0)]
apply vec3_eq <;> norm_num <;> ring