Orders on Ordinals

CHANGES.md

@@ -1,5 +1,10 @@
 # Change List
 
+## 2024-02-20
+Added extension for notations `._1` and `._2` for `firstInPair(_)` and `secondInPair(_)`.
+
+Added `assumeAll` keyword to deconstruct the LHS of the goal and assume all discovered formulas.
+
 ## 2024-02-05
 The "draft()" option can now be used at the start of a file to skip checking proofs of theorem outside this file during development.
 

lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala

@@ -261,4 +261,18 @@ object CommonTactics {
     }
   }
 
+  /**
+   * Assume every formula on the LHS of the goal sequent, deconstructing
+   * conjunctions.
+   */
+  def assumeAll(using lib: Library, proof: lib.Proof) =
+    def deconstruct(f: F.Formula): Seq[F.Formula] =
+      f match
+        case F.AppliedConnector(F.And, fs) => fs.flatMap(deconstruct)
+        case _ => Seq(f)
+
+    val lhs = proof.possibleGoal.get.left.toSeq
+    val assumptions = lhs.flatMap(deconstruct).toSeq diff proof.getAssumptions
+
+    lib.assume(using proof)(assumptions: _*)
 }