awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
dsimp :
  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) =
    v 0 * (w 1 * u 2 - w 2 * u 1) + v 1 * (w 2 * u 0 - w 0 * u 2) + v 2 * (w 0 * u 1 - w 1 * u 0)
⊢ u 0 * ![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 * ![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 * ![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 =
    v 0 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 0 +
        v 1 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 1 +
      v 2 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 2

Tactic:
dsimp only [Matrix.cons_val]

Premises used: Matrix.cons_val
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
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) =
    v 0 * (w 1 * u 2 - w 2 * u 1) + v 1 * (w 2 * u 0 - w 0 * u 2) + v 2 * (w 0 * u 1 - w 1 * u 0)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
rw :
  u 0 * ![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 * ![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 * ![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, v, w] 0 0 * ![u, v, w] 1 1 * ![u, v, w] 2 2 - ![u, v, w] 0 0 * ![u, v, w] 1 2 * ![u, v, w] 2 1 -
            ![u, v, w] 0 1 * ![u, v, w] 1 0 * ![u, v, w] 2 2 +
          ![u, v, w] 0 1 * ![u, v, w] 1 2 * ![u, v, w] 2 0 +
        ![u, v, w] 0 2 * ![u, v, w] 1 0 * ![u, v, w] 2 1 -
      ![u, v, w] 0 2 * ![u, v, w] 1 1 * ![u, v, w] 2 0
⊢ u ⬝ᵥ
      (((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        w =
    det ![u, v, w]

Tactic:
rw [vec3_dotProduct, cross_apply, det_fin_three]

Premises used: Matrix.vec3_dotProduct, cross_apply, Matrix.det_fin_three
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
dsimp :
  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
⊢ u 0 * ![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 * ![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 * ![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, v, w] 0 0 * ![u, v, w] 1 1 * ![u, v, w] 2 2 - ![u, v, w] 0 0 * ![u, v, w] 1 2 * ![u, v, w] 2 1 -
            ![u, v, w] 0 1 * ![u, v, w] 1 0 * ![u, v, w] 2 2 +
          ![u, v, w] 0 1 * ![u, v, w] 1 2 * ![u, v, w] 2 0 +
        ![u, v, w] 0 2 * ![u, v, w] 1 0 * ![u, v, w] 2 1 -
      ![u, v, w] 0 2 * ![u, v, w] 1 1 * ![u, v, w] 2 0

Tactic:
dsimp only [Matrix.cons_val]

Premises used: Matrix.cons_val
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
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

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w x : Fin 3 → R
simp_rw :
  ![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 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 0 +
        ![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 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 1 +
      ![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 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 2 =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)
⊢ dotProduct (m := Fin 3)
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) u : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        v)
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) w : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        x) =
    u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w

Tactic:
simp_rw [cross_apply, vec3_dotProduct]

Premises used: Matrix.vec3_dotProduct, cross_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w x : Fin 3 → R
dsimp :
  (u 1 * v 2 - u 2 * v 1) * (w 1 * x 2 - w 2 * x 1) + (u 2 * v 0 - u 0 * v 2) * (w 2 * x 0 - w 0 * x 2) +
      (u 0 * v 1 - u 1 * v 0) * (w 0 * x 1 - w 1 * x 0) =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)
⊢ ![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 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 0 +
        ![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 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 1 +
      ![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 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 2 =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)

Tactic:
dsimp only [Matrix.cons_val]

Premises used: Matrix.cons_val
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w x : Fin 3 → R
⊢ (u 1 * v 2 - u 2 * v 1) * (w 1 * x 2 - w 2 * x 1) + (u 2 * v 0 - u 0 * v 2) * (w 2 * x 0 - w 0 * x 2) +
      (u 0 * v 1 - u 1 * v 0) * (w 0 * x 1 - w 1 * x 0) =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
simp_rw :
  ![u 1 * ![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 * ![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 * ![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 * ![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 * ![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 * ![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 * 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 -
          ![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 * ![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 * ![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),
      ![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 -
          ![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 * ![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 * ![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),
      ![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 -
          ![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 * ![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 * ![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)]
⊢ (((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) u : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
        (a : Fin 3 → R) → Fin 3 → R)
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          w :
        Fin 3 → R) =
    HAdd.hAdd (α := Fin 3 → R) (β := Fin 3 → R)
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R)
                ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) u : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
                    (a : Fin 3 → R) → Fin 3 → R)
                  v) :
              (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          w :
        Fin 3 → R)
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) u : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
                (a : Fin 3 → R) → Fin 3 → R)
              w :
            Fin 3 → R) :
        Fin 3 → R)

Tactic:
simp_rw [cross_apply, vec3_add]

Premises used: Matrix.vec3_add, cross_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
h₀ :
  u 1 * (v 0 * w 1 - v 1 * w 0) - u 2 * (v 2 * w 0 - v 0 * w 2) =
    (u 2 * v 0 - u 0 * v 2) * w 2 - (u 0 * v 1 - u 1 * v 0) * w 1 +
      (v 1 * (u 0 * w 1 - u 1 * w 0) - v 2 * (u 2 * w 0 - u 0 * w 2))
⊢ u 1 * ![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 * ![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 * 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 -
        ![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 * ![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 * ![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)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
h₁ :
  u 2 * (v 1 * w 2 - v 2 * w 1) - u 0 * (v 0 * w 1 - v 1 * w 0) =
    (u 0 * v 1 - u 1 * v 0) * w 0 - (u 1 * v 2 - u 2 * v 1) * w 2 +
      (v 2 * (u 1 * w 2 - u 2 * w 1) - v 0 * (u 0 * w 1 - u 1 * w 0))
⊢ u 2 * ![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 * ![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 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 -
        ![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 * ![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 * ![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)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
h₂ :
  u 0 * (v 2 * w 0 - v 0 * w 2) - u 1 * (v 1 * w 2 - v 2 * w 1) =
    (u 1 * v 2 - u 2 * v 1) * w 1 - (u 2 * v 0 - u 0 * v 2) * w 0 +
      (v 0 * (u 2 * w 0 - u 0 * w 2) - v 1 * (u 1 * w 2 - u 2 * w 1))
⊢ u 0 * ![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 * ![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 * 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 -
        ![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 * ![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 * ![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)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ u 1 * (v 0 * w 1 - v 1 * w 0) - u 2 * (v 2 * w 0 - v 0 * w 2) =
    (u 2 * v 0 - u 0 * v 2) * w 2 - (u 0 * v 1 - u 1 * v 0) * w 1 +
      (v 1 * (u 0 * w 1 - u 1 * w 0) - v 2 * (u 2 * w 0 - u 0 * w 2))

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ u 2 * (v 1 * w 2 - v 2 * w 1) - u 0 * (v 0 * w 1 - v 1 * w 0) =
    (u 0 * v 1 - u 1 * v 0) * w 0 - (u 1 * v 2 - u 2 * v 1) * w 2 +
      (v 2 * (u 1 * w 2 - u 2 * w 1) - v 0 * (u 0 * w 1 - u 1 * w 0))

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 2 * w 0 - v 0 * w 2) - u 1 * (v 1 * w 2 - v 2 * w 1) =
    (u 1 * v 2 - u 2 * v 1) * w 1 - (u 2 * v 0 - u 0 * v 2) * w 0 +
      (v 0 * (u 2 * w 0 - u 0 * w 2) - v 1 * (u 1 * w 2 - u 2 * w 1))

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ (((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R)
            ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) u : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
                (a : Fin 3 → R) → Fin 3 → R)
              v) :
          (Fin 3 → R) →ₗ[R] Fin 3 → R) :
        (a : Fin 3 → R) → Fin 3 → R)
      w =
    HSub.hSub (α := Fin 3 → R) (β := Fin 3 → R)
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) u : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
                (a : Fin 3 → R) → Fin 3 → R)
              w :
            Fin 3 → R) :
        Fin 3 → R)
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) u : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
                (a : Fin 3 → R) → Fin 3 → R)
              w :
            Fin 3 → R) :
        Fin 3 → R)

Tactic:
lie_lie u v w

Premises used: lie_lie
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ HAdd.hAdd (β := Fin 3 → R)
      (HAdd.hAdd (α := Fin 3 → R) (β := Fin 3 → R)
        ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) u : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
              (a : Fin 3 → R) → Fin 3 → R)
            ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
                  (a : Fin 3 → R) → Fin 3 → R)
                w :
              Fin 3 → R) :
          Fin 3 → R)
        ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
              (a : Fin 3 → R) → Fin 3 → R)
            ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) w : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
                  (a : Fin 3 → R) → Fin 3 → R)
                u :
              Fin 3 → R) :
          Fin 3 → R))
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) w : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) u : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
                (a : Fin 3 → R) → Fin 3 → R)
              v :
            Fin 3 → R) :
        Fin 3 → R) =
    0

