-- Mathlib/Combinatorics/Configuration.lean
lemma crossProduct_eq_zero_of_dotProduct_eq_zero {a b c d : Fin 3 → K} (hac : dotProduct a c = 0)
    (hbc : dotProduct b c = 0) (had : dotProduct a d = 0) (hbd : dotProduct b d = 0) :
    crossProduct a b = 0 ∨ crossProduct c d = 0

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
⊢ False

Tactic:
let A : Matrix (Fin 2) (Fin 3) K := ![a, b]

Result:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0

Tactic:
by_contra h

Result:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : ¬((crossProduct a) b = 0 ∨ (crossProduct c) d = 0)
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
hAB : A.rank + Bᵀ.rank ≤ Fintype.card (Fin 3)
⊢ False

Tactic:
rw [rank_transpose, h.1.rank_matrix, h.2.rank_matrix, Fintype.card_fin, Fintype.card_fin] at hAB

Result:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
hAB : (Nat.succ 0).succ + (Nat.succ 0).succ ≤ 3
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
⊢ False

Tactic:
have hAB : A * B.transpose = 0 := by
  ext i j
  fin_cases i <;> fin_cases j <;> assumption

Result:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
hAB : A * Bᵀ = 0
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
hAB : (Nat.succ 0).succ + (Nat.succ 0).succ ≤ 3
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
⊢ A * Bᵀ = 0

Tactic:
ext i j

Result:
case a
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
i j : Fin 2
⊢ (A * Bᵀ) i j = 0 i j

Proof state:
case a
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
i j : Fin 2
⊢ (A * Bᵀ) i j = 0 i j

Tactic:
fin_cases i <;> fin_cases j <;> assumption

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
hAB : A * Bᵀ = 0
⊢ False

Tactic:
replace hAB := rank_add_rank_le_card_of_mul_eq_zero hAB

Result:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
hAB : A.rank + Bᵀ.rank ≤ Fintype.card (Fin 3)
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : ¬((crossProduct a) b = 0 ∨ (crossProduct c) d = 0)
⊢ False

Tactic:
simp_rw [not_or, ← ne_eq, crossProduct_ne_zero_iff_linearIndependent] at h

Result:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
⊢ False

Tactic:
let B : Matrix (Fin 2) (Fin 3) K := ![c, d]

Result:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]
A : Matrix (Fin 2) (Fin 3) K := ![a, b]
B : Matrix (Fin 2) (Fin 3) K := ![c, d]
⊢ False