chore: fmt bench

src/Init/Data/Option/Basic.lean

@@ -292,6 +292,12 @@ instance (r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.lt
   | some _, none   => isFalse not_false
   | none,   none   => isFalse not_false
 
+instance (r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.le r)
+  | none,   some _ => isTrue trivial
+  | some x, some y => s x y
+  | some _, none   => isFalse not_false
+  | none,   none   => isTrue trivial
+
 namespace SomeLtNone
 
 /--

src/Lean/Data.lean

@@ -30,3 +30,4 @@ public import Lean.Data.NameTrie
 public import Lean.Data.RBTree
 public import Lean.Data.RBMap
 public import Lean.Data.RArray
+public import Lean.Data.Fmt

src/Lean/Data/Fmt.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2025 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Marc Huisinga
+-/
+module
+
+prelude
+public import Lean.Data.Fmt.Basic
+public import Lean.Data.Fmt.Formatter
+public import Lean.Data.Fmt.LawfulCost
+public import Lean.Data.Fmt.Json