From ff72e1029d8ca630cf54d6aa8490f1fb8c02f21a Mon Sep 17 00:00:00 2001
From: Franklin Dyer <franklin+github@dyer.me>
Date: Fri, 4 Oct 2024 11:14:11 -0600
Subject: [PATCH 01/12] added theorem for fully right-associating operation
 trees in associative magmas (semigroups)

---
 equational_theories/FreeMonoid.lean | 50 +++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 equational_theories/FreeMonoid.lean

diff --git a/equational_theories/FreeMonoid.lean b/equational_theories/FreeMonoid.lean
new file mode 100644
index 000000000..2834d5349
--- /dev/null
+++ b/equational_theories/FreeMonoid.lean
@@ -0,0 +1,50 @@
+import equational_theories.Equations
+import equational_theories.FreeMagma
+import equational_theories.MagmaLaw
+
+open FreeMagma
+open Law
+
+namespace FreeMonoid
+
+def treeConcat {α : Type _} (t : FreeMagma α) : List α :=
+  match t with
+    | Lf a      => [a]
+    | (tl ⋆ tr) => treeConcat tl ++ treeConcat tr
+
+def rightJoinTrees {α : Type _} (t1 t2 : FreeMagma α) : FreeMagma α :=
+  match t1 with
+    | Lf a      =>  Lf a ⋆ t2
+    | (tl ⋆ tr) => tl ⋆ (rightJoinTrees tr t2)
+
+def rightAssociateTree {α : Type _} (t : FreeMagma α) : FreeMagma α :=
+  match t with
+    | Lf a      => Lf a
+    | (tl ⋆ tr) => rightJoinTrees (rightAssociateTree tl) (rightAssociateTree tr)
+
+theorem AssocImpliesForkEquivRightJoin {α : Type _} {G : Type _} [Magma G]
+  (assoc : Equation4512 G) (f : α → G) (tl tr : FreeMagma α)
+  : evalInMagma f (tl ⋆ tr) = evalInMagma f (rightJoinTrees tl tr) :=
+  match tl with
+    | Lf _        => Eq.refl _
+    | (tl1 ⋆ tl2) => Eq.trans
+      (Eq.symm $ assoc (evalInMagma f tl1) (evalInMagma f tl2) (evalInMagma f tr))
+      (congrArg (fun t ↦ (evalInMagma f tl1) ◇ t) (AssocImpliesForkEquivRightJoin assoc f tl2 tr))
+
+theorem AssocFullyRightAssociate {α : Type _} {G : Type _} [Magma G]
+  (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α)
+  : evalInMagma f t = evalInMagma f (rightAssociateTree t) :=
+  match t with
+    | Lf _      => Eq.refl _
+    | (tl ⋆ tr) => Eq.trans
+      (congrArg (fun s ↦ s ◇ (evalInMagma f tr)) (AssocFullyRightAssociate assoc f tl)) $ Eq.trans
+      (congrArg (fun s ↦ (evalInMagma f (rightAssociateTree tl)) ◇ s) (AssocFullyRightAssociate assoc f tr))
+      (AssocImpliesForkEquivRightJoin assoc f (rightAssociateTree tl) (rightAssociateTree tr))
+
+/-- Example usage of AssocFullyRightAssociate -/
+theorem Assoc4 {G : Type _} [Magma G] (assoc : Equation4512 G)
+  : ∀ x y z w : G, ((x ◇ y) ◇ z) ◇ w = x ◇ (y ◇ (z ◇ w)) :=
+  fun x y z w ↦ AssocFullyRightAssociate
+    assoc
+    (fun | 0 => x | 1 => y | 2 => z | 3 => w : Fin 4 → G)
+    (((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3)

From 7cab02ed7d0459c4ec5498b871fd5dcb455bb095 Mon Sep 17 00:00:00 2001
From: Franklin Dyer <franklin+github@dyer.me>
Date: Fri, 4 Oct 2024 11:48:37 -0600
Subject: [PATCH 02/12] added Equation1571_implies_Equation3167 as another
 example usage of AssocFullyRightAssociate

---
 equational_theories/AllEquations.lean |  2 +-
 equational_theories/Equations.lean    |  2 ++
 equational_theories/Subgraph.lean     | 12 ++++++++++++
 3 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/equational_theories/AllEquations.lean b/equational_theories/AllEquations.lean
index cc37d9ea7..365419da5 100644
--- a/equational_theories/AllEquations.lean
+++ b/equational_theories/AllEquations.lean
@@ -3185,7 +3185,7 @@ equation 3163 := x = (((y ◇ y) ◇ z) ◇ y) ◇ x
 equation 3164 := x = (((y ◇ y) ◇ z) ◇ y) ◇ y
 equation 3165 := x = (((y ◇ y) ◇ z) ◇ y) ◇ z
 equation 3166 := x = (((y ◇ y) ◇ z) ◇ y) ◇ w
-equation 3167 := x = (((y ◇ y) ◇ z) ◇ z) ◇ x
+-- equation 3167 := x = (((y ◇ y) ◇ z) ◇ z) ◇ x
 equation 3168 := x = (((y ◇ y) ◇ z) ◇ z) ◇ y
 equation 3169 := x = (((y ◇ y) ◇ z) ◇ z) ◇ z
 equation 3170 := x = (((y ◇ y) ◇ z) ◇ z) ◇ w
diff --git a/equational_theories/Equations.lean b/equational_theories/Equations.lean
index 78140ff2c..4b44dfde8 100644
--- a/equational_theories/Equations.lean
+++ b/equational_theories/Equations.lean
@@ -90,6 +90,8 @@ abbrev Equation1689 (G: Type _) [Magma G] := ∀ x y z : G, x = (y ◇ x) ◇ ((
 
 abbrev Equation2662 (G: Type _) [Magma G] := ∀ x y : G, x = ((x ◇ y) ◇ (x ◇ y)) ◇ x
 
+abbrev Equation3167 (G: Type _) [Magma G] := ∀ x y z : G, x = (((y ◇ y) ◇ z) ◇ z) ◇ x
+
 /-- From Putnam 1978, Problem A4, part (a) -/
 abbrev Equation3722 (G: Type _) [Magma G] := ∀ x y : G, x ◇ y = (x ◇ y) ◇ (x ◇ y)
 
diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index fe9a0ecf6..cbe95b440 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -4,6 +4,7 @@ import equational_theories.EquationalResult
 import equational_theories.Closure
 import equational_theories.Equations
 import equational_theories.FactsSyntax
+import equational_theories.FreeMonoid
 
 /- This is a subproject of the main project to completely describe a small subgraph of the entire
 implication graph. The list of equations under consideration can be found at https://teorth.github.io/equational_theories/blueprint/subgraph-eq.html
@@ -340,6 +341,17 @@ theorem Equation1571_implies_Equation4512 (G: Type*) [Magma G] (h: Equation1571
   apply Eq.trans $ h (x ◇ (y ◇ z)) y x
   rw [eq43 (x ◇ (y ◇ z)) x, ← eq16 (y ◇ z) x, ← eq16 z y, eq43 y x]
 
+/-- An example usage of AssocFullyRightAssociate -/
+theorem Equation1571_implies_Equation3167 (G : Type _) [Magma G] (h : Equation1571 G) : Equation3167 G := by
+  intros x y z
+  have eq4512 := Equation1571_implies_Equation4512 G h
+  have eq16 := Equation1571_implies_Equation16 G h
+  apply Eq.symm
+  apply Eq.trans $ FreeMonoid.AssocFullyRightAssociate eq4512 (fun | 0 => y | 1 => y | 2 => z | 3 => z | 4 => x : Fin 5 → G) ((((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3) ⋆ Lf 4)
+  apply Eq.trans $ Eq.symm $ eq16 _ y
+  apply Eq.trans $ Eq.symm $ eq16 _ z
+  exact Eq.refl _
+
 /-- This result was first obtained by Kisielewicz in 1997 via computer assistance. -/
 @[equational_result]
 theorem Equation1689_implies_Equation2 (G: Type*) [Magma G] (h: Equation1689 G) : Equation2 G:= by

From d0d4a283778f9b562203ba356a701040b6a95db4 Mon Sep 17 00:00:00 2001
From: Franklin Dyer <franklin+github@dyer.me>
Date: Fri, 4 Oct 2024 17:16:03 -0600
Subject: [PATCH 03/12] added definition of FreeSemigroup and instanced it into
 Magma

---
 equational_theories/FreeMonoid.lean | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/equational_theories/FreeMonoid.lean b/equational_theories/FreeMonoid.lean
index 2834d5349..6627e096f 100644
--- a/equational_theories/FreeMonoid.lean
+++ b/equational_theories/FreeMonoid.lean
@@ -5,8 +5,6 @@ import equational_theories.MagmaLaw
 open FreeMagma
 open Law
 
-namespace FreeMonoid
-
 def treeConcat {α : Type _} (t : FreeMagma α) : List α :=
   match t with
     | Lf a      => [a]
@@ -48,3 +46,15 @@ theorem Assoc4 {G : Type _} [Magma G] (assoc : Equation4512 G)
     assoc
     (fun | 0 => x | 1 => y | 2 => z | 3 => w : Fin 4 → G)
     (((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3)
+
+inductive FreeSemigroup (α : Type _)
+  | Singleton : α → FreeSemigroup α
+  | Cons : α → FreeSemigroup α → FreeSemigroup α
+
+def semigroupConcat {α : Type _} (s1 s2 : FreeSemigroup α) : FreeSemigroup α :=
+  match s1 with
+    | FreeSemigroup.Singleton a   => FreeSemigroup.Cons a s2
+    | FreeSemigroup.Cons a s1tail => FreeSemigroup.Cons a (semigroupConcat s1tail s2)
+
+instance (α : Type _) : Magma (FreeSemigroup α) where
+  op := semigroupConcat

From 27e53bd59c8d425ef63b1b059bcebd4eaeb4608e Mon Sep 17 00:00:00 2001
From: Franklin Dyer <franklin+github@dyer.me>
Date: Sat, 5 Oct 2024 16:30:13 -0600
Subject: [PATCH 04/12] added (currently nonworking) first attempt at insertion
 sort reduction on commutative semigroups

---
 equational_theories/FreeMonoid.lean | 126 +++++++++++++++++++++++++++-
 1 file changed, 124 insertions(+), 2 deletions(-)

diff --git a/equational_theories/FreeMonoid.lean b/equational_theories/FreeMonoid.lean
index 6627e096f..d3afd532d 100644
--- a/equational_theories/FreeMonoid.lean
+++ b/equational_theories/FreeMonoid.lean
@@ -1,5 +1,8 @@
+import Mathlib.Logic.Basic
+
 import equational_theories.Equations
 import equational_theories.FreeMagma
+import equational_theories.Homomorphisms
 import equational_theories.MagmaLaw
 
 open FreeMagma
@@ -29,6 +32,7 @@ theorem AssocImpliesForkEquivRightJoin {α : Type _} {G : Type _} [Magma G]
       (Eq.symm $ assoc (evalInMagma f tl1) (evalInMagma f tl2) (evalInMagma f tr))
       (congrArg (fun t ↦ (evalInMagma f tl1) ◇ t) (AssocImpliesForkEquivRightJoin assoc f tl2 tr))
 
+/- Associativity allows us to fully right-associate an entire operation tree -/
 theorem AssocFullyRightAssociate {α : Type _} {G : Type _} [Magma G]
   (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α)
   : evalInMagma f t = evalInMagma f (rightAssociateTree t) :=
@@ -47,14 +51,132 @@ theorem Assoc4 {G : Type _} [Magma G] (assoc : Equation4512 G)
     (fun | 0 => x | 1 => y | 2 => z | 3 => w : Fin 4 → G)
     (((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3)
 
+def insertSortedRightAssocTree {n : Nat} (i : (Fin n)) (t : FreeMagma (Fin n)) : FreeMagma (Fin n) :=
+  match t with
+    | Lf j        => ite (i <= j) (Lf i ⋆ Lf j) (Lf j ⋆ Lf i)
+    | Lf j ⋆ tr   => ite (i <= j) (Lf i ⋆ (Lf j ⋆ tr)) (Lf j ⋆ (Lf i ⋆ tr))
+    | (_ ⋆ _) ⋆ _ => Lf i ⋆ t
+
+theorem AssocCommAllowsSortedInsertion {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G)
+  (i : Fin n) (f : Fin n → G) (t : FreeMagma (Fin n))
+  : evalInMagma f (insertSortedRightAssocTree i t) = (f i) ◇ (evalInMagma f t) :=
+  match t with
+    | Lf j => by
+      have eqor := ite_eq_or_eq (i ≤ j) (Lf i ⋆ Lf j) (Lf j ⋆ Lf i)
+      cases eqor with
+      | inl eq1 => apply Eq.trans (congrArg (evalInMagma f) eq1); exact Eq.refl _
+      | inr eq2 => apply Eq.trans (congrArg (evalInMagma f) eq2); exact comm (f j) (f i)
+    | Lf j ⋆ tr => by
+      have eqor := ite_eq_or_eq (i ≤ j) (Lf i ⋆ (Lf j ⋆ tr)) (Lf j ⋆ (Lf i ⋆ tr))
+      cases eqor with
+      | inl eq1 =>
+        apply Eq.trans (congrArg (evalInMagma f) eq1);
+        exact Eq.refl _
+      | inr eq2 =>
+        apply Eq.trans (congrArg (evalInMagma f) eq2);
+        apply Eq.trans $ assoc (f j) (f i) _;
+        rw [comm (f j) (f i)];
+        exact Eq.symm $ assoc (f i) (f j) _
+    | (_ ⋆ _) ⋆ _ => Eq.refl _
+
 inductive FreeSemigroup (α : Type _)
   | Singleton : α → FreeSemigroup α
   | Cons : α → FreeSemigroup α → FreeSemigroup α
 
+local postfix:61 ".+" => FreeSemigroup.Singleton
+local infixr:60 " ,+ " => FreeSemigroup.Cons
+
 def semigroupConcat {α : Type _} (s1 s2 : FreeSemigroup α) : FreeSemigroup α :=
   match s1 with
-    | FreeSemigroup.Singleton a   => FreeSemigroup.Cons a s2
-    | FreeSemigroup.Cons a s1tail => FreeSemigroup.Cons a (semigroupConcat s1tail s2)
+    | a .+        => a ,+ s2
+    | a ,+ s1tail => a ,+ (semigroupConcat s1tail s2)
 
 instance (α : Type _) : Magma (FreeSemigroup α) where
   op := semigroupConcat
+
+theorem FreeSgrAssoc {α : Type} : Equation4512 (FreeSemigroup α) :=
+  fun ls1 ls2 ls3 ↦ match ls1 with
+    | _ .+      => Eq.refl _
+    | a ,+ ls1' => congrArg (fun ls ↦ a ,+ ls) (FreeSgrAssoc ls1' ls2 ls3)
+
+/- "Flatten" a FreeMagma tree expression into its semigroup representation -/
+def freeMagmaToFreeSgr {α : Type _} : MagmaHom (FreeMagma α) (FreeSemigroup α) where
+  toFun := fun t ↦ evalInMagma FreeSemigroup.Singleton t
+  map_op' := fun s _ ↦ match s with
+    | Lf _ => Eq.refl _
+    | _ ⋆ _ => Eq.refl _
+
+local postfix:70 " ↠Sgr " => freeMagmaToFreeSgr.toFun
+
+def evalInSgr {α : Type _} {G : Type _} [Magma G] (f : α → G) (ls : FreeSemigroup α) : G :=
+  match ls with
+    | a .+ => f a
+    | a ,+ lstail => f a ◇ evalInSgr f lstail
+
+def evalInSgrHom {α : Type _} {G : Type _} [Magma G] (assoc : Equation4512 G) (f : α → G) : MagmaHom (FreeSemigroup α) G where
+  toFun := evalInSgr f
+  map_op' := let rec mapper : ∀ ls1 ls2 : FreeSemigroup α, evalInSgr f (ls1 ◇ ls2) = evalInSgr f ls1 ◇ evalInSgr f ls2 :=
+    fun ls1 ls2 ↦ match ls1 with
+      | _ .+      => Eq.refl _
+      | a ,+ ls1' => Eq.trans
+        (congrArg (fun x ↦ f a ◇ x) (mapper ls1' ls2))
+        (assoc (f a) (evalInSgr f ls1') (evalInSgr f ls2))
+    mapper
+
+def foldFreeSemigroup {G : Type _} [Magma G] (ls : FreeSemigroup G) : G :=
+  match ls with
+    | a .+        => a
+    | a ,+ lstail => a ◇ (foldFreeSemigroup lstail)
+
+/- When evaluating in an associative structure, we may reduce a FreeMagma tree to a FreeSemigroup list -/
+theorem AssocImpliesSgrProjFaithful {α : Type _} {G : Type _} [Magma G] (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α)
+  : evalInMagma f t = evalInSgr f (freeMagmaToFreeSgr t) :=
+  match t with
+    | Lf a => Eq.refl _
+    | Lf a ⋆ tr => congrArg (fun y ↦ (f a) ◇ y) (AssocImpliesSgrProjFaithful assoc f tr)
+    | (tl1 ⋆ tl2) ⋆ tr => by
+      apply Eq.symm
+      apply Eq.trans $ congrArg (evalInSgr f) $ freeMagmaToFreeSgr.map_op' (tl1 ⋆ tl2) tr
+      apply Eq.trans $ congrArg (fun s ↦ evalInSgr f (s ◇ tr ↠Sgr)) $ freeMagmaToFreeSgr.map_op' tl1 tl2
+      apply Eq.trans $ (evalInSgrHom assoc f).map_op' (tl1 ↠Sgr ◇ tl2 ↠Sgr) (tr ↠Sgr)
+      apply Eq.trans $ congrArg (fun s ↦ s ◇ (evalInSgr f (tr ↠Sgr))) $ (evalInSgrHom assoc f).map_op' (tl1 ↠Sgr) (tl2 ↠Sgr)
+      apply Eq.symm
+      apply Eq.trans $ congrArg (fun s ↦ _ ◇ s) (AssocImpliesSgrProjFaithful assoc f tr)
+      apply Eq.trans $ congrArg (fun s ↦ (s ◇ _) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl1)
+      apply Eq.trans $ congrArg (fun s ↦ (_ ◇ s) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl2)
+      trivial
+
+def insertSemigroupSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
+  match ls with
+    | j .+        => if i <= j then i ,+ j .+ else j ,+ j .+
+    | j ,+ lstail => if i <= j then i ,+ j ,+ lstail else j ,+ i ,+ lstail
+
+def insertionSortSgr {n : Nat} (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
+  match ls with
+    | i .+ => i .+
+    | i ,+ lstail => insertSemigroupSorted i (insertionSortSgr lstail)
+
+theorem CommSgrImpliesInsertSortedFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
+  : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (i ,+ ls) = (f i) ◇ evalInSgr f ls :=
+  fun i ls ↦ match ls with
+  | j .+ => by
+      have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j .+) (j ,+ i .+)
+      cases eqor with
+      | inl eq1 => apply Eq.trans (congrArg (evalInSgr f) eq1); exact Eq.refl _
+      | inr eq2 => apply Eq.trans (congrArg (evalInSgr f) eq2); exact comm (f j) (f i)
+    | Lf j ⋆ tr => by
+      have eqor := ite_eq_or_eq (i ≤ j) (Lf i ⋆ (Lf j ⋆ tr)) (Lf j ⋆ (Lf i ⋆ tr))
+      cases eqor with
+      | inl eq1 =>
+        apply Eq.trans (congrArg (evalInMagma f) eq1);
+        exact Eq.refl _
+      | inr eq2 =>
+        apply Eq.trans (congrArg (evalInMagma f) eq2);
+        apply Eq.trans $ assoc (f j) (f i) _;
+        rw [comm (f j) (f i)];
+        exact Eq.symm $ assoc (f i) (f j) _
+
+theorem CommSgrImpliesInsertionSortFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
+  : ∀ ls : FreeSemigroup (Fin n), evalInSgr f ls = evalInSgr f (insertionSortSgr ls)
+  | i .+ => Eq.refl _
+  | i ,+ lstail => _

From 8a764dbe402344c3c4a554a3a3d28a5a213aaf33 Mon Sep 17 00:00:00 2001
From: Franklin Dyer <franklin+github@dyer.me>
Date: Sat, 5 Oct 2024 16:55:37 -0600
Subject: [PATCH 05/12] completed insertion sort proof for commutative
 semigroups

---
 equational_theories/FreeMonoid.lean | 48 +++++++----------------------
 1 file changed, 11 insertions(+), 37 deletions(-)

diff --git a/equational_theories/FreeMonoid.lean b/equational_theories/FreeMonoid.lean
index d3afd532d..a2f628aba 100644
--- a/equational_theories/FreeMonoid.lean
+++ b/equational_theories/FreeMonoid.lean
@@ -51,34 +51,6 @@ theorem Assoc4 {G : Type _} [Magma G] (assoc : Equation4512 G)
     (fun | 0 => x | 1 => y | 2 => z | 3 => w : Fin 4 → G)
     (((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3)
 
-def insertSortedRightAssocTree {n : Nat} (i : (Fin n)) (t : FreeMagma (Fin n)) : FreeMagma (Fin n) :=
-  match t with
-    | Lf j        => ite (i <= j) (Lf i ⋆ Lf j) (Lf j ⋆ Lf i)
-    | Lf j ⋆ tr   => ite (i <= j) (Lf i ⋆ (Lf j ⋆ tr)) (Lf j ⋆ (Lf i ⋆ tr))
-    | (_ ⋆ _) ⋆ _ => Lf i ⋆ t
-
-theorem AssocCommAllowsSortedInsertion {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G)
-  (i : Fin n) (f : Fin n → G) (t : FreeMagma (Fin n))
-  : evalInMagma f (insertSortedRightAssocTree i t) = (f i) ◇ (evalInMagma f t) :=
-  match t with
-    | Lf j => by
-      have eqor := ite_eq_or_eq (i ≤ j) (Lf i ⋆ Lf j) (Lf j ⋆ Lf i)
-      cases eqor with
-      | inl eq1 => apply Eq.trans (congrArg (evalInMagma f) eq1); exact Eq.refl _
-      | inr eq2 => apply Eq.trans (congrArg (evalInMagma f) eq2); exact comm (f j) (f i)
-    | Lf j ⋆ tr => by
-      have eqor := ite_eq_or_eq (i ≤ j) (Lf i ⋆ (Lf j ⋆ tr)) (Lf j ⋆ (Lf i ⋆ tr))
-      cases eqor with
-      | inl eq1 =>
-        apply Eq.trans (congrArg (evalInMagma f) eq1);
-        exact Eq.refl _
-      | inr eq2 =>
-        apply Eq.trans (congrArg (evalInMagma f) eq2);
-        apply Eq.trans $ assoc (f j) (f i) _;
-        rw [comm (f j) (f i)];
-        exact Eq.symm $ assoc (f i) (f j) _
-    | (_ ⋆ _) ⋆ _ => Eq.refl _
-
 inductive FreeSemigroup (α : Type _)
   | Singleton : α → FreeSemigroup α
   | Cons : α → FreeSemigroup α → FreeSemigroup α
@@ -148,8 +120,8 @@ theorem AssocImpliesSgrProjFaithful {α : Type _} {G : Type _} [Magma G] (assoc
 
 def insertSemigroupSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
   match ls with
-    | j .+        => if i <= j then i ,+ j .+ else j ,+ j .+
-    | j ,+ lstail => if i <= j then i ,+ j ,+ lstail else j ,+ i ,+ lstail
+    | j .+        => if i ≤ j then i ,+ j .+ else j ,+ i .+
+    | j ,+ lstail => if i ≤ j then i ,+ j ,+ lstail else j ,+ i ,+ lstail
 
 def insertionSortSgr {n : Nat} (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
   match ls with
@@ -157,26 +129,28 @@ def insertionSortSgr {n : Nat} (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin
     | i ,+ lstail => insertSemigroupSorted i (insertionSortSgr lstail)
 
 theorem CommSgrImpliesInsertSortedFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
-  : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (i ,+ ls) = (f i) ◇ evalInSgr f ls :=
+  : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (insertSemigroupSorted i ls) = (f i) ◇ evalInSgr f ls :=
   fun i ls ↦ match ls with
   | j .+ => by
       have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j .+) (j ,+ i .+)
       cases eqor with
       | inl eq1 => apply Eq.trans (congrArg (evalInSgr f) eq1); exact Eq.refl _
       | inr eq2 => apply Eq.trans (congrArg (evalInSgr f) eq2); exact comm (f j) (f i)
-    | Lf j ⋆ tr => by
-      have eqor := ite_eq_or_eq (i ≤ j) (Lf i ⋆ (Lf j ⋆ tr)) (Lf j ⋆ (Lf i ⋆ tr))
+    | j ,+ lstail => by
+      have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j ,+ lstail) (j ,+ i ,+ lstail)
       cases eqor with
       | inl eq1 =>
-        apply Eq.trans (congrArg (evalInMagma f) eq1);
+        apply Eq.trans (congrArg (evalInSgr f) eq1);
         exact Eq.refl _
       | inr eq2 =>
-        apply Eq.trans (congrArg (evalInMagma f) eq2);
+        apply Eq.trans (congrArg (evalInSgr f) eq2);
         apply Eq.trans $ assoc (f j) (f i) _;
         rw [comm (f j) (f i)];
         exact Eq.symm $ assoc (f i) (f j) _
 
 theorem CommSgrImpliesInsertionSortFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
   : ∀ ls : FreeSemigroup (Fin n), evalInSgr f ls = evalInSgr f (insertionSortSgr ls)
-  | i .+ => Eq.refl _
-  | i ,+ lstail => _
+  | _ .+        => Eq.refl _
+  | i ,+ lstail => Eq.trans
+    (congrArg (fun s ↦ (f i) ◇ s) (CommSgrImpliesInsertionSortFaithful assoc comm f lstail))
+    (Eq.symm $ CommSgrImpliesInsertSortedFaithful assoc comm f i (insertionSortSgr lstail))

From 57951d15141f1031df422ea40003b00888bec2df Mon Sep 17 00:00:00 2001
From: Franklin Dyer <franklin+github@dyer.me>
Date: Sat, 5 Oct 2024 16:56:59 -0600
Subject: [PATCH 06/12] renamed FreeMonoid.lean to FreeSemigroup.lean and
 cleaned up inconsistent naming

---
 equational_theories/{FreeMonoid.lean => FreeSemigroup.lean} | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)
 rename equational_theories/{FreeMonoid.lean => FreeSemigroup.lean} (96%)

diff --git a/equational_theories/FreeMonoid.lean b/equational_theories/FreeSemigroup.lean
similarity index 96%
rename from equational_theories/FreeMonoid.lean
rename to equational_theories/FreeSemigroup.lean
index a2f628aba..83ef4223e 100644
--- a/equational_theories/FreeMonoid.lean
+++ b/equational_theories/FreeSemigroup.lean
@@ -118,7 +118,7 @@ theorem AssocImpliesSgrProjFaithful {α : Type _} {G : Type _} [Magma G] (assoc
       apply Eq.trans $ congrArg (fun s ↦ (_ ◇ s) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl2)
       trivial
 
-def insertSemigroupSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
+def insertSgrSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
   match ls with
     | j .+        => if i ≤ j then i ,+ j .+ else j ,+ i .+
     | j ,+ lstail => if i ≤ j then i ,+ j ,+ lstail else j ,+ i ,+ lstail
@@ -126,10 +126,10 @@ def insertSemigroupSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : F
 def insertionSortSgr {n : Nat} (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
   match ls with
     | i .+ => i .+
-    | i ,+ lstail => insertSemigroupSorted i (insertionSortSgr lstail)
+    | i ,+ lstail => insertSgrSorted i (insertionSortSgr lstail)
 
 theorem CommSgrImpliesInsertSortedFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
-  : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (insertSemigroupSorted i ls) = (f i) ◇ evalInSgr f ls :=
+  : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (insertSgrSorted i ls) = (f i) ◇ evalInSgr f ls :=
   fun i ls ↦ match ls with
   | j .+ => by
       have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j .+) (j ,+ i .+)

From 2d4d3394642503c61c5c44a89db1397655da4795 Mon Sep 17 00:00:00 2001
From: Franklin Dyer <franklin+github@dyer.me>
Date: Sat, 5 Oct 2024 18:36:29 -0600
Subject: [PATCH 07/12] changed import from FreeMonoid to FreeSemigroup

---
 equational_theories/Subgraph.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index cbe95b440..f73c0866d 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -4,7 +4,7 @@ import equational_theories.EquationalResult
 import equational_theories.Closure
 import equational_theories.Equations
 import equational_theories.FactsSyntax
-import equational_theories.FreeMonoid
+import equational_theories.FreeSemigroup
 
 /- This is a subproject of the main project to completely describe a small subgraph of the entire
 implication graph. The list of equations under consideration can be found at https://teorth.github.io/equational_theories/blueprint/subgraph-eq.html
@@ -347,7 +347,7 @@ theorem Equation1571_implies_Equation3167 (G : Type _) [Magma G] (h : Equation15
   have eq4512 := Equation1571_implies_Equation4512 G h
   have eq16 := Equation1571_implies_Equation16 G h
   apply Eq.symm
-  apply Eq.trans $ FreeMonoid.AssocFullyRightAssociate eq4512 (fun | 0 => y | 1 => y | 2 => z | 3 => z | 4 => x : Fin 5 → G) ((((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3) ⋆ Lf 4)
+  apply Eq.trans $ AssocFullyRightAssociate eq4512 (fun | 0 => y | 1 => y | 2 => z | 3 => z | 4 => x : Fin 5 → G) ((((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3) ⋆ Lf 4)
   apply Eq.trans $ Eq.symm $ eq16 _ y
   apply Eq.trans $ Eq.symm $ eq16 _ z
   exact Eq.refl _

From b5d45fe3a2cbdee73ef6c6252e6c40227c1d9393 Mon Sep 17 00:00:00 2001
From: Franklin Dyer <franklin+github@dyer.me>
Date: Sun, 6 Oct 2024 21:24:54 -0600
Subject: [PATCH 08/12] finished general-purpose prover that should knock out
 all consequences of Equation1571

---
 equational_theories/AllEquations.lean  |  2 +-
 equational_theories/Equations.lean     |  1 +
 equational_theories/FreeSemigroup.lean | 70 ++++++++++++++++++++------
 equational_theories/Subgraph.lean      | 51 +++++++++++++------
 4 files changed, 92 insertions(+), 32 deletions(-)

diff --git a/equational_theories/AllEquations.lean b/equational_theories/AllEquations.lean
index 365419da5..cf0121ab0 100644
--- a/equational_theories/AllEquations.lean
+++ b/equational_theories/AllEquations.lean
@@ -4674,7 +4674,7 @@ equation 4652 := (x ◇ y) ◇ x = (z ◇ w) ◇ w
 equation 4653 := (x ◇ y) ◇ x = (z ◇ w) ◇ u
 equation 4654 := (x ◇ y) ◇ y = (x ◇ y) ◇ z
 equation 4655 := (x ◇ y) ◇ y = (x ◇ z) ◇ y
-equation 4656 := (x ◇ y) ◇ y = (x ◇ z) ◇ z
+-- equation 4656 := (x ◇ y) ◇ y = (x ◇ z) ◇ z
 equation 4657 := (x ◇ y) ◇ y = (x ◇ z) ◇ w
 equation 4658 := (x ◇ y) ◇ y = (y ◇ x) ◇ x
 equation 4659 := (x ◇ y) ◇ y = (y ◇ x) ◇ z
diff --git a/equational_theories/Equations.lean b/equational_theories/Equations.lean
index 4b44dfde8..eb2b1c8a1 100644
--- a/equational_theories/Equations.lean
+++ b/equational_theories/Equations.lean
@@ -116,6 +116,7 @@ abbrev Equation4579 (G: Type _) [Magma G] := ∀ x y z w u : G, x ◇ (y ◇ z)
 /-- all products of three values are the same, regardless bracketing -/
 abbrev Equation4582 (G: Type _) [Magma G] := ∀ x y z w u v : G, x ◇ (y ◇ z) = (w ◇ u) ◇ v
 
+abbrev Equation4656 (G: Type _) [Magma G] := ∀ x y z : G, (x ◇ y) ◇ y = (x ◇ z) ◇ z
 
 /- Some order 5 laws -/
 
diff --git a/equational_theories/FreeSemigroup.lean b/equational_theories/FreeSemigroup.lean
index 83ef4223e..860f783d7 100644
--- a/equational_theories/FreeSemigroup.lean
+++ b/equational_theories/FreeSemigroup.lean
@@ -132,21 +132,21 @@ theorem CommSgrImpliesInsertSortedFaithful {n : Nat} {G : Type _} [Magma G] (ass
   : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (insertSgrSorted i ls) = (f i) ◇ evalInSgr f ls :=
   fun i ls ↦ match ls with
   | j .+ => by
-      have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j .+) (j ,+ i .+)
-      cases eqor with
-      | inl eq1 => apply Eq.trans (congrArg (evalInSgr f) eq1); exact Eq.refl _
-      | inr eq2 => apply Eq.trans (congrArg (evalInSgr f) eq2); exact comm (f j) (f i)
-    | j ,+ lstail => by
-      have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j ,+ lstail) (j ,+ i ,+ lstail)
-      cases eqor with
-      | inl eq1 =>
-        apply Eq.trans (congrArg (evalInSgr f) eq1);
-        exact Eq.refl _
-      | inr eq2 =>
-        apply Eq.trans (congrArg (evalInSgr f) eq2);
-        apply Eq.trans $ assoc (f j) (f i) _;
-        rw [comm (f j) (f i)];
-        exact Eq.symm $ assoc (f i) (f j) _
+    have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j .+) (j ,+ i .+)
+    cases eqor with
+    | inl eq1 => apply Eq.trans (congrArg (evalInSgr f) eq1); exact Eq.refl _
+    | inr eq2 => apply Eq.trans (congrArg (evalInSgr f) eq2); exact comm (f j) (f i)
+  | j ,+ lstail => by
+    have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j ,+ lstail) (j ,+ i ,+ lstail)
+    cases eqor with
+    | inl eq1 =>
+      apply Eq.trans (congrArg (evalInSgr f) eq1);
+      exact Eq.refl _
+    | inr eq2 =>
+      apply Eq.trans (congrArg (evalInSgr f) eq2);
+      apply Eq.trans $ assoc (f j) (f i) _;
+      rw [comm (f j) (f i)];
+      exact Eq.symm $ assoc (f i) (f j) _
 
 theorem CommSgrImpliesInsertionSortFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
   : ∀ ls : FreeSemigroup (Fin n), evalInSgr f ls = evalInSgr f (insertionSortSgr ls)
@@ -154,3 +154,43 @@ theorem CommSgrImpliesInsertionSortFaithful {n : Nat} {G : Type _} [Magma G] (as
   | i ,+ lstail => Eq.trans
     (congrArg (fun s ↦ (f i) ◇ s) (CommSgrImpliesInsertionSortFaithful assoc comm f lstail))
     (Eq.symm $ CommSgrImpliesInsertSortedFaithful assoc comm f i (insertionSortSgr lstail))
+
+def involutionReduce {α : Type _} [DecidableEq α] (ls : FreeSemigroup α) : FreeSemigroup α :=
+  match ls with
+  | a .+              => a .+
+  | a ,+ b .+         => a ,+ b .+
+  | a ,+ b ,+ lstail  => if (a = b) then involutionReduce lstail else a ,+ involutionReduce (b ,+ lstail)
+
+def InvolutiveImpliesInvolutionReduceFaithful {α : Type _} [DecidableEq α] {G : Type _} [Magma G] (ls : FreeSemigroup α) (invol : Equation16 G) (f : α → G)
+  : evalInSgr f ls = evalInSgr f (involutionReduce ls) :=
+  match ls with
+  | a .+              => Eq.refl _
+  | a ,+ b .+         => Eq.refl _
+  | a ,+ b ,+ lstail  => by
+    have eqor := dite_eq_or_eq (P := a = b) (A := fun _ ↦ involutionReduce lstail) (B := fun _ ↦ a ,+ involutionReduce (b ,+ lstail))
+    cases eqor with
+    | inl eqcase =>
+      apply Eq.trans $ congrArg (fun s ↦ (f s) ◇ (f b ◇ (evalInSgr f lstail))) eqcase.1
+      apply Eq.trans $ Eq.symm $ invol (evalInSgr f lstail) (f b)
+      apply Eq.trans $ InvolutiveImpliesInvolutionReduceFaithful lstail invol f
+      exact Eq.symm $ congrArg (evalInSgr f) eqcase.2
+    | inr neqcase =>
+      apply Eq.symm
+      apply Eq.trans $ congrArg (evalInSgr f) neqcase.2
+      exact congrArg (fun s ↦ f a ◇ s) $ Eq.symm $ InvolutiveImpliesInvolutionReduceFaithful (b ,+ lstail) invol f
+
+def equation1571Reducer {n : Nat} (t : FreeMagma (Fin (n+1))) : FreeSemigroup (Fin (n+1)) :=
+  involutionReduce $ insertionSortSgr $ freeMagmaToFreeSgr (t ⋆ (Lf (Fin.last n) ⋆ Lf (Fin.last n)))
+
+theorem foo : equation1571Reducer (n := 3) (Lf 0) = 0 ,+ 3 ,+ 3 .+ := Eq.refl _
+
+def AbGrpPow2ImpliesEquation1571ReducerFaithful {n : Nat} {G : Type _} [Magma G] (t : FreeMagma (Fin (n+1))) (f : Fin (n+1) → G)
+  (assoc : Equation4512 G) (comm : Equation43 G) (invol : Equation16 G)
+  : evalInMagma f t = evalInSgr f (equation1571Reducer t) := by
+  apply Eq.symm
+  apply Eq.trans $ Eq.symm $ InvolutiveImpliesInvolutionReduceFaithful _ invol f
+  apply Eq.trans $ Eq.symm $ CommSgrImpliesInsertionSortFaithful assoc comm f _
+  apply Eq.trans $ Eq.symm $ AssocImpliesSgrProjFaithful assoc f _
+  apply Eq.trans $ comm (evalInMagma f t) _
+  apply Eq.trans $ Eq.symm $ assoc _ _ _
+  exact Eq.symm $ invol (evalInMagma f t) (f $ Fin.last n)
diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index f73c0866d..d3e880f0d 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -5,6 +5,7 @@ import equational_theories.Closure
 import equational_theories.Equations
 import equational_theories.FactsSyntax
 import equational_theories.FreeSemigroup
+import equational_theories.MagmaLaw
 
 /- This is a subproject of the main project to completely describe a small subgraph of the entire
 implication graph. The list of equations under consideration can be found at https://teorth.github.io/equational_theories/blueprint/subgraph-eq.html
@@ -281,11 +282,11 @@ theorem Lemma_eq1689_implies_h8 (G: Type*) [Magma G] (h: Equation1689 G) : ∀ a
 
 /-- The below results for Equation1571 are out of order because early ones are lemmas for later ones -/
 @[equational_result]
-theorem Equation1571_implies_Equation2662 (G: Type*) [Magma G] (h: Equation1571 G) : Equation2662 G :=
+theorem Equation1571_implies_Equation2662 (G: Type _) [Magma G] (h: Equation1571 G) : Equation2662 G :=
   fun x y ↦ Eq.trans (h x (x ◇ y) (x ◇ y)) (congrArg (fun z ↦ ((x ◇ y) ◇ (x ◇ y)) ◇ z) (Eq.symm $ h x x y))
 
 @[equational_result]
-theorem Equation1571_implies_Equation40 (G: Type*) [Magma G] (h: Equation1571 G) : Equation40 G := by
+theorem Equation1571_implies_Equation40 (G: Type _) [Magma G] (h: Equation1571 G) : Equation40 G := by
   have eq2662 := Equation1571_implies_Equation2662 G h
   have sqRotate : ∀ x y z : G, (x ◇ y) ◇ (x ◇ y) = (y ◇ z) ◇ (y ◇ z)
     := fun x y z ↦ Eq.trans (congrArg (fun w ↦ (x ◇ y) ◇ (x ◇ w)) (eq2662 y z)) (Eq.symm $ h ((y ◇ z) ◇ (y ◇ z)) x y)
@@ -296,7 +297,7 @@ theorem Equation1571_implies_Equation40 (G: Type*) [Magma G] (h: Equation1571 G)
   exact sqConstInImage (x ◇ x) (x ◇ (x ◇ x)) (y ◇ y) (y ◇ (y ◇ y))
 
 @[equational_result]
-theorem Equation1571_implies_Equation23 (G: Type*) [Magma G] (h: Equation1571 G) : Equation23 G := by
+theorem Equation1571_implies_Equation23 (G: Type _) [Magma G] (h: Equation1571 G) : Equation23 G := by
   have eq40 := Equation1571_implies_Equation40 G h
   intro x
   apply Eq.trans $ h x (x ◇ x) (x ◇ x)
@@ -304,7 +305,7 @@ theorem Equation1571_implies_Equation23 (G: Type*) [Magma G] (h: Equation1571 G)
   rw [← eq40 x (x ◇ x)]
 
 @[equational_result]
-theorem Equation1571_implies_Equation8 (G: Type*) [Magma G] (h: Equation1571 G) : Equation8 G := by
+theorem Equation1571_implies_Equation8 (G: Type _) [Magma G] (h: Equation1571 G) : Equation8 G := by
   have eq23 := Equation1571_implies_Equation23 G h
   have eq40 := Equation1571_implies_Equation40 G h
   intro x
@@ -314,7 +315,7 @@ theorem Equation1571_implies_Equation8 (G: Type*) [Magma G] (h: Equation1571 G)
   apply refl _
 
 @[equational_result]
-theorem Equation1571_implies_Equation16 (G: Type*) [Magma G] (h: Equation1571 G) : Equation16 G := by
+theorem Equation1571_implies_Equation16 (G: Type _) [Magma G] (h: Equation1571 G) : Equation16 G := by
   have eq8 := Equation1571_implies_Equation8 G h
   have eq40 := Equation1571_implies_Equation40 G h
   intro x y
@@ -325,7 +326,7 @@ theorem Equation1571_implies_Equation16 (G: Type*) [Magma G] (h: Equation1571 G)
   exact Eq.symm $ (h x y (y ◇ y))
 
 @[equational_result]
-theorem Equation1571_implies_Equation43 (G: Type*) [Magma G] (h: Equation1571 G) : Equation43 G := by
+theorem Equation1571_implies_Equation43 (G: Type _) [Magma G] (h: Equation1571 G) : Equation43 G := by
   have eq16 := Equation1571_implies_Equation16 G h
   have eq23 := Equation1571_implies_Equation23 G h
   have eq40 := Equation1571_implies_Equation40 G h
@@ -334,23 +335,41 @@ theorem Equation1571_implies_Equation43 (G: Type*) [Magma G] (h: Equation1571 G)
   rw [← h x x y, ← eq23 x, ← eq16 y x, eq40 x y, ← eq23 y]
 
 @[equational_result]
-theorem Equation1571_implies_Equation4512 (G: Type*) [Magma G] (h: Equation1571 G) : Equation4512 G := by
+theorem Equation1571_implies_Equation4512 (G: Type _) [Magma G] (h: Equation1571 G) : Equation4512 G := by
   have eq16 := Equation1571_implies_Equation16 G h
   have eq43 := Equation1571_implies_Equation43 G h
   intro x y z
   apply Eq.trans $ h (x ◇ (y ◇ z)) y x
   rw [eq43 (x ◇ (y ◇ z)) x, ← eq16 (y ◇ z) x, ← eq16 z y, eq43 y x]
 
-/-- An example usage of AssocFullyRightAssociate -/
-theorem Equation1571_implies_Equation3167 (G : Type _) [Magma G] (h : Equation1571 G) : Equation3167 G := by
+theorem ProveEquation1571Consequence {n : Nat} {G : Type _} [Magma G] (eq1571 : Equation1571 G)
+  (law : Law.MagmaLaw (Fin (n+1))) (eq : equation1571Reducer law.lhs = equation1571Reducer law.rhs)
+  : G ⊧ law := by
+  have comm := Equation1571_implies_Equation43 G eq1571
+  have assoc := Equation1571_implies_Equation4512 G eq1571
+  have invol := Equation1571_implies_Equation16 G eq1571
+  intro sub
+  apply Eq.trans $ AbGrpPow2ImpliesEquation1571ReducerFaithful law.lhs sub assoc comm invol
+  apply Eq.trans $ congrArg (evalInSgr sub) eq
+  exact Eq.symm $ AbGrpPow2ImpliesEquation1571ReducerFaithful law.rhs sub assoc comm invol
+
+/- Example usage of the general-purpose prover ProveEquation1571Consequence -/
+theorem Equation1571_implies_Equation3167 {G : Type} [Magma G] (h : Equation1571 G) : Equation3167 G := by
   intros x y z
-  have eq4512 := Equation1571_implies_Equation4512 G h
-  have eq16 := Equation1571_implies_Equation16 G h
-  apply Eq.symm
-  apply Eq.trans $ AssocFullyRightAssociate eq4512 (fun | 0 => y | 1 => y | 2 => z | 3 => z | 4 => x : Fin 5 → G) ((((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3) ⋆ Lf 4)
-  apply Eq.trans $ Eq.symm $ eq16 _ y
-  apply Eq.trans $ Eq.symm $ eq16 _ z
-  exact Eq.refl _
+  exact ProveEquation1571Consequence (n := 2)
+      h
+      {lhs := Lf 0, rhs := (((Lf 1 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 2) ⋆ Lf 0}
+      (Eq.refl _)
+      (fun | 0 => x | 1 => y | 2 => z)
+
+/- Example usage of the general-purpose prover ProveEquation1571Consequence -/
+theorem Equation1571_implies_Equation4656 {G : Type} [Magma G] (h : Equation1571 G) : Equation4656 G := by
+  intros x y z
+  exact ProveEquation1571Consequence (n := 2)
+      h
+      {lhs := (Lf 0 ⋆ Lf 1) ⋆ Lf 1, rhs := (Lf 0 ⋆ Lf 2) ⋆ Lf 2}
+      (Eq.refl _)
+      (fun | 0 => x | 1 => y | 2 => z)
 
 /-- This result was first obtained by Kisielewicz in 1997 via computer assistance. -/
 @[equational_result]

From a68732e9a2e740922c0d983a21521cb33a4f8e99 Mon Sep 17 00:00:00 2001
From: Franklin Dyer <franklin+github@dyer.me>
Date: Sun, 6 Oct 2024 23:46:46 -0600
Subject: [PATCH 09/12] removed 'foo'

---
 equational_theories/FreeSemigroup.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/equational_theories/FreeSemigroup.lean b/equational_theories/FreeSemigroup.lean
index 860f783d7..1be24ce25 100644
--- a/equational_theories/FreeSemigroup.lean
+++ b/equational_theories/FreeSemigroup.lean
@@ -182,8 +182,6 @@ def InvolutiveImpliesInvolutionReduceFaithful {α : Type _} [DecidableEq α] {G
 def equation1571Reducer {n : Nat} (t : FreeMagma (Fin (n+1))) : FreeSemigroup (Fin (n+1)) :=
   involutionReduce $ insertionSortSgr $ freeMagmaToFreeSgr (t ⋆ (Lf (Fin.last n) ⋆ Lf (Fin.last n)))
 
-theorem foo : equation1571Reducer (n := 3) (Lf 0) = 0 ,+ 3 ,+ 3 .+ := Eq.refl _
-
 def AbGrpPow2ImpliesEquation1571ReducerFaithful {n : Nat} {G : Type _} [Magma G] (t : FreeMagma (Fin (n+1))) (f : Fin (n+1) → G)
   (assoc : Equation4512 G) (comm : Equation43 G) (invol : Equation16 G)
   : evalInMagma f t = evalInSgr f (equation1571Reducer t) := by

From ee8d70de14b203518a29ef7228af7001a88cf4a5 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 7 Oct 2024 08:30:39 +0200
Subject: [PATCH 10/12] golf proofs

---
 equational_theories/Subgraph.lean | 110 +++++++++++-------------------
 1 file changed, 41 insertions(+), 69 deletions(-)

diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index 8bb86e625..f684a9ab7 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -285,93 +285,65 @@ theorem Lemma_eq1689_implies_h8 (G: Type*) [Magma G] (h: Equation1689 G) : ∀ a
 /-- The below results for Equation1571 are out of order because early ones are lemmas for later ones -/
 @[equational_result]
 theorem Equation1571_implies_Equation2662 (G: Type _) [Magma G] (h: Equation1571 G) : Equation2662 G :=
-  fun x y ↦ Eq.trans (h x (x ◇ y) (x ◇ y)) (congrArg (fun z ↦ ((x ◇ y) ◇ (x ◇ y)) ◇ z) (Eq.symm $ h x x y))
+  fun x y ↦ Eq.trans (h x (x ◇ y) (x ◇ y)) (congrArg (fun z ↦ ((x ◇ y) ◇ (x ◇ y)) ◇ z)
+    (Eq.symm $ h x x y))
 
 @[equational_result]
 theorem Equation1571_implies_Equation40 (G: Type _) [Magma G] (h: Equation1571 G) : Equation40 G := by
-  have eq2662 := Equation1571_implies_Equation2662 G h
-  have sqRotate : ∀ x y z : G, (x ◇ y) ◇ (x ◇ y) = (y ◇ z) ◇ (y ◇ z)
-    := fun x y z ↦ Eq.trans (congrArg (fun w ↦ (x ◇ y) ◇ (x ◇ w)) (eq2662 y z)) (Eq.symm $ h ((y ◇ z) ◇ (y ◇ z)) x y)
-  have sqConstInImage : ∀ x y z w : G, (x ◇ y) ◇ (x ◇ y) = (z ◇ w) ◇ (z ◇ w)
-    := fun x y z w ↦ Eq.trans (sqRotate x y z) (sqRotate y z w)
-  intro x y
-  rw [h x x x, h y y y]
-  exact sqConstInImage (x ◇ x) (x ◇ (x ◇ x)) (y ◇ y) (y ◇ (y ◇ y))
+  have sqRotate : ∀ x y z : G, (x ◇ y) ◇ (x ◇ y) = (y ◇ z) ◇ (y ◇ z) :=
+    fun x y z ↦ Eq.trans (congrArg (fun w ↦ (x ◇ y) ◇ (x ◇ w))
+      (Equation1571_implies_Equation2662 G h y z)) (Eq.symm $ h ((y ◇ z) ◇ (y ◇ z)) x y)
+  have sqConstInImage : ∀ x y z w : G, (x ◇ y) ◇ (x ◇ y) = (z ◇ w) ◇ (z ◇ w) :=
+    fun x y z w ↦ Eq.trans (sqRotate x y z) (sqRotate y z w)
+  exact fun x y ↦ h x x x ▸ h y y y ▸ sqConstInImage (x ◇ x) (x ◇ (x ◇ x)) (y ◇ y) (y ◇ (y ◇ y))
 
 @[equational_result]
 theorem Equation1571_implies_Equation23 (G: Type _) [Magma G] (h: Equation1571 G) : Equation23 G := by
-  have eq40 := Equation1571_implies_Equation40 G h
-  intro x
-  apply Eq.trans $ h x (x ◇ x) (x ◇ x)
-  rw [← h x x x]
-  rw [← eq40 x (x ◇ x)]
-
-@[equational_result]
-theorem Equation1571_implies_Equation8 (G: Type _) [Magma G] (h: Equation1571 G) : Equation8 G := by
-  have eq23 := Equation1571_implies_Equation23 G h
-  have eq40 := Equation1571_implies_Equation40 G h
-  intro x
-  apply Eq.trans $ h x x x
-  apply Eq.trans $ congrArg (fun a ↦ a ◇ (x ◇ (x ◇ x))) (eq40 x (x ◇ (x ◇ x)))
-  apply Eq.trans $ Eq.symm $ eq23 (x ◇ (x ◇ x))
-  apply refl _
-
-@[equational_result]
-theorem Equation1571_implies_Equation16 (G: Type _) [Magma G] (h: Equation1571 G) : Equation16 G := by
-  have eq8 := Equation1571_implies_Equation8 G h
-  have eq40 := Equation1571_implies_Equation40 G h
-  intro x y
-  apply Eq.symm
-  apply Eq.trans $ congrArg (fun w ↦ y ◇ (y ◇ w)) (eq8 x)
-  rw [eq40 x y]
-  apply Eq.trans $ (congrArg (fun w ↦ w ◇ (y ◇ (x ◇ (y ◇ y))))) (eq8 y)
-  exact Eq.symm $ (h x y (y ◇ y))
+  refine fun x ↦ Eq.trans (h x (x ◇ x) (x ◇ x)) ?_
+  rw [← h x x x, ← Equation1571_implies_Equation40 G h x (x ◇ x)]
+
+@[equational_result]
+theorem Equation1571_implies_Equation8 (G: Type _) [Magma G] (h: Equation1571 G) : Equation8 G :=
+  fun x ↦ Eq.trans (h x x x) (((congrArg (fun a ↦ a ◇ (x ◇ (x ◇ x))))
+    (Equation1571_implies_Equation40 G h x (x ◇ (x ◇ x)))).trans
+      (((Equation1571_implies_Equation23 G h (x ◇ (x ◇ x))).symm).trans rfl))
+
+@[equational_result]
+theorem Equation1571_implies_Equation16 (G: Type _) [Magma G] (h: Equation1571 G) : Equation16 G :=
+  fun x y ↦ ((congrArg (fun w ↦ y ◇ (y ◇ w)) (Equation1571_implies_Equation8 G h x)).trans
+    ((Equation1571_implies_Equation40 G h x y ▸ ((congrArg (fun w ↦ w ◇ (y ◇ (x ◇ (y ◇ y)))))
+      (Equation1571_implies_Equation8 G h y)).trans (h x y (y ◇ y)).symm))).symm
 
 @[equational_result]
 theorem Equation1571_implies_Equation43 (G: Type _) [Magma G] (h: Equation1571 G) : Equation43 G := by
-  have eq16 := Equation1571_implies_Equation16 G h
-  have eq23 := Equation1571_implies_Equation23 G h
-  have eq40 := Equation1571_implies_Equation40 G h
-  intro x y
-  apply Eq.trans $ h _ (x ◇ x) (x ◇ (x ◇ y))
-  rw [← h x x y, ← eq23 x, ← eq16 y x, eq40 x y, ← eq23 y]
+  refine fun x y ↦ (h _ (x ◇ x) (x ◇ (x ◇ y))).trans ?_
+  rw [← h x x y, ← Equation1571_implies_Equation23 G h x, ← Equation1571_implies_Equation16 G h y x,
+    Equation1571_implies_Equation40 G h x y, ← Equation1571_implies_Equation23 G h y]
 
 @[equational_result]
 theorem Equation1571_implies_Equation4512 (G: Type _) [Magma G] (h: Equation1571 G) : Equation4512 G := by
-  have eq16 := Equation1571_implies_Equation16 G h
-  have eq43 := Equation1571_implies_Equation43 G h
-  intro x y z
-  apply Eq.trans $ h (x ◇ (y ◇ z)) y x
-  rw [eq43 (x ◇ (y ◇ z)) x, ← eq16 (y ◇ z) x, ← eq16 z y, eq43 y x]
+  refine fun x y z ↦ (h (x ◇ (y ◇ z)) y x).trans ?_
+  rw [Equation1571_implies_Equation43 G h (x ◇ (y ◇ z)) x, ← Equation1571_implies_Equation16 G h (y ◇ z) x, ← Equation1571_implies_Equation16 G h z y, Equation1571_implies_Equation43 G h y x]
 
 theorem ProveEquation1571Consequence {n : Nat} {G : Type _} [Magma G] (eq1571 : Equation1571 G)
-  (law : Law.MagmaLaw (Fin (n+1))) (eq : equation1571Reducer law.lhs = equation1571Reducer law.rhs)
-  : G ⊧ law := by
-  have comm := Equation1571_implies_Equation43 G eq1571
-  have assoc := Equation1571_implies_Equation4512 G eq1571
-  have invol := Equation1571_implies_Equation16 G eq1571
-  intro sub
-  apply Eq.trans $ AbGrpPow2ImpliesEquation1571ReducerFaithful law.lhs sub assoc comm invol
-  apply Eq.trans $ congrArg (evalInSgr sub) eq
-  exact Eq.symm $ AbGrpPow2ImpliesEquation1571ReducerFaithful law.rhs sub assoc comm invol
+    (law : Law.MagmaLaw (Fin (n+1))) (eq : equation1571Reducer law.lhs = equation1571Reducer law.rhs)
+    : G ⊧ law :=
+  fun _ ↦ (AbGrpPow2ImpliesEquation1571ReducerFaithful law.lhs _
+    (Equation1571_implies_Equation4512 G eq1571) (Equation1571_implies_Equation43 G eq1571)
+      (Equation1571_implies_Equation16 G eq1571)).trans ((congrArg (evalInSgr _) eq).trans
+        (AbGrpPow2ImpliesEquation1571ReducerFaithful law.rhs _
+          (Equation1571_implies_Equation4512 G eq1571) (Equation1571_implies_Equation43 G eq1571)
+            (Equation1571_implies_Equation16 G eq1571)).symm)
 
 /- Example usage of the general-purpose prover ProveEquation1571Consequence -/
-theorem Equation1571_implies_Equation3167 {G : Type} [Magma G] (h : Equation1571 G) : Equation3167 G := by
-  intros x y z
-  exact ProveEquation1571Consequence (n := 2)
-      h
-      {lhs := Lf 0, rhs := (((Lf 1 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 2) ⋆ Lf 0}
-      (Eq.refl _)
-      (fun | 0 => x | 1 => y | 2 => z)
+theorem Equation1571_implies_Equation3167 {G : Type} [Magma G] (h : Equation1571 G) : Equation3167 G :=
+  fun x y z ↦ ProveEquation1571Consequence (n := 2) h
+    {lhs := Lf 0, rhs := (((Lf 1 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 2) ⋆ Lf 0} rfl fun | 0 => x | 1 => y | 2 => z
 
 /- Example usage of the general-purpose prover ProveEquation1571Consequence -/
-theorem Equation1571_implies_Equation4656 {G : Type} [Magma G] (h : Equation1571 G) : Equation4656 G := by
-  intros x y z
-  exact ProveEquation1571Consequence (n := 2)
-      h
-      {lhs := (Lf 0 ⋆ Lf 1) ⋆ Lf 1, rhs := (Lf 0 ⋆ Lf 2) ⋆ Lf 2}
-      (Eq.refl _)
-      (fun | 0 => x | 1 => y | 2 => z)
+theorem Equation1571_implies_Equation4656 {G : Type} [Magma G] (h : Equation1571 G) : Equation4656 G :=
+  fun x y z ↦ ProveEquation1571Consequence (n := 2) h
+    {lhs := (Lf 0 ⋆ Lf 1) ⋆ Lf 1, rhs := (Lf 0 ⋆ Lf 2) ⋆ Lf 2} rfl fun | 0 => x | 1 => y | 2 => z
 
 /-- This result was first obtained by Kisielewicz in 1997 via computer assistance. -/
 @[equational_result]

From 0cc5fe6fcf1978142b9405de81cbf250280926c0 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 7 Oct 2024 08:35:42 +0200
Subject: [PATCH 11/12] Update Subgraph.lean

---
 equational_theories/Subgraph.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index f684a9ab7..eb4ba827a 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -299,7 +299,7 @@ theorem Equation1571_implies_Equation40 (G: Type _) [Magma G] (h: Equation1571 G
 
 @[equational_result]
 theorem Equation1571_implies_Equation23 (G: Type _) [Magma G] (h: Equation1571 G) : Equation23 G := by
-  refine fun x ↦ Eq.trans (h x (x ◇ x) (x ◇ x)) ?_
+  refine fun x ↦ (h x (x ◇ x) (x ◇ x)).trans ?_
   rw [← h x x x, ← Equation1571_implies_Equation40 G h x (x ◇ x)]
 
 @[equational_result]

From 3ca9ebb70abd1f15f20f7ba44a6155c05bdb6213 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 7 Oct 2024 08:36:08 +0200
Subject: [PATCH 12/12] Update Subgraph.lean

---
 equational_theories/Subgraph.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index eb4ba827a..a829dcbd2 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -323,7 +323,9 @@ theorem Equation1571_implies_Equation43 (G: Type _) [Magma G] (h: Equation1571 G
 @[equational_result]
 theorem Equation1571_implies_Equation4512 (G: Type _) [Magma G] (h: Equation1571 G) : Equation4512 G := by
   refine fun x y z ↦ (h (x ◇ (y ◇ z)) y x).trans ?_
-  rw [Equation1571_implies_Equation43 G h (x ◇ (y ◇ z)) x, ← Equation1571_implies_Equation16 G h (y ◇ z) x, ← Equation1571_implies_Equation16 G h z y, Equation1571_implies_Equation43 G h y x]
+  rw [Equation1571_implies_Equation43 G h (x ◇ (y ◇ z)) x,
+    ← Equation1571_implies_Equation16 G h (y ◇ z) x, ← Equation1571_implies_Equation16 G h z y,
+    Equation1571_implies_Equation43 G h y x]
 
 theorem ProveEquation1571Consequence {n : Nat} {G : Type _} [Magma G] (eq1571 : Equation1571 G)
     (law : Law.MagmaLaw (Fin (n+1))) (eq : equation1571Reducer law.lhs = equation1571Reducer law.rhs)