chore(linear_algebra/orientation): golf a proof (#10742)

src/linear_algebra/determinant.lean

@@ -385,6 +385,14 @@ begin
   simp [alternating_map.map_perm, basis.det_self]
 end
 
+@[simp] lemma alternating_map.map_basis_eq_zero_iff (f : alternating_map R M R ι) :
+  f e = 0 ↔ f = 0 :=
+⟨λ h, by simpa [h] using f.eq_smul_basis_det e, λ h, h.symm ▸ alternating_map.zero_apply _⟩
+
+lemma alternating_map.map_basis_ne_zero_iff (f : alternating_map R M R ι) :
+  f e ≠ 0 ↔ f ≠ 0 :=
+not_congr $ f.map_basis_eq_zero_iff e
+
 variables {A : Type*} [comm_ring A] [is_domain A] [module A M]
 
 @[simp] lemma basis.det_comp (e : basis ι A M) (f : M →ₗ[A] M) (v : ι → M) :

src/linear_algebra/orientation.lean

@@ -345,14 +345,11 @@ by rw [basis.orientation, basis.orientation, ray_eq_iff,
 lemma orientation_eq_or_eq_neg (e : basis ι R M) (x : orientation R M ι) :
   x = e.orientation ∨ x = -e.orientation :=
 begin
-  rw [basis.orientation, ←x.some_vector_ray, ray_eq_iff, ←ray_neg, ray_eq_iff,
-      x.some_vector.eq_smul_basis_det e],
-  rcases lt_trichotomy (x.some_vector e) 0 with h|h|h,
-  { right,
-    exact (same_ray_neg_smul_left_iff e.det_ne_zero (_ : R)).2 h },
-  { simpa [h] using x.some_vector.eq_smul_basis_det e },
-  { left,
-    exact (same_ray_smul_left_iff e.det_ne_zero (_ : R)).2 h }
+  induction x using module.ray.ind with x hx,
+  rw [basis.orientation, ray_eq_iff, ←ray_neg, ray_eq_iff, x.eq_smul_basis_det e,
+    same_ray_neg_smul_left_iff e.det_ne_zero (_ : R), same_ray_smul_left_iff e.det_ne_zero (_ : R),
+    lt_or_lt_iff_ne, ne_comm, alternating_map.map_basis_ne_zero_iff],
+  exact hx
 end
 
 end basis