-- Mathlib/Combinatorics/Configuration.lean
lemma eq_or_eq_of_orthogonal {a b c d : ℙ K (Fin 3 → K)} (hac : a.orthogonal c)
    (hbc : b.orthogonal c) (had : a.orthogonal d) (hbd : b.orthogonal d) :
    a = b ∨ c = d

Proof state:
case h
K : Type u_3
inst✝ : Field K
b c d : ℙ K (Fin 3 → K)
hbc : b.orthogonal c
hbd : b.orthogonal d
a : Fin 3 → K
ha : a ≠ 0
hac : (Projectivization.mk K a ha).orthogonal c
had : (Projectivization.mk K a ha).orthogonal d
⊢ Projectivization.mk K a ha = b ∨ c = d

Tactic:
induction b with | h b hb =>
induction c with | h c hc =>
induction d with | h d hd =>
rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Result:
no goals

Proof state:
case h.h.h
K : Type u_3
inst✝ : Field K
d : ℙ K (Fin 3 → K)
a : Fin 3 → K
ha : a ≠ 0
had : (Projectivization.mk K a ha).orthogonal d
b : Fin 3 → K
hb : b ≠ 0
hbd : (Projectivization.mk K b hb).orthogonal d
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
⊢ Projectivization.mk K a ha = Projectivization.mk K b hb ∨ Projectivization.mk K c hc = d

Tactic:
induction d with | h d hd =>
rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Result:
no goals

Proof state:
case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ Projectivization.mk K a ha = Projectivization.mk K b hb ∨ Projectivization.mk K c hc = Projectivization.mk K d hd

Tactic:
rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]

Result:
case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0

Proof state:
case h.h
K : Type u_3
inst✝ : Field K
c d : ℙ K (Fin 3 → K)
a : Fin 3 → K
ha : a ≠ 0
hac : (Projectivization.mk K a ha).orthogonal c
had : (Projectivization.mk K a ha).orthogonal d
b : Fin 3 → K
hb : b ≠ 0
hbc : (Projectivization.mk K b hb).orthogonal c
hbd : (Projectivization.mk K b hb).orthogonal d
⊢ Projectivization.mk K a ha = Projectivization.mk K b hb ∨ c = d

Tactic:
induction c with | h c hc =>
induction d with | h d hd =>
rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Result:
no goals

Proof state:
case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0

Tactic:
exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
a b c d : ℙ K (Fin 3 → K)
hac : a.orthogonal c
hbc : b.orthogonal c
had : a.orthogonal d
hbd : b.orthogonal d
⊢ a = b ∨ c = d

Tactic:
induction a with | h a ha =>
induction b with | h b hb =>
induction c with | h c hc =>
induction d with | h d hd =>
rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Result:
no goals