From f0b35d5047d1a3b57628ac041a6ed486f8dd12f4 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 30 Sep 2024 19:38:00 +1000
Subject: [PATCH] chore: fix explicitness of Option.mem_toList

---
 src/Init/Data/Option/List.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/Option/List.lean b/src/Init/Data/Option/List.lean
index 17616c379ea3..aa22d3912d04 100644
--- a/src/Init/Data/Option/List.lean
+++ b/src/Init/Data/Option/List.lean
@@ -8,7 +8,7 @@ import Init.Data.List.Lemmas
 
 namespace Option
 
-@[simp] theorem mem_toList (a : α) (o : Option α) : a ∈ o.toList ↔ a ∈ o := by
+@[simp] theorem mem_toList {a : α} {o : Option α} : a ∈ o.toList ↔ a ∈ o := by
   cases o <;> simp [eq_comm]
 
 end Option