Replace constructor with Iff.intro

keeganperry7 · awalterschulze · commit ab9482348650 · 2025-01-13T12:30:52.000Z
diff --git a/Katydid/Regex/SmartRegex.lean b/Katydid/Regex/SmartRegex.lean
@@ -436,7 +436,7 @@ theorem derive_commutes {α: Type} (r: Regex α) (x: α):
     split_ifs with h
     · rw [denote]
       simp only [Language.emptystr, cons.injEq]
-      constructor
+      apply Iff.intro
       · intro hxs
         use x
       · intro ⟨w, hxs, hp⟩
