diff --git a/library/init/data/ordering/basic.lean b/library/init/data/ordering/basic.lean
index 9f8e7b80e0..79f839d7fa 100644
--- a/library/init/data/ordering/basic.lean
+++ b/library/init/data/ordering/basic.lean
@@ -31,7 +31,7 @@ theorem swap_swap : ∀ (o : ordering), o.swap.swap = o
 | gt := rfl
 end ordering
 
-def cmp_using {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (a b : α) : ordering :=
+@[inline] def cmp_using {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (a b : α) : ordering :=
 if lt a b      then ordering.lt
 else if lt b a then ordering.gt
 else                ordering.eq