From e9350edf3c30b9ff3172a0d0ef9e40fae6d2cdb1 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Sat, 25 Nov 2023 18:59:36 +0000
Subject: [PATCH] Proofs improvements

---
 ProvenZk/Gates.lean | 60 ++++++++++++---------------------------------
 1 file changed, 16 insertions(+), 44 deletions(-)

diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean
index 9f3c8be..2dbcf20 100644
--- a/ProvenZk/Gates.lean
+++ b/ProvenZk/Gates.lean
@@ -134,17 +134,10 @@ lemma xor_equivalence {a b out : ZMod N} :
     simp at h
     casesm* (_ ∧ _)
     rename_i ha hb _
-    cases ha
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
+    cases ha <;> cases hb <;> {
+      subst_vars
+      simp
+    }
   . intro h
     casesm* (_ ∨ _)
     repeat (
@@ -166,17 +159,10 @@ lemma or_equivalence {a b out : ZMod N} :
     simp at h
     casesm* (_ ∧ _)
     rename_i ha hb _
-    cases ha
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
+    cases ha <;> cases hb <;> {
+      subst_vars
+      simp
+    }
   . intro h
     casesm* (_ ∨ _)
     repeat (
@@ -200,17 +186,10 @@ lemma and_equivalence {a b out : ZMod N} :
     simp at h
     casesm* (_ ∧ _)
     rename_i ha hb _
-    cases ha
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
+    cases ha <;> cases hb <;> {
+      subst_vars
+      simp
+    }
   . intro h
     casesm* (_ ∨ _)
     repeat (
@@ -280,17 +259,10 @@ lemma lookup_equivalence {b0 b1 i0 i1 i2 i3 out : ZMod N} :
   . intro h
     casesm* (_ ∧ _)
     rename_i hb0 hb1 _
-    cases hb0
-    . cases hb1
-      . subst_vars
-        simp
-      . subst_vars
-        simp
-    . cases hb1
-      . subst_vars
-        simp
-      . subst_vars
-        simp [add_assoc]
+    cases hb0 <;> cases hb1 <;> {
+      subst_vars
+      simp [add_assoc]
+    }
   . intro h
     casesm* (_ ∨ _)
     repeat (