From 8ac1b902376eb0afc1536ac87b9187c10fb0091b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 20 Feb 2024 16:15:41 +0100
Subject: [PATCH] fix: PHPDemo

---
 LeanSAT/PHPDemo/Nodup.lean   | 416 +++++++++--------------------------
 LeanSAT/PHPDemo/Theorem.lean |  80 +++----
 2 files changed, 150 insertions(+), 346 deletions(-)

diff --git a/LeanSAT/PHPDemo/Nodup.lean b/LeanSAT/PHPDemo/Nodup.lean
index f31cf48e..567a0fd7 100644
--- a/LeanSAT/PHPDemo/Nodup.lean
+++ b/LeanSAT/PHPDemo/Nodup.lean
@@ -24,10 +24,10 @@ theorem eq_zero_or_one_or_two_of_lt_three {n : Nat} (h : n < 3) : n = 0 ∨ n =
   . exact Or.inr $ Or.inr h
 
 theorem c1Nodup :
-  ∀ i : Fin #[(v1, true), (v2, true), (v3, true)].size, ∀ j : Fin #[(v1, true), (v2, true), (v3, true)].size,
-  i.1 ≠ j.1 → #[(v1, true), (v2, true), (v3, true)][i] ≠ #[(v1, true), (v2, true), (v3, true)][j] := by
+    ∀ i : Fin #[(v1, true), (v2, true), (v3, true)].size, ∀ j : Fin #[(v1, true), (v2, true), (v3, true)].size,
+    i.1 ≠ j.1 → #[(v1, true), (v2, true), (v3, true)][i] ≠ #[(v1, true), (v2, true), (v3, true)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v1, true), (v2, true), (v3, true)].size = 3 := by simp only
+  have hsize : #[(v1, true), (v2, true), (v3, true)].size = 3 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -36,27 +36,14 @@ theorem c1Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_or_two_of_lt_three j_property
   rcases i_vals with hi | hi | hi
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c2Nodup :
-  ∀ i : Fin #[(v4, true), (v5, true), (v6, true)].size, ∀ j : Fin #[(v4, true), (v5, true), (v6, true)].size,
-  i.1 ≠ j.1 → #[(v4, true), (v5, true), (v6, true)][i] ≠ #[(v4, true), (v5, true), (v6, true)][j] := by
+    ∀ i : Fin #[(v4, true), (v5, true), (v6, true)].size, ∀ j : Fin #[(v4, true), (v5, true), (v6, true)].size,
+    i.1 ≠ j.1 → #[(v4, true), (v5, true), (v6, true)][i] ≠ #[(v4, true), (v5, true), (v6, true)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v4, true), (v5, true), (v6, true)].size = 3 := by simp only
+  have hsize : #[(v4, true), (v5, true), (v6, true)].size = 3 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -65,27 +52,14 @@ theorem c2Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_or_two_of_lt_three j_property
   rcases i_vals with hi | hi | hi
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c3Nodup :
-  ∀ i : Fin #[(v7, true), (v8, true), (v9, true)].size, ∀ j : Fin #[(v7, true), (v8, true), (v9, true)].size,
-  i.1 ≠ j.1 → #[(v7, true), (v8, true), (v9, true)][i] ≠ #[(v7, true), (v8, true), (v9, true)][j] := by
+    ∀ i : Fin #[(v7, true), (v8, true), (v9, true)].size, ∀ j : Fin #[(v7, true), (v8, true), (v9, true)].size,
+    i.1 ≠ j.1 → #[(v7, true), (v8, true), (v9, true)][i] ≠ #[(v7, true), (v8, true), (v9, true)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v7, true), (v8, true), (v9, true)].size = 3 := by simp only
+  have hsize : #[(v7, true), (v8, true), (v9, true)].size = 3 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -94,27 +68,14 @@ theorem c3Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_or_two_of_lt_three j_property
   rcases i_vals with hi | hi | hi
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c4Nodup :
-  ∀ i : Fin #[(v10, true), (v11, true), (v12, true)].size, ∀ j : Fin #[(v10, true), (v11, true), (v12, true)].size,
-  i.1 ≠ j.1 → #[(v10, true), (v11, true), (v12, true)][i] ≠ #[(v10, true), (v11, true), (v12, true)][j] := by
+    ∀ i : Fin #[(v10, true), (v11, true), (v12, true)].size, ∀ j : Fin #[(v10, true), (v11, true), (v12, true)].size,
+    i.1 ≠ j.1 → #[(v10, true), (v11, true), (v12, true)][i] ≠ #[(v10, true), (v11, true), (v12, true)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v10, true), (v11, true), (v12, true)].size = 3 := by simp only
+  have hsize : #[(v10, true), (v11, true), (v12, true)].size = 3 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -123,27 +84,14 @@ theorem c4Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_or_two_of_lt_three j_property
   rcases i_vals with hi | hi | hi
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c5Nodup :
-  ∀ i : Fin #[(v1, false), (v4, false)].size, ∀ j : Fin #[(v1, false), (v4, false)].size,
-  i.1 ≠ j.1 → #[(v1, false), (v4, false)][i] ≠ #[(v1, false), (v4, false)][j] := by
+    ∀ i : Fin #[(v1, false), (v4, false)].size, ∀ j : Fin #[(v1, false), (v4, false)].size,
+    i.1 ≠ j.1 → #[(v1, false), (v4, false)][i] ≠ #[(v1, false), (v4, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v1, false), (v4, false)].size = 2 := by simp only
+  have hsize : #[(v1, false), (v4, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -152,22 +100,14 @@ theorem c5Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c6Nodup :
-  ∀ i : Fin #[(v1, false), (v7, false)].size, ∀ j : Fin #[(v1, false), (v7, false)].size,
-  i.1 ≠ j.1 → #[(v1, false), (v7, false)][i] ≠ #[(v1, false), (v7, false)][j] := by
+    ∀ i : Fin #[(v1, false), (v7, false)].size, ∀ j : Fin #[(v1, false), (v7, false)].size,
+    i.1 ≠ j.1 → #[(v1, false), (v7, false)][i] ≠ #[(v1, false), (v7, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v1, false), (v7, false)].size = 2 := by simp only
+  have hsize : #[(v1, false), (v7, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -176,22 +116,14 @@ theorem c6Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c7Nodup :
-  ∀ i : Fin #[(v1, false), (v10, false)].size, ∀ j : Fin #[(v1, false), (v10, false)].size,
-  i.1 ≠ j.1 → #[(v1, false), (v10, false)][i] ≠ #[(v1, false), (v10, false)][j] := by
+    ∀ i : Fin #[(v1, false), (v10, false)].size, ∀ j : Fin #[(v1, false), (v10, false)].size,
+    i.1 ≠ j.1 → #[(v1, false), (v10, false)][i] ≠ #[(v1, false), (v10, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v1, false), (v10, false)].size = 2 := by simp only
+  have hsize : #[(v1, false), (v10, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -200,22 +132,14 @@ theorem c7Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c8Nodup :
-  ∀ i : Fin #[(v4, false), (v7, false)].size, ∀ j : Fin #[(v4, false), (v7, false)].size,
-  i.1 ≠ j.1 → #[(v4, false), (v7, false)][i] ≠ #[(v4, false), (v7, false)][j] := by
+    ∀ i : Fin #[(v4, false), (v7, false)].size, ∀ j : Fin #[(v4, false), (v7, false)].size,
+    i.1 ≠ j.1 → #[(v4, false), (v7, false)][i] ≠ #[(v4, false), (v7, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v4, false), (v7, false)].size = 2 := by simp only
+  have hsize : #[(v4, false), (v7, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -224,22 +148,14 @@ theorem c8Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c9Nodup :
-  ∀ i : Fin #[(v4, false), (v10, false)].size, ∀ j : Fin #[(v4, false), (v10, false)].size,
-  i.1 ≠ j.1 → #[(v4, false), (v10, false)][i] ≠ #[(v4, false), (v10, false)][j] := by
+    ∀ i : Fin #[(v4, false), (v10, false)].size, ∀ j : Fin #[(v4, false), (v10, false)].size,
+    i.1 ≠ j.1 → #[(v4, false), (v10, false)][i] ≠ #[(v4, false), (v10, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v4, false), (v10, false)].size = 2 := by simp only
+  have hsize : #[(v4, false), (v10, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -248,22 +164,14 @@ theorem c9Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c10Nodup :
-  ∀ i : Fin #[(v7, false), (v10, false)].size, ∀ j : Fin #[(v7, false), (v10, false)].size,
-  i.1 ≠ j.1 → #[(v7, false), (v10, false)][i] ≠ #[(v7, false), (v10, false)][j] := by
+    ∀ i : Fin #[(v7, false), (v10, false)].size, ∀ j : Fin #[(v7, false), (v10, false)].size,
+    i.1 ≠ j.1 → #[(v7, false), (v10, false)][i] ≠ #[(v7, false), (v10, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v7, false), (v10, false)].size = 2 := by simp only
+  have hsize : #[(v7, false), (v10, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -272,22 +180,14 @@ theorem c10Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c11Nodup :
-  ∀ i : Fin #[(v2, false), (v5, false)].size, ∀ j : Fin #[(v2, false), (v5, false)].size,
-  i.1 ≠ j.1 → #[(v2, false), (v5, false)][i] ≠ #[(v2, false), (v5, false)][j] := by
+    ∀ i : Fin #[(v2, false), (v5, false)].size, ∀ j : Fin #[(v2, false), (v5, false)].size,
+    i.1 ≠ j.1 → #[(v2, false), (v5, false)][i] ≠ #[(v2, false), (v5, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v2, false), (v5, false)].size = 2 := by simp only
+  have hsize : #[(v2, false), (v5, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -296,22 +196,14 @@ theorem c11Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c12Nodup :
-  ∀ i : Fin #[(v2, false), (v8, false)].size, ∀ j : Fin #[(v2, false), (v8, false)].size,
-  i.1 ≠ j.1 → #[(v2, false), (v8, false)][i] ≠ #[(v2, false), (v8, false)][j] := by
+    ∀ i : Fin #[(v2, false), (v8, false)].size, ∀ j : Fin #[(v2, false), (v8, false)].size,
+    i.1 ≠ j.1 → #[(v2, false), (v8, false)][i] ≠ #[(v2, false), (v8, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v2, false), (v8, false)].size = 2 := by simp only
+  have hsize : #[(v2, false), (v8, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -320,22 +212,14 @@ theorem c12Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c13Nodup :
-  ∀ i : Fin #[(v2, false), (v11, false)].size, ∀ j : Fin #[(v2, false), (v11, false)].size,
-  i.1 ≠ j.1 → #[(v2, false), (v11, false)][i] ≠ #[(v2, false), (v11, false)][j] := by
+    ∀ i : Fin #[(v2, false), (v11, false)].size, ∀ j : Fin #[(v2, false), (v11, false)].size,
+    i.1 ≠ j.1 → #[(v2, false), (v11, false)][i] ≠ #[(v2, false), (v11, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v2, false), (v11, false)].size = 2 := by simp only
+  have hsize : #[(v2, false), (v11, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -344,22 +228,14 @@ theorem c13Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c14Nodup :
-  ∀ i : Fin #[(v5, false), (v8, false)].size, ∀ j : Fin #[(v5, false), (v8, false)].size,
-  i.1 ≠ j.1 → #[(v5, false), (v8, false)][i] ≠ #[(v5, false), (v8, false)][j] := by
+    ∀ i : Fin #[(v5, false), (v8, false)].size, ∀ j : Fin #[(v5, false), (v8, false)].size,
+    i.1 ≠ j.1 → #[(v5, false), (v8, false)][i] ≠ #[(v5, false), (v8, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v5, false), (v8, false)].size = 2 := by simp only
+  have hsize : #[(v5, false), (v8, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -368,22 +244,14 @@ theorem c14Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c15Nodup :
-  ∀ i : Fin #[(v5, false), (v11, false)].size, ∀ j : Fin #[(v5, false), (v11, false)].size,
-  i.1 ≠ j.1 → #[(v5, false), (v11, false)][i] ≠ #[(v5, false), (v11, false)][j] := by
+    ∀ i : Fin #[(v5, false), (v11, false)].size, ∀ j : Fin #[(v5, false), (v11, false)].size,
+    i.1 ≠ j.1 → #[(v5, false), (v11, false)][i] ≠ #[(v5, false), (v11, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v5, false), (v11, false)].size = 2 := by simp only
+  have hsize : #[(v5, false), (v11, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -392,22 +260,14 @@ theorem c15Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c16Nodup :
-  ∀ i : Fin #[(v8, false), (v11, false)].size, ∀ j : Fin #[(v8, false), (v11, false)].size,
-  i.1 ≠ j.1 → #[(v8, false), (v11, false)][i] ≠ #[(v8, false), (v11, false)][j] := by
+    ∀ i : Fin #[(v8, false), (v11, false)].size, ∀ j : Fin #[(v8, false), (v11, false)].size,
+    i.1 ≠ j.1 → #[(v8, false), (v11, false)][i] ≠ #[(v8, false), (v11, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v8, false), (v11, false)].size = 2 := by simp only
+  have hsize : #[(v8, false), (v11, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -416,22 +276,14 @@ theorem c16Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c17Nodup :
-  ∀ i : Fin #[(v3, false), (v6, false)].size, ∀ j : Fin #[(v3, false), (v6, false)].size,
-  i.1 ≠ j.1 → #[(v3, false), (v6, false)][i] ≠ #[(v3, false), (v6, false)][j] := by
+    ∀ i : Fin #[(v3, false), (v6, false)].size, ∀ j : Fin #[(v3, false), (v6, false)].size,
+    i.1 ≠ j.1 → #[(v3, false), (v6, false)][i] ≠ #[(v3, false), (v6, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v3, false), (v6, false)].size = 2 := by simp only
+  have hsize : #[(v3, false), (v6, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -440,22 +292,14 @@ theorem c17Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c18Nodup :
-  ∀ i : Fin #[(v3, false), (v9, false)].size, ∀ j : Fin #[(v3, false), (v9, false)].size,
-  i.1 ≠ j.1 → #[(v3, false), (v9, false)][i] ≠ #[(v3, false), (v9, false)][j] := by
+    ∀ i : Fin #[(v3, false), (v9, false)].size, ∀ j : Fin #[(v3, false), (v9, false)].size,
+    i.1 ≠ j.1 → #[(v3, false), (v9, false)][i] ≠ #[(v3, false), (v9, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v3, false), (v9, false)].size = 2 := by simp only
+  have hsize : #[(v3, false), (v9, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -464,22 +308,14 @@ theorem c18Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c19Nodup :
-  ∀ i : Fin #[(v3, false), (v12, false)].size, ∀ j : Fin #[(v3, false), (v12, false)].size,
-  i.1 ≠ j.1 → #[(v3, false), (v12, false)][i] ≠ #[(v3, false), (v12, false)][j] := by
+    ∀ i : Fin #[(v3, false), (v12, false)].size, ∀ j : Fin #[(v3, false), (v12, false)].size,
+    i.1 ≠ j.1 → #[(v3, false), (v12, false)][i] ≠ #[(v3, false), (v12, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v3, false), (v12, false)].size = 2 := by simp only
+  have hsize : #[(v3, false), (v12, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -488,22 +324,14 @@ theorem c19Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c20Nodup :
-  ∀ i : Fin #[(v6, false), (v9, false)].size, ∀ j : Fin #[(v6, false), (v9, false)].size,
-  i.1 ≠ j.1 → #[(v6, false), (v9, false)][i] ≠ #[(v6, false), (v9, false)][j] := by
+    ∀ i : Fin #[(v6, false), (v9, false)].size, ∀ j : Fin #[(v6, false), (v9, false)].size,
+    i.1 ≠ j.1 → #[(v6, false), (v9, false)][i] ≠ #[(v6, false), (v9, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v6, false), (v9, false)].size = 2 := by simp only
+  have hsize : #[(v6, false), (v9, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -512,22 +340,14 @@ theorem c20Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c21Nodup :
-  ∀ i : Fin #[(v6, false), (v12, false)].size, ∀ j : Fin #[(v6, false), (v12, false)].size,
-  i.1 ≠ j.1 → #[(v6, false), (v12, false)][i] ≠ #[(v6, false), (v12, false)][j] := by
+    ∀ i : Fin #[(v6, false), (v12, false)].size, ∀ j : Fin #[(v6, false), (v12, false)].size,
+    i.1 ≠ j.1 → #[(v6, false), (v12, false)][i] ≠ #[(v6, false), (v12, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v6, false), (v12, false)].size = 2 := by simp only
+  have hsize : #[(v6, false), (v12, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -536,22 +356,14 @@ theorem c21Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
 
 theorem c22Nodup :
