R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ 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] 0 +
        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] 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] 2 =
    vecCons u ![v, w] 0 0 * vecCons u ![v, w] 1 1 * vecCons u ![v, w] 2 2 -
              vecCons u ![v, w] 0 0 * vecCons u ![v, w] 1 2 * vecCons u ![v, w] 2 1 -
            vecCons u ![v, w] 0 1 * vecCons u ![v, w] 1 0 * vecCons u ![v, w] 2 2 +
          vecCons u ![v, w] 0 1 * vecCons u ![v, w] 1 2 * vecCons u ![v, w] 2 0 +
        vecCons u ![v, w] 0 2 * vecCons u ![v, w] 1 0 * vecCons u ![v, w] 2 1 -
      vecCons u ![v, w] 0 2 * vecCons u ![v, w] 1 1 * vecCons u ![v, w] 2 0
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u ⬝ᵥ ↑(↑crossProduct v) w = det ![u, v, w]
rw [vec3_dotProduct, cross_apply, det_fin_three]
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 1 * w 2 - v 2 * w 1) + u 1 * (v 2 * w 0 - v 0 * w 2) + u 2 * (v 0 * w 1 - v 1 * w 0) =
    u 0 * v 1 * w 2 - u 0 * v 2 * w 1 - u 1 * v 0 * w 2 + u 1 * v 2 * w 0 + u 2 * v 0 * w 1 - u 2 * v 1 * w 0
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ 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] 0 +
        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] 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] 2 =
    vecCons u ![v, w] 0 0 * vecCons u ![v, w] 1 1 * vecCons u ![v, w] 2 2 -
              vecCons u ![v, w] 0 0 * vecCons u ![v, w] 1 2 * vecCons u ![v, w] 2 1 -
            vecCons u ![v, w] 0 1 * vecCons u ![v, w] 1 0 * vecCons u ![v, w] 2 2 +
          vecCons u ![v, w] 0 1 * vecCons u ![v, w] 1 2 * vecCons u ![v, w] 2 0 +
        vecCons u ![v, w] 0 2 * vecCons u ![v, w] 1 0 * vecCons u ![v, w] 2 1 -
      vecCons u ![v, w] 0 2 * vecCons u ![v, w] 1 1 * vecCons u ![v, w] 2 0
norm_num
no goals
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 1 * w 2 - v 2 * w 1) + u 1 * (v 2 * w 0 - v 0 * w 2) + u 2 * (v 0 * w 1 - v 1 * w 0) =
    u 0 * v 1 * w 2 - u 0 * v 2 * w 1 - u 1 * v 0 * w 2 + u 1 * v 2 * w 0 + u 2 * v 0 * w 1 - u 2 * v 1 * w 0
ring