Add equations of 1 variable and their implications

blueprint/src/chapter/equations.tex

@@ -24,6 +24,9 @@ \chapter{Equations}
 \begin{definition}[Equation 8]\label{eq8}\lean{Equation8}\leanok\uses{magma-def}  Equation 8 is the law $x=x \circ (x \circ x)$.
 \end{definition}
 
+\begin{definition}[Equation 23]\label{eq23}\lean{Equation23}\leanok\uses{magma-def}  Equation 23 is the law $x = (x \circ x) \circ x$.
+\end{definition}
+
 \begin{definition}[Equation 38]\label{eq38}\lean{Equation38}\leanok\uses{magma-def}  Equation 38 is the law $x \circ x = x \circ y$.
 \end{definition}
 
@@ -45,12 +48,93 @@ \chapter{Equations}
 \begin{definition}[Equation 46]\label{eq46}\lean{Equation46}\leanok\uses{magma-def}  Equation 46 is the law $x \circ y = z \circ w$.
 \end{definition}
 
+\begin{definition}[Equation 47]\label{eq47}\lean{Equation47}\leanok\uses{magma-def}  Equation 47 is the law $x = x \circ (x \circ (x \circ x))$.
+\end{definition}
+
+\begin{definition}[Equation 99]\label{eq99}\lean{Equation99}\leanok\uses{magma-def}  Equation 99 is the law $x = x \circ ((x \circ x) \circ x)$.
+\end{definition}
+
+\begin{definition}[Equation 151]\label{eq151}\lean{Equation151}\leanok\uses{magma-def}  Equation 151 is the law $x = (x \circ x) \circ (x \circ x)$.
+\end{definition}
+
 \begin{definition}[Equation 168]\label{eq168}\lean{Equation168}\leanok\uses{magma-def}  Equation 168 is the law $x = (y \circ x) \circ (x \circ z)$.
 \end{definition}
 
+\begin{definition}[Equation 203]\label{eq203}\lean{Equation203}\leanok\uses{magma-def}  Equation 203 is the law $x = (x \circ (x \circ x)) \circ x$.
+\end{definition}
+
+\begin{definition}[Equation 255]\label{eq255}\lean{Equation255}\leanok\uses{magma-def}  Equation 255 is the law $x = ((x \circ x) \circ x) \circ x$.
+\end{definition}
+
+\begin{definition}[Equation 307]\label{eq307}\lean{Equation307}\leanok\uses{magma-def}  Equation 307 is the law $x \circ x = x \circ (x \circ x)$.
+\end{definition}
+
+\begin{definition}[Equation 359]\label{eq359}\lean{Equation359}\leanok\uses{magma-def}  Equation 359 is the law $x \circ x = (x \circ x) \circ x$.
+\end{definition}
+
 \begin{definition}[Equation 387]\label{eq387}\lean{Equation387}\leanok\uses{magma-def}  Equation 387 is the law $x \circ y = (y \circ y) \circ x$.
 \end{definition}
 