-  ∀ i : Fin #[(v9, false), (v12, false)].size, ∀ j : Fin #[(v9, false), (v12, false)].size,
-  i.1 ≠ j.1 → #[(v9, false), (v12, false)][i] ≠ #[(v9, false), (v12, false)][j] := by
+    ∀ i : Fin #[(v9, false), (v12, false)].size, ∀ j : Fin #[(v9, false), (v12, false)].size,
+    i.1 ≠ j.1 → #[(v9, false), (v12, false)][i] ≠ #[(v9, false), (v12, false)][j] := by
   intro i j i_ne_j heq
-  have hsize : #[(v9, false), (v12, false)].size = 2 := by simp only
+  have hsize : #[(v9, false), (v12, false)].size = 2 := by decide
   simp only [getElem_fin] at heq
   have i_property := i.2
   simp only [hsize] at i_property
@@ -560,13 +372,5 @@ theorem c22Nodup :
   simp only [hsize] at j_property
   have j_vals := eq_zero_or_one_of_lt_two j_property
   rcases i_vals with hi | hi
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
-  . rcases j_vals with hj | hj
-    repeat {
-      simp only [hi, hj] at i_ne_j
-      try {simp only [hi, Array.getElem_eq_data_get, List.get, hj, Prod.mk.injEq] at heq}
-    }
+  all_goals
+    rcases j_vals with hj | hj <;> simp_all (config := { decide := true }) [Array.getElem_eq_data_get, List.get]
diff --git a/LeanSAT/PHPDemo/Theorem.lean b/LeanSAT/PHPDemo/Theorem.lean
index 2287bacb..8d2bc73d 100644
--- a/LeanSAT/PHPDemo/Theorem.lean
+++ b/LeanSAT/PHPDemo/Theorem.lean
@@ -70,173 +70,173 @@ theorem php3_of_php3_formula_unsat : unsatisfiable (PosFin 13) php3_formula →
       List.mem_cons, Prod.mk.injEq, and_false, List.mem_singleton, or_self, Bool.not_eq_true, false_implies, and_true, true_and,
       forall_eq_or_imp, decide_eq_false_iff_not, forall_eq, List.mem_nil_iff] at php3_unsat
     cases hfp1 : f p1
