-- Mathlib/LinearAlgebra/CrossProduct.lean
lemma crossProduct_ne_zero_iff_linearIndependent {F : Type*} [Field F] {v w : Fin 3 → F} :
    crossProduct v w ≠ 0 ↔ LinearIndependent F ![v, w]

Proof state:
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]

Result:
no goals

Proof state:
case neg.mpr
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

Tactic:
rw [hv', cons_eq_zero_iff, cons_eq_zero_iff, cons_eq_zero_iff, zero_empty] at hv

Result:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬(v 0 = 0 ∧ v 1 = 0 ∧ v 2 = 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

Proof state:
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
⊢ (crossProduct v) w ≠ 0 ↔ LinearIndependent F ![v, w]

Tactic:
rw [not_iff_comm]

Result:
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
⊢ ¬LinearIndependent F ![v, w] ↔ (crossProduct v) w = 0

Proof state:
case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ ¬LinearIndependent F ![v, w] → (crossProduct v) w = 0

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

Result:
case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ (∃ x, x • v = w) → (crossProduct v) w = 0

Proof state:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ (crossProduct v) w = 0 → ¬LinearIndependent F ![v, w]

Tactic:
have hv' : v = ![v 0, v 1, v 2] := by simp [← List.ofFn_inj]

Result:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
⊢ (crossProduct v) w = 0 → ¬LinearIndependent F ![v, w]

Proof state:
case neg
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ ¬LinearIndependent F ![v, w] ↔ (crossProduct v) w = 0

Tactic:
constructor

Result:
case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ ¬LinearIndependent F ![v, w] → (crossProduct v) w = 0

case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ (crossProduct v) w = 0 → ¬LinearIndependent F ![v, w]

Proof state:
case neg.mpr
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

Tactic:
simp only [smul_eq_mul, mul_comm (w 0), mul_comm (w 1), mul_comm (w 2), h1] at h20 h21 h22

Result:
case neg.mpr
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

Proof state:
case neg.mpr
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

Tactic:
have h22 := LinearIndependent.pair_iff.mp h2 (- w 2) (v 2)

Result:
case neg.mpr
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

Proof state:
case neg.mpr
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

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

Result:
case neg.mpr
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

Proof state:
case neg.mpr
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 : (crossProduct v) w = 0
h2 : LinearIndependent F ![v, w]
⊢ False

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

Result:
case neg.mpr
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

Proof state:
case neg.mpr
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

Tactic:
have h20 := LinearIndependent.pair_iff.mp h2 (- w 0) (v 0)

Result:
case neg.mpr
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

Proof state:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬(v 0 = 0 ∧ v 1 = 0 ∧ v 2 = 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

Tactic:
exact hv ⟨(h20 trivial).2, (h21 trivial).2, (h22 trivial).2, rfl⟩

Result:
no goals

Proof state:
case neg.mp.intro
F : Type u_2
inst✝ : Field F
v : Fin 3 → F
hv : ¬v = 0
a : F
⊢ (crossProduct v) (a • v) = 0

Tactic:
rw [LinearMap.map_smul, cross_self, smul_zero]

Result:
no goals

Proof state:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
⊢ (crossProduct v) w = 0 → ¬LinearIndependent F ![v, w]

Tactic:
have hw' : w = ![w 0, w 1, w 2] := by simp [← List.ofFn_inj]

Result:
case neg.mpr
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]
⊢ (crossProduct v) w = 0 → ¬LinearIndependent F ![v, w]

Proof state:
case pos
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

Result:
no goals