Tactic:
lie_jacobi u v w

Premises used: lie_jacobi
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
rw :
  ¬LinearIndependent F ![v, w] ↔
    Eq (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F)
⊢ Ne (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F) ↔
    LinearIndependent F ![v, w]

Tactic:
rw [not_iff_comm]

Premises used: not_iff_comm
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
pos :
  ∀ (hv : v = 0),
    ¬LinearIndependent F ![v, w] ↔
      Eq (α := Fin 3 → F)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
          Fin 3 → F)
        (0 : Fin 3 → F)
neg :
  ∀ (hv : ¬v = 0),
    ¬LinearIndependent F ![v, w] ↔
      Eq (α := Fin 3 → F)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
          Fin 3 → F)
        (0 : Fin 3 → F)
⊢ ¬LinearIndependent F ![v, w] ↔
    Eq (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F)

Tactic:
by_cases hv : v = 0
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : v = 0
pos : ¬LinearIndependent F ![0, w]
⊢ ¬LinearIndependent F ![v, w] ↔
    Eq (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F)

Tactic:
rw [hv, map_zero, LinearMap.zero_apply, eq_self, iff_true]

Premises used: LinearMap.zero_apply, iff_true, map_zero, eq_self
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![0, w]

Tactic:
fun h ↦ h.ne_zero 0 rfl

