prove e6 and e7 equiv to e2 (#11)

* prove e6 and e7 equiv to e2

* mark proofs as complete

blueprint/src/chapter/implications.tex

@@ -29,14 +29,14 @@ \chapter{Implications}
 \begin{theorem}[7 equivalent to 2]\label{7_equiv_2}\uses{eq2,eq7}\lean{Equation7_implies_Equation2, Equation2_implies_Equation7}\leanok  Definition \ref{eq7} is equivalent to Definition \ref{eq2}.
 \end{theorem}
 
-\begin{proof}
+\begin{proof}\leanok
   When $x = y * z$, obviously $x = y$ because $x = x * x$ and $y = x * x$. the other way around is trivial.
 \end{proof}
 
 \begin{theorem}[6 equivalent to 2]\label{6_equiv_2}\uses{eq2,eq6}\lean{Equation6_implies_Equation2, Equation2_implies_Equation6}\leanok  Definition \ref{eq6} is equivalent to Definition \ref{eq2}.
 \end{theorem}
 
-\begin{proof}  Similar to the previous argument.
+\begin{proof}\leanok  Similar to the previous argument.
 \end{proof}
 
 More generally, any equation of the form $x = f(y,z,w,u,v)$ is equivalent to Equation 2 (eventually once we have enough API for Magma relations, we could formalize this general claim rather than establish it on a case by case basis).  It is also trivial that Equation 2 implies every other equation.

equational_theories/Basic.lean

@@ -73,19 +73,21 @@ theorem Equation2_implies_Equation4 (G: Type*) [Magma G] (h: Equation2 G) : Equa
   fun _ _ => h _ _
 
 theorem Equation2_implies_Equation6 (G: Type*) [Magma G] (h: Equation2 G) : Equation6 G :=
-  sorry
+  fun _ _ => h _ _
 
 theorem Equation2_implies_Equation7 (G: Type*) [Magma G] (h: Equation2 G) : Equation7 G :=
-  sorry
+  fun _ _ _ => h _ _
 
 theorem Equation2_implies_Equation46 (G: Type*) [Magma G] (h: Equation2 G) : Equation46 G :=
   fun _ _ _ _ => h _ _
 
-theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equation2 G :=
-  sorry
+theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equation2 G := by
+  intro a b
+  rw [h a a, ← h b]
 
-theorem Equation7_implies_Equation2 (G: Type*) [Magma G] (h: Equation7 G) : Equation2 G :=
-  sorry
+theorem Equation7_implies_Equation2 (G: Type*) [Magma G] (h: Equation7 G) : Equation2 G := by
+  intro a b
+  rw [h a a a, ←h b]
 
 theorem Equation4_implies_Equation3 (G: Type*) [Magma G] (h: Equation4 G) : Equation3 G := by
   intro _