Replace constructor with Iff.intro

katydid · Jan 13, 2025 · ab94823 · ab94823
1 parent de8f3bb
commit ab94823
Showing 1 changed file with 1 addition and 1 deletion.
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⟩