fix ray_trash

jjdishere · Nov 21, 2023 · 5ed7609 · 5ed7609
1 parent e5abc42
commit 5ed7609
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean
@@ -9,7 +9,7 @@ theorem Seg_nd.not_lies_int_extn_and_rev_extn_of_lies_on {A : P} {seg_nd : Seg_n
   apply Ray.not_lies_int_of_lies_on_rev
   simp only [extn_eq_rev_toray_rev, Ray.rev_rev_eq_self]
   apply lies_on_toray_of_lies_on
-  apply Seg.lies_on_iff_lies_on_rev.mpr
+  apply Seg.lies_on_rev_iff_lies_on.mpr
   exact lieson
   apply Ray.not_lies_int_of_lies_on_rev
   simp only [extn_eq_rev_toray_rev, Ray.rev_rev_eq_self, Seg_nd.rev_rev_eq_self]