awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
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]
⊢ False
have 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
Tactic: simp_rw [cross_apply, cons_eq_zero_iff, zero_empty, and_true, sub_eq_zero] at h1
Cleared hypotheses: h1
-- 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]
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
⊢ False
have h20 : -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)
-- 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]
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
⊢ False
have h21 : -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)
-- 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]
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
⊢ False
have h22 : -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)
-- 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]
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
⊢ False
have h20₁ : ![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
Cleared hypotheses: h20, h21, h22
-- 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]
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
h20₁ : ![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
⊢ False
have h21₁ : ![w 1 • v 0, w 1 • v 1, w 1 • v 2] = ![v 1 • w 0, v 1 • w 1, v 1 • w 2] → -w 1 = 0 ∧ v 1 = 0
Tactic: rw [neg_smul, neg_add_eq_zero, hv', hw', smul_vec3, smul_vec3, ← hv', ← hw'] at h20 h21 h22
Cleared hypotheses: h20, h21, h22
-- 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]
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
h20₁ : ![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
h21₁ : ![w 1 • v 0, w 1 • v 1, w 1 • v 2] = ![v 1 • w 0, v 1 • w 1, v 1 • w 2] → -w 1 = 0 ∧ v 1 = 0
⊢ False
have h22₁ : ![w 2 • v 0, w 2 • v 1, w 2 • v 2] = ![v 2 • w 0, v 2 • w 1, v 2 • w 2] → -w 2 = 0 ∧ v 2 = 0
Tactic: rw [neg_smul, neg_add_eq_zero, hv', hw', smul_vec3, smul_vec3, ← hv', ← hw'] at h20 h21 h22
Cleared hypotheses: h20, h21, h22
-- 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]
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 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
h21 : ![w 1 • v 0, w 1 • v 1, w 1 • v 2] = ![v 1 • w 0, v 1 • w 1, v 1 • w 2] → -w 1 = 0 ∧ v 1 = 0
h22 : ![w 2 • v 0, w 2 • v 1, w 2 • v 2] = ![v 2 • w 0, v 2 • w 1, v 2 • w 2] → -w 2 = 0 ∧ v 2 = 0
⊢ False
have h20₁ : True → -w 0 = 0 ∧ v 0 = 0
Tactic: simp only [smul_eq_mul, mul_comm (w 0), mul_comm (w 1), mul_comm (w 2), h1] at h20 h21 h22
Cleared hypotheses: h20, h21, h22
-- 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]
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 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
h21 : ![w 1 • v 0, w 1 • v 1, w 1 • v 2] = ![v 1 • w 0, v 1 • w 1, v 1 • w 2] → -w 1 = 0 ∧ v 1 = 0
h22 : ![w 2 • v 0, w 2 • v 1, w 2 • v 2] = ![v 2 • w 0, v 2 • w 1, v 2 • w 2] → -w 2 = 0 ∧ v 2 = 0
h20₁ : True → -w 0 = 0 ∧ v 0 = 0
⊢ False
have h21₁ : True → -w 1 = 0 ∧ v 1 = 0
Tactic: simp only [smul_eq_mul, mul_comm (w 0), mul_comm (w 1), mul_comm (w 2), h1] at h20 h21 h22
Cleared hypotheses: h20, h21, h22
-- 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]
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 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
h21 : ![w 1 • v 0, w 1 • v 1, w 1 • v 2] = ![v 1 • w 0, v 1 • w 1, v 1 • w 2] → -w 1 = 0 ∧ v 1 = 0
h22 : ![w 2 • v 0, w 2 • v 1, w 2 • v 2] = ![v 2 • w 0, v 2 • w 1, v 2 • w 2] → -w 2 = 0 ∧ v 2 = 0
h20₁ : True → -w 0 = 0 ∧ v 0 = 0
h21₁ : True → -w 1 = 0 ∧ v 1 = 0
⊢ False
have h22₁ : True → -w 2 = 0 ∧ v 2 = 0
Tactic: simp only [smul_eq_mul, mul_comm (w 0), mul_comm (w 1), mul_comm (w 2), h1] at h20 h21 h22
Cleared hypotheses: h20, h21, h22
-- 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]
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 : True → -w 0 = 0 ∧ v 0 = 0
h21 : True → -w 1 = 0 ∧ v 1 = 0
h22 : True → -w 2 = 0 ∧ v 2 = 0
⊢ False
have hv₁ : ¬(v 0 = 0 ∧ v 1 = 0 ∧ v 2 = 0 ∧ Eq.{u_2 + 1} (α := Fin 0 → F) ![] ![])
Tactic: rw [hv', cons_eq_zero_iff, cons_eq_zero_iff, cons_eq_zero_iff, zero_empty] at hv
Cleared hypotheses: hv, hv', hw', h2, h1, h20, h21, h22
-- 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)
            ((((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 =
    (u ⬝ᵥ w) • v - (v ⬝ᵥ w) • u
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] 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,
    ![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,
    ![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] =
  (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u
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 : 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] 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,
      ![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,
      ![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] =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u
have h : ∀ (i : Fin (Nat.succ 0).succ.succ),
  ![![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,
        ![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,
        ![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]
      i =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
i : Fin (Nat.succ 0).succ.succ
⊢ ![![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,
        ![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,
        ![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]
      i =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u) i
have h : ![![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,
      ![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,
      ![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]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
i : Fin (Nat.succ 0).succ.succ
h :
  ![![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,
        ![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,
        ![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]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨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,
        ![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,
        ![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]
      i =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u) i
have h₁ : ![![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,
      ![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,
      ![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]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
i : Fin (Nat.succ 0).succ.succ
h :
  ![![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,
        ![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,
        ![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]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![![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,
        ![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,
        ![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]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨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,
        ![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,
        ![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]
      i =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u) i
have h₂ : ![![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,
      ![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,
      ![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]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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 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,
        ![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,
        ![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]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
have h : (u 2 * v 0 - u 0 * v 2) * w 2 - (u 0 * v 1 - u 1 * v 0) * w 1 =
  (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * v 0 - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) * u 0
Tactic: simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.reduceFinMk, cons_val,
      Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
-- 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 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,
        ![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,
        ![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]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
have h : (u 0 * v 1 - u 1 * v 0) * w 0 - (u 1 * v 2 - u 2 * v 1) * w 2 =
  (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * v 1 - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) * u 1
Tactic: simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.reduceFinMk, cons_val,
      Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
-- 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 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,
        ![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,
        ![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]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
have h : (u 1 * v 2 - u 2 * v 1) * w 1 - (u 2 * v 0 - u 0 * v 2) * w 0 =
  (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * v 2 - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) * u 2
Tactic: simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.reduceFinMk, cons_val,
      Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
-- 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) =
    (u ⬝ᵥ w) • v - (v ⬝ᵥ u) • w
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 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w
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 : 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 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w
have h : ∀ (i : Fin (Nat.succ 0).succ.succ),
  ![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]
      i =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w) i
Tactic: ext i