+\begin{definition}[Equation 411]\label{eq411}\lean{Equation411}\leanok\uses{magma-def}  Equation 411 is the law $x = x \circ (x \circ (x \circ (x \circ x)))$.
+\end{definition}
+
+\begin{definition}[Equation 614]\label{eq614}\lean{Equation614}\leanok\uses{magma-def}  Equation 614 is the law $x = x \circ (x \circ ((x \circ x) \circ x))$.
+\end{definition}
+
+\begin{definition}[Equation 817]\label{eq817}\lean{Equation817}\leanok\uses{magma-def}  Equation 817 is the law $x = x \circ ((x \circ x) \circ (x \circ x))$.
+\end{definition}
+
+\begin{definition}[Equation 1020]\label{eq1020}\lean{Equation1020}\leanok\uses{magma-def}  Equation 1020 is the law $x = x \circ ((x \circ (x \circ x)) \circ x)$.
+\end{definition}
+
+\begin{definition}[Equation 1223]\label{eq1223}\lean{Equation1223}\leanok\uses{magma-def}  Equation 1223 is the law $x = x \circ (((x \circ x) \circ x) \circ x)$.
+\end{definition}
+
+\begin{definition}[Equation 1426]\label{eq1426}\lean{Equation1426}\leanok\uses{magma-def}  Equation 1426 is the law $x = (x \circ x) \circ (x \circ (x \circ x))$.
+\end{definition}
+
+\begin{definition}[Equation 1629]\label{eq1629}\lean{Equation1629}\leanok\uses{magma-def}  Equation 1629 is the law $x = (x \circ x) \circ ((x \circ x) \circ x)$.
+\end{definition}
+
+\begin{definition}[Equation 1832]\label{eq1832}\lean{Equation1832}\leanok\uses{magma-def}  Equation 1832 is the law $x = (x \circ (x \circ x)) \circ (x \circ x)$.
+\end{definition}
+
+\begin{definition}[Equation 2035]\label{eq2035}\lean{Equation2035}\leanok\uses{magma-def}  Equation 2035 is the law $x = ((x \circ x) \circ x) \circ (x \circ x)$.
+\end{definition}
+
+\begin{definition}[Equation 2238]\label{eq2238}\lean{Equation2238}\leanok\uses{magma-def}  Equation 2238 is the law $x = (x \circ (x \circ (x \circ x))) \circ x$.
+\end{definition}
+
+\begin{definition}[Equation 2441]\label{eq2441}\lean{Equation2441}\leanok\uses{magma-def}  Equation 2441 is the law $x = (x \circ ((x \circ x) \circ x)) \circ x$.
+\end{definition}
+
+\begin{definition}[Equation 2644]\label{eq2644}\lean{Equation2644}\leanok\uses{magma-def}  Equation 2644 is the law $x = ((x \circ x) \circ (x \circ x)) \circ x$.
+\end{definition}
+
+\begin{definition}[Equation 2847]\label{eq2847}\lean{Equation2847}\leanok\uses{magma-def}  Equation 2847 is the law $x = ((x \circ (x \circ x)) \circ x) \circ x$.
+\end{definition}
+
+\begin{definition}[Equation 3050]\label{eq3050}\lean{Equation3050}\leanok\uses{magma-def}  Equation 3050 is the law $x = (((x \circ x) \circ x) \circ x) \circ x$.
+\end{definition}
+
+\begin{definition}[Equation 3253]\label{eq3253}\lean{Equation3253}\leanok\uses{magma-def}  Equation 3253 is the law $x \circ x = x \circ (x \circ (x \circ x))$.
+\end{definition}
+
+\begin{definition}[Equation 3456]\label{eq3456}\lean{Equation3456}\leanok\uses{magma-def}  Equation 3456 is the law $x \circ x = x \circ ((x \circ x) \circ x)$.
+\end{definition}
+
+\begin{definition}[Equation 3659]\label{eq3659}\lean{Equation3659}\leanok\uses{magma-def}  Equation 3659 is the law $x \circ x = (x \circ x) \circ (x \circ x)$.
+\end{definition}
+
+\begin{definition}[Equation 3862]\label{eq3862}\lean{Equation3862}\leanok\uses{magma-def}  Equation 3862 is the law $x \circ x = (x \circ (x \circ x)) \circ x$.
+\end{definition}
+
+\begin{definition}[Equation 4065]\label{eq4065}\lean{Equation4065}\leanok\uses{magma-def}  Equation 4065 is the law $x \circ x = ((x \circ x) \circ x) \circ x$.
+\end{definition}
+
+\begin{definition}[Equation 4380]\label{eq4380}\lean{Equation4380}\leanok\uses{magma-def}  Equation 4380 is the law $x \circ (x \circ x) = (x \circ x) \circ x$.
+\end{definition}
+
 \begin{definition}[Equation 4512]\label{eq4512}\lean{Equation4512}\leanok\uses{magma-def}  Equation 4512 is the law $x \circ (y \circ z) = (x \circ y) \circ z$.
 \end{definition}
 

equational_theories/Basic.lean

@@ -36,6 +36,8 @@ def Equation7 (G: Type*) [Magma G] := ∀ x y z : G, x = y ∘ z
 
 def Equation8 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ x)
 
+def Equation23 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ x) ∘ x
+
 /-- value of multiplication is independent of right argument -/
 def Equation38 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = x ∘ y
 
@@ -57,11 +59,65 @@ def Equation43 (G: Type*) [Magma G] := ∀ x y : G, x ∘ y = y ∘ x
 /-- The constant law -/
 def Equation46 (G: Type*) [Magma G] := ∀ x y z w : G, x ∘ y = z ∘ w
 
+def Equation47 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ (x ∘ x))
+
+def Equation99 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ ((x ∘ x) ∘ x)
+
+def Equation151 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ x) ∘ (x ∘ x)
+
 /-- The central groupoid law -/
 def Equation168 (G: Type*) [Magma G] := ∀ x y z : G, x = (y ∘ x) ∘ (x ∘ z)
 
