diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index caa0f9e15e0c2..c37e317a3ee61 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -129,7 +129,7 @@ theorem comp_eq_fun (f : γ → β) : r ∘r (· = f ·) = (r · <| f ·) := by
 theorem comp_eq : r ∘r (· = ·) = r := comp_eq_fun ..
 
 @[simp]
-theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (f · |> r <| ·) := by
+theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (r <| f ·) := by
   ext x y
   simp [Comp]