-    repeat {simp only [hfp1, not_true, not_false_eq_true, implies_true, and_self, and_true] at php3_unsat}
+    repeat {simp (config := { decide := true }) only [hfp1, not_true, not_false_eq_true, implies_true, and_self, and_true] at php3_unsat}
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c2Nodup c (Eq.symm hc)
     simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10 ,v11, v12, Array.toList_eq, Array.data_toArray, List.find?,
       List.mem_cons, Prod.mk.injEq, and_false, List.mem_singleton, or_self, Bool.not_eq_true, false_implies, and_true, true_and,
       forall_eq_or_imp, decide_eq_false_iff_not, forall_eq, List.mem_nil_iff] at php3_unsat
     cases hfp2 : f p2
-    repeat {simp only [hfp2, not_true, not_false_eq_true, implies_true, and_self, and_true] at php3_unsat}
+    repeat {simp (config := { decide := true }) only [hfp2, not_true, not_false_eq_true, implies_true, and_self, and_true] at php3_unsat}
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c3Nodup c (Eq.symm hc)
     simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10 ,v11, v12, Array.toList_eq, Array.data_toArray, List.find?,
       List.mem_cons, Prod.mk.injEq, and_false, List.mem_singleton, or_self, Bool.not_eq_true, false_implies, and_true, true_and,
       forall_eq_or_imp, decide_eq_false_iff_not, forall_eq, List.mem_nil_iff] at php3_unsat
     cases hfp3 : f p3