+def Equation203 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ (x ∘ x)) ∘ x
+
+def Equation255 (G: Type*) [Magma G] := ∀ x : G, x = ((x ∘ x) ∘ x) ∘ x
+
+def Equation307 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = x ∘ (x ∘ x)
+
+def Equation359 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = (x ∘ x) ∘ x
+
 def Equation387 (G: Type*) [Magma G] := ∀ x y : G, x ∘ y = (y ∘ y) ∘ x
 
+def Equation411 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ (x ∘ (x ∘ x)))
+
+def Equation614 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ ((x ∘ x) ∘ x))
+
+def Equation817 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ ((x ∘ x) ∘ (x ∘ x))
+
+def Equation1020 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ ((x ∘ (x ∘ x)) ∘ x)
+
+def Equation1223 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (((x ∘ x) ∘ x) ∘ x)
+
+def Equation1426 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ x) ∘ (x ∘ (x ∘ x))
+
+def Equation1629 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ x) ∘ ((x ∘ x) ∘ x)
+
+def Equation1832 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ (x ∘ x)) ∘ (x ∘ x)
+
+def Equation2035 (G: Type*) [Magma G] := ∀ x : G, x = ((x ∘ x) ∘ x) ∘ (x ∘ x)
+
+def Equation2238 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ (x ∘ (x ∘ x))) ∘ x
+
+def Equation2441 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ ((x ∘ x) ∘ x)) ∘ x
+
+def Equation2644 (G: Type*) [Magma G] := ∀ x : G, x = ((x ∘ x) ∘ (x ∘ x)) ∘ x
+
+def Equation2847 (G: Type*) [Magma G] := ∀ x : G, x = ((x ∘ (x ∘ x)) ∘ x) ∘ x
+
+def Equation3050 (G: Type*) [Magma G] := ∀ x : G, x = (((x ∘ x) ∘ x) ∘ x) ∘ x
+
+def Equation3253 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = x ∘ (x ∘ (x ∘ x))
+
+def Equation3456 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = x ∘ ((x ∘ x) ∘ x)
+
+def Equation3659 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = (x ∘ x) ∘ (x ∘ x)
+
+def Equation3862 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = (x ∘ (x ∘ x)) ∘ x
+
+def Equation4065 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = ((x ∘ x) ∘ x) ∘ x
+
+def Equation4380 (G: Type*) [Magma G] := ∀ x : G, x ∘ (x ∘ x) = (x ∘ x) ∘ x
+
 /-- The associative law -/
 def Equation4512 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ (y ∘ z) = (x ∘ y) ∘ z
 
@@ -90,6 +146,82 @@ theorem Equation2_implies_Equation7 (G: Type*) [Magma G] (h: Equation2 G) : Equa
 theorem Equation2_implies_Equation46 (G: Type*) [Magma G] (h: Equation2 G) : Equation46 G :=
   fun _ _ _ _ => h _ _
 
