feat: extract_from_and tactic (#63)

Author: GZGavinZhao

SP1Foundations.lean

@@ -8,5 +8,6 @@ import SP1Foundations.Opcode
 import SP1Foundations.Register
 import SP1Foundations.SP1State
 import SP1Foundations.SailM
+import SP1Foundations.Tactics
 import SP1Foundations.Unsigned
 import SP1Foundations.Word

SP1Foundations/Tactics.lean

@@ -0,0 +1,19 @@
+import Lean
+
+open Lean
+
+/-- Recursively extract a goal from nested conjunctions in the context.
+    Splits ANDs and tries exact on each branch, recursing if needed. -/
+syntax "extract_from_and" ident : tactic
+
+macro_rules
+| `(tactic| extract_from_and $h:ident) => `(tactic|
+  first
+  | exact $h
+  | (obtain ⟨h_left, h_right⟩ := $h
+     first
+     | exact h_left
+     | exact h_right
+     | extract_from_and h_left
+     | extract_from_and h_right)
+)