From 42d5714e1457b49a9827237062e5dd10cc67f6ca Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Thu, 26 Dec 2024 17:55:59 +0530
Subject: [PATCH] chore: instMembershipListLanguage ->
 Language.instMembershipList

---
 SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean
index 79d918eeb..61e466085 100644
--- a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean
+++ b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean
@@ -19,9 +19,9 @@ import SSA.Experimental.Bits.AutoStructs.NFA'
 open AutoStructs
 open Mathlib
 
+set_option pp.explicit true in
 @[simp] theorem Language.mem_setOf_eq {x : List α} {p : List α → Prop} :
-    @Membership.mem (List α) (Language α) instMembershipListLanguage {y | p y} x = p x := by
-  rfl
+    @Membership.mem (List α) (Language α) Language.instMembershipList {y | p y} x = p x := rfl
 
 @[simp] theorem Language.trivial : x ∈ (⊤ : Language α) := by trivial