diff --git a/tests/lean/run/fieldAutoBound.lean b/tests/lean/run/fieldAutoBound.lean
new file mode 100644
index 0000000000..847eab275e
--- /dev/null
+++ b/tests/lean/run/fieldAutoBound.lean
@@ -0,0 +1,10 @@
+namespace Test
+
+open Function
+
+class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
+  map_const : (Functor.mapConst : α → f β → f α) = Functor.map ∘ const β
+  id_map (x : f α) : id <$> x = x
+  comp_map (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> x
+
+end Test