From e07ed1ae5cc92635e4e32abd0d41a808b6620ad7 Mon Sep 17 00:00:00 2001
From: Parth Shastri <31370288+cppio@users.noreply.github.com>
Date: Mon, 16 Jun 2025 11:44:56 -0400
Subject: [PATCH] chore: add missing `instance` (#8772)

Changes `ReverseImplicationOrder.instCompleteLattice` to be an
`instance`.
---
 src/Init/Internal/Order/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean
index c3661e497d..cc4d9518e0 100644
--- a/src/Init/Internal/Order/Basic.lean
+++ b/src/Init/Internal/Order/Basic.lean
@@ -914,7 +914,7 @@ instance ReverseImplicationOrder.instOrder : PartialOrder ReverseImplicationOrde
   rel_antisymm h₁ h₂ := propext ⟨h₂, h₁⟩
 
 -- This defines a complete lattice on `Prop`, used to define coinductive predicates
-def ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplicationOrder where
+instance ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplicationOrder where
   sup c := ∀ p, c p → p
   sup_spec := by
     intro x c