chore: fix long line

leanprover-community · Oct 25, 2024 · 401211b · 401211b
1 parent 146f718
commit 401211b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Batteries/Data/Fin/Enum.lean b/Batteries/Data/Fin/Enum.lean
@@ -162,8 +162,8 @@ private instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : DecidableRel
 
 instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : Fin.Enum (Quotient s) where
   size := Fin.count fun i => getRepr (decodeSetoid s) i = i
-  decode i := Quotient.liftOn (decodeQuotient (decodeSetoid s) i) (fun i => Quotient.mk s (decode i))
-    (fun _ _ h => Quotient.sound h)
+  decode i := Quotient.liftOn (decodeQuotient (decodeSetoid s) i)
+    (fun i => Quotient.mk s (decode i)) (fun _ _ h => Quotient.sound h)
   encode x := Quotient.liftOn x
     (fun x => encodeQuotient (decodeSetoid s) (Quotient.mk _ (encode x))) <| by
       intro _ _ h