Premises used: LinearIndependent.ne_zero, OfNat.ofNat, Not, rfl
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![0, w]

Tactic:
exact fun h ↦ h.ne_zero 0 rfl
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
neg :
  ¬LinearIndependent F ![v, w] →
    Eq (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F)
neg₁ :
  Eq (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F) →
    ¬LinearIndependent F ![v, w]
⊢ ¬LinearIndependent F ![v, w] ↔
    Eq (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
neg :
  (∃ (x : F), x • v = w) →
    Eq (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F)
⊢ ¬LinearIndependent F ![v, w] →
    Eq (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F)

Tactic:
rw [LinearIndependent.pair_iff' hv, not_forall_not]

Premises used: not_forall_not, LinearIndependent.pair_iff'
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v : Fin 3 → F
hv : ¬v = 0
a : F
neg :
  HSMul.hSMul (β := Fin 3 → F) a
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          v :
        Fin 3 → F) =
    0
neg₁ : HSMul.hSMul (β := Fin 3 → F) a 0 = 0
neg₂ neg₃ : Eq.{u_2 + 1} (α := Fin 3 → F) 0 0
⊢ Eq (α := Fin 3 → F)
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → Fin 3 → F)
        (a • v) :
      Fin 3 → F)
    (0 : Fin 3 → F)

Tactic:
rw [map_smul, cross_self, smul_zero]

Premises used: cross_self, smul_zero, map_smul
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ v = ![v 0, v 1, v 2]

Tactic:
simp [← List.ofFn_inj]

Premises used: List.ofFn_inj
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ v = ![v 0, v 1, v 2]

Tactic:
have hv' : v = ![v 0, v 1, v 2] := by simp [← List.ofFn_inj]
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
⊢ w = ![w 0, w 1, w 2]

Tactic:
simp [← List.ofFn_inj]

Premises used: List.ofFn_inj
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
⊢ w = ![w 0, w 1, w 2]

Tactic:
have hw' : w = ![w 0, w 1, w 2] := by simp [← List.ofFn_inj]
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h1 :
  Eq (α := Fin 3 → F)
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → Fin 3 → F)
        w :
      Fin 3 → F)
    (0 : Fin 3 → F)
h2 : LinearIndependent F ![v, w]
⊢ v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0

Tactic:
simp_rw [cross_apply, cons_eq_zero_iff, zero_empty, and_true, sub_eq_zero] at h1

Premises used: and_true, sub_eq_zero, cross_apply, Matrix.cons_eq_zero_iff, Matrix.zero_empty
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
⊢ -w 0 • v + v 0 • w = 0 → -w 0 = 0 ∧ v 0 = 0

Tactic:
have h20 := LinearIndependent.pair_iff.mp h2 (- w 0) (v 0)
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : -w 0 • v + v 0 • w = 0 → -w 0 = 0 ∧ v 0 = 0
⊢ -w 1 • v + v 1 • w = 0 → -w 1 = 0 ∧ v 1 = 0

Tactic:
have h21 := LinearIndependent.pair_iff.mp h2 (- w 1) (v 1)
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : -w 0 • v + v 0 • w = 0 → -w 0 = 0 ∧ v 0 = 0
h21 : -w 1 • v + v 1 • w = 0 → -w 1 = 0 ∧ v 1 = 0
⊢ -w 2 • v + v 2 • w = 0 → -w 2 = 0 ∧ v 2 = 0

Tactic:
have h22 := LinearIndependent.pair_iff.mp h2 (- w 2) (v 2)
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : -w 0 • v + v 0 • w = 0 → -w 0 = 0 ∧ v 0 = 0
h21 : -w 1 • v + v 1 • w = 0 → -w 1 = 0 ∧ v 1 = 0
h22 : -w 2 • v + v 2 • w = 0 → -w 2 = 0 ∧ v 2 = 0
⊢ ![w 0 • v 0, w 0 • v 1, w 0 • v 2] = ![v 0 • w 0, v 0 • w 1, v 0 • w 2] → -w 0 = 0 ∧ v 0 = 0

Tactic:
rw [neg_smul, neg_add_eq_zero, hv', hw', smul_vec3, smul_vec3, ← hv', ← hw'] at h20 h21 h22

Premises used: neg_smul, Matrix.smul_vec3, neg_add_eq_zero