awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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
have 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)
Tactic: dsimp only [Matrix.cons_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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]
have 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
Tactic: rw [vec3_dotProduct, cross_apply, det_fin_three]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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
have 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
Tactic: dsimp only [Matrix.cons_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w x : Fin 3 → R
⊢ 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
have 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)
Tactic: simp_rw [cross_apply, vec3_dotProduct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w x : Fin 3 → R
⊢ ![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)
have 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)
Tactic: dsimp only [Matrix.cons_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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) 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)
have 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)]
Tactic: simp_rw [cross_apply, vec3_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ ![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)]
have h₀ : 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: apply vec3_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
h₀ :
  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)
⊢ ![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)]
have h₁ : 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: apply vec3_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
F : Type u_2
inst : Field F
v w : 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]
have 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)
Tactic: rw [not_iff_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
F : Type u_2
inst : Field F
v w : 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)
have 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)
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)
⊢ ¬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)
have 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)
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
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)
have pos : ¬LinearIndependent F ![0, w]
Tactic: rw [hv, map_zero, LinearMap.zero_apply, eq_self, iff_true]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)
⊢ ¬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)
have 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]
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
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)
have 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)
Tactic: rw [LinearIndependent.pair_iff' hv, not_forall_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
F : Type u_2
inst : Field F
v : Fin 3 → F
hv : ¬v = 0
a : F
⊢ 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)
have 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
Tactic: rw [map_smul, cross_self, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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
⊢ 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)
have neg₁ : HSMul.hSMul (β := Fin 3 → F) a 0 = 0
Tactic: rw [map_smul, cross_self, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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
⊢ 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)
have neg₂ : Eq.{u_2 + 1} (α := Fin 3 → F) 0 0
Tactic: rw [map_smul, cross_self, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (hypothesis)
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 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)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F) →
    ¬LinearIndependent F ![v, w]
have hv' : v = ![v 0, v 1, v 2]
Tactic: have hv' : v = ![v 0, v 1, v 2] := by simp [← List.ofFn_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (hypothesis)
Goal:
F : Type u_2
inst : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
⊢ 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]
have hw' : w = ![w 0, w 1, w 2]
Tactic: have hw' : w = ![w 0, w 1, w 2] := by simp [← List.ofFn_inj]