∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] (x x_1 x_2 x_3 : { v // v ≠ 0 }) (a : Fˣ),
  (fun m => m • ↑x_1) a = ↑x →
    ∀ (b : Fˣ),
      (fun m => m • ↑x_3) b = ↑x_2 →
        (fun v w => if h : (crossProduct ↑v) ↑w = 0 then v else ⟨(crossProduct ↑v) ↑w, h⟩) x x_2 ≈
          (fun v w => if h : (crossProduct ↑v) ↑w = 0 then v else ⟨(crossProduct ↑v) ↑w, h⟩) x_1 x_3