-    repeat {simp only [hfp3, not_true, not_false_eq_true, implies_true, and_self, and_true] at php3_unsat}
+    repeat {simp (config := { decide := true }) only [hfp3, not_true, not_false_eq_true, implies_true, and_self, and_true] at php3_unsat}
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c4Nodup c (Eq.symm hc)
     simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10 ,v11, v12, Array.toList_eq, Array.data_toArray, List.find?,
       List.mem_cons, Prod.mk.injEq, and_false, List.mem_singleton, or_self, Bool.not_eq_true, false_implies, and_true, true_and,
       forall_eq_or_imp, decide_eq_false_iff_not, forall_eq, List.mem_nil_iff] at php3_unsat
     cases hfp4 : f p4
-    repeat {simp only [hfp4, not_true, not_false_eq_true, implies_true, and_self, and_true] at php3_unsat}
+    repeat {simp (config := { decide := true }) only [hfp4, not_true, not_false_eq_true, implies_true, and_self, and_true] at php3_unsat}
 
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c5Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p1 p2 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c6Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p1 p3 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c7Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p1 p4 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c8Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p2 p3 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c9Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p2 p4 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c10Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p3 p4 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
 
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c11Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p1 p2 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c12Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p1 p3 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c13Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p1 p4 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c14Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p2 p3 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c15Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p2 p4 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c16Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p3 p4 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
 
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c17Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p1 p2 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c18Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p1 p3 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c19Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p1 p4 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | c_in_php3_formula
   . have hc' := Clause.ofArray_eq _ c20Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p2 p3 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   rcases c_in_php3_formula with hc | hc
   . have hc' := Clause.ofArray_eq _ c21Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p2 p4 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
   . have hc' := Clause.ofArray_eq _ c22Nodup c (Eq.symm hc)
-    simp only [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
+    simp [hc', v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, Array.toList_eq, Array.data_toArray, List.find?, List.mem_cons,
       Prod.mk.injEq, and_true, List.mem_singleton, Bool.not_eq_true, and_false, or_self, false_implies, forall_eq_or_imp,
       decide_eq_false_iff_not, decide_not, Bool.not_eq_false', decide_eq_true_eq, forall_eq, List.mem_nil_iff] at php3_unsat
     specialize h p3 p4 (by simp only [not_false_eq_true])
-    rw [php3_unsat.1, php3_unsat.2.1] at h
+    rw [php3_unsat.1, php3_unsat.2] at h
     exact h rfl
 
 def php3_lrat_proof := certified_php3_lrat_proof.map Subtype.val