+theorem Equation3_implies_Equation8 (G: Type*) [Magma G] (h: Equation3 G) : Equation8 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation3_implies_Equation23 (G: Type*) [Magma G] (h: Equation3 G) : Equation23 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation3_implies_Equation47 (G: Type*) [Magma G] (h: Equation3 G) : Equation47 G := by
+  intro x
+  rw [<-h, <-h, <-h]
+
+theorem Equation3_implies_Equation99 (G: Type*) [Magma G] (h: Equation3 G) : Equation99 G := by
+  intro x
+  rw [<-h, <-h, <-h]
+
+theorem Equation3_implies_Equation151 (G: Type*) [Magma G] (h: Equation3 G) : Equation151 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation3_implies_Equation203 (G: Type*) [Magma G] (h: Equation3 G) : Equation203 G := by
+  intro x
+  rw [<-h, <-h, <-h]
+
+theorem Equation3_implies_Equation255 (G: Type*) [Magma G] (h: Equation3 G) : Equation255 G := by
+  intro x
+  rw [<-h, <-h, <-h]
+
+theorem Equation3_implies_Equation307 (G: Type*) [Magma G] (h: Equation3 G) : Equation307 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation3_implies_Equation359 (G: Type*) [Magma G] (h: Equation3 G) : Equation359 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation3_implies_Equation614 (G: Type*) [Magma G] (h: Equation3 G) : Equation614 G := by
+  intro x
+  rw [<-h, <-h, <-h, <-h]
+
+theorem Equation3_implies_Equation817 (G: Type*) [Magma G] (h: Equation3 G) : Equation817 G := by
+  intro x
+  rw [<-h, <-h, <-h]
+
+theorem Equation3_implies_Equation1223 (G: Type*) [Magma G] (h: Equation3 G) : Equation1223 G := by
+  intro x
+  rw [<-h, <-h, <-h, <-h]
+
+theorem Equation3_implies_Equation1426 (G: Type*) [Magma G] (h: Equation3 G) : Equation1426 G := by
+  intro x
+  rw [<-h, <-h, <-h]
+
+theorem Equation3_implies_Equation2035 (G: Type*) [Magma G] (h: Equation3 G) : Equation2035 G := by
+  intro x
+  rw [<-h, <-h, <-h]
+
+theorem Equation3_implies_Equation2238 (G: Type*) [Magma G] (h: Equation3 G) : Equation2238 G := by
+  intro x
+  rw [<-h, <-h, <-h, <-h]
+
+theorem Equation3_implies_Equation2644 (G: Type*) [Magma G] (h: Equation3 G) : Equation2644 G := by
+  intro x
+  rw [<-h, <-h, <-h]
+
+theorem Equation3_implies_Equation2847 (G: Type*) [Magma G] (h: Equation3 G) : Equation2847 G := by
+  intro x
+  rw [<-h, <-h, <-h, <-h]
+
+theorem Equation3_implies_Equation3659 (G: Type*) [Magma G] (h: Equation3 G) : Equation3659 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation3_implies_Equation4380 (G: Type*) [Magma G] (h: Equation3 G) : Equation4380 G := by
+  intro x
+  rw [<-h]
+
 theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equation2 G := by
   intro a b
   rw [h a a, ← h b]
@@ -110,6 +242,46 @@ theorem Equation4_implies_Equation4522 (G: Type*) [Magma G] (h: Equation4 G) : E
   intro x y z w u
   rw [<-h, <-h, <-h]
 
+theorem Equation8_implies_Equation411 (G: Type*) [Magma G] (h: Equation8 G) : Equation411 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation8_implies_Equation1020 (G: Type*) [Magma G] (h: Equation8 G) : Equation1020 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation8_implies_Equation1832 (G: Type*) [Magma G] (h: Equation8 G) : Equation1832 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation8_implies_Equation3253 (G: Type*) [Magma G] (h: Equation8 G) : Equation3253 G := by
+  intro x
+  rw [<-h]
+
+theorem Equation8_implies_Equation3862 (G: Type*) [Magma G] (h: Equation8 G) : Equation3862 G := by
+  intro x
+  rw [<-h]
+
+theorem Equation23_implies_Equation1629 (G: Type*) [Magma G] (h: Equation23 G) : Equation1629 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation23_implies_Equation2441 (G: Type*) [Magma G] (h: Equation23 G) : Equation2441 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation23_implies_Equation3050 (G: Type*) [Magma G] (h: Equation23 G) : Equation3050 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation23_implies_Equation3456 (G: Type*) [Magma G] (h: Equation23 G) : Equation3456 G := by
+  intro x
+  rw [<-h]
+
+theorem Equation23_implies_Equation4065 (G: Type*) [Magma G] (h: Equation23 G) : Equation4065 G := by
+  intro x
+  rw [<-h]
+
 theorem Equation46_implies_Equation42 (G: Type*) [Magma G] (h: Equation46 G) : Equation42 G :=
   fun _ _ _ => h _ _ _ _
 
@@ -119,6 +291,14 @@ theorem Equation46_implies_Equation387 (G: Type*) [Magma G] (h: Equation46 G) :
 theorem Equation46_implies_Equation4582 (G: Type*) [Magma G] (h: Equation46 G) : Equation4582 G :=
   fun _ _ _ _ _ _ => h _ _ _ _
 
+theorem Equation307_implies_Equation3253 (G: Type*) [Magma G] (h: Equation307 G) : Equation3253 G := by
+  intro x
+  rw [<-h, <-h]
+
+theorem Equation359_implies_Equation4065 (G: Type*) [Magma G] (h: Equation359 G) : Equation4065 G := by
+  intro x
+  rw [<-h, <-h]
+
 /-- This proof is from https://mathoverflow.net/a/450905/766 -/
 theorem Equation387_implies_Equation43 (G: Type*) [Magma G] (h: Equation387 G) : Equation43 G := by
   have idem (x : G) : (x ∘ x) ∘ (x ∘ x) = (x ∘ x) := by