2 files changed, 74 insertions, 23 deletions
diff --git a/library/relation/closure.tex b/library/relation/closure.tex
index 8eebf08..0734685 100644
--- a/library/relation/closure.tex
+++ b/library/relation/closure.tex
@@ -11,6 +11,9 @@
 \begin{proposition}\label{reflexive_closure_is_reflexive}
     $\reflexiveClosure{X}{R}$ is reflexive on $X$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{reflexive_closure,reflexive_on,union_iff,id_iff}.
+\end{proof}
 
 \begin{definition}\label{reflexive_reduction}
     $\reflexiveReduction{X}{R} = R\setminus\identity{X}$.
diff --git a/library/relation/equivalence.tex b/library/relation/equivalence.tex
index f8b1ba7..896ca57 100644
--- a/library/relation/equivalence.tex
+++ b/library/relation/equivalence.tex
@@ -16,6 +16,9 @@
     Let $E$ be a partial equivalence.
     Then $E$ is quasireflexive.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{quasireflexive,symmetric,transitive}.
+\end{proof}
 
 \begin{abbreviation}\label{equivalence}
     $E$ is an equivalence iff
@@ -88,6 +91,12 @@
     Then $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$.
 \end{proposition}
 \begin{proof}
+    We have for all $c\in\equivalenceClass{E}{a}$
+        we have $c\in\equivalenceClass{E}{b}$
+        by \cref{downward_closure_iff,transitive}.
+    We have for all $c\in\equivalenceClass{E}{b}$
+        we have $c\in\equivalenceClass{E}{a}$
+        by \cref{downward_closure_iff,symmetric,transitive}.
     Follows by set extensionality.
 \end{proof}
 
@@ -97,12 +106,20 @@
     Suppose $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$.
     Then $a\mathrel{E} b$.
 \end{proposition}
+\begin{proof}
+    $a\in\equivalenceClass{E}{a}$ by \cref{equivclasses_inhabited_equivalenceon}.
+    Thus $a\in\equivalenceClass{E}{b}$.
+    Follows by \cref{downward_closure_iff}.
+\end{proof}
 
 \begin{proposition}\label{equiv_iff_equivclasses_eq}
     Let $E$ be an equivalence on $A$.
     Let $a, b\in A$.
     Then $a\mathrel{E} b$ iff $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{equiv_implies_equivanlence_classes_eq,equivclasses_eq_implies_equiv}.
+\end{proof}
 
 \begin{proposition}\label{equivclasses_diseq_implies_disjoint}
     Let $E$ be a partial equivalence.
@@ -110,21 +127,28 @@
     Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$.
 \end{proposition}
 \begin{proof}
-    Suppose not.
-    Take $c$ such that $c\in \equivalenceClass{E}{a},\equivalenceClass{E}{b}$.
-    Then $c\mathrel{E} a$ and
-         $c\mathrel{E} b$.
-    $E$ is symmetric.
-    Thus $a\mathrel{E} c$ by \hyperref[symmetric]{symmetry}.
-    $E$ is transitive.
-    Thus $a\mathrel{E} b$ by \hyperref[transitive]{transitivity}.
-    Then $b\mathrel{E} a$ by \hyperref[symmetric]{symmetry}.
-    %
-    Thus $a\in \equivalenceClass{E}{b}$ and $b\in \equivalenceClass{E}{a}$
-        by \cref{downward_closure_iff}.
-    Hence $\equivalenceClass{E}{a}\subseteq \equivalenceClass{E}{b}\subseteq \equivalenceClass{E}{a}$
-        by \cref{transitive_downward_subseteq}.
-    Contradiction by \cref{subseteq_antisymmetric}.
+    Show there exists no $c$ such that
+        $c\in\equivalenceClass{E}{a}$ and
+        $c\in\equivalenceClass{E}{b}$.
+    \begin{subproof}
+        Assume there exists a set $c$ such that
+            $c\in\equivalenceClass{E}{a}$ and
+            $c\in\equivalenceClass{E}{b}$.
+        Take $c$ such that $c\in\equivalenceClass{E}{a}$ and
+            $c\in\equivalenceClass{E}{b}$ by assumption.
+        We have $c\mathrel{E}a$ and $c\mathrel{E}b$
+            by \cref{downward_closure_iff}.
+        Thus $a\mathrel{E}c$ and $b\mathrel{E}c$ by \cref{symmetric}.
+        Thus $a\mathrel{E}b$ and $b\mathrel{E}a$ by \cref{transitive}.
+        Hence $\equivalenceClass{E}{a}\subseteq\equivalenceClass{E}{b}$
+            by \cref{downward_closure_iff,transitive_downward_subseteq}.
+        We have $\equivalenceClass{E}{b}\subseteq\equivalenceClass{E}{a}$
+            by \cref{downward_closure_iff,transitive_downward_subseteq}.
+        Thus $\equivalenceClass{E}{a}=\equivalenceClass{E}{b}$
+            by \cref{subseteq_antisymmetric}.
+        Contradiction by assumption.
+    \end{subproof}
+    Follows by \cref{disjoint}.
 \end{proof}
 
 \begin{corollary}\label{equivalence_equivclasses_diseq_implies_disjoint}
@@ -159,6 +183,13 @@
 \begin{proposition}\label{quotient_emptyset}
     $\quotient{\emptyset}{\emptyset} = \emptyset$.
 \end{proposition}
+\begin{proof}
+    We have for all $C\in\quotient{\emptyset}{\emptyset}$
+        we have $C\in\emptyset$ by \cref{quotient,emptyset}.
+    We have for all $C\in\emptyset$
+        we have $C\in\quotient{\emptyset}{\emptyset}$ by \cref{emptyset}.
+    Follows by set extensionality.
+\end{proof}
 
 
 \begin{proposition}\label{quotient_elems_disjoint}
@@ -167,8 +198,8 @@
     Then $B$ is disjoint from $C$.
 \end{proposition}
 \begin{proof}
-    Take $b$ such that $B = \equivalenceClass{E}{b}$.
-    Take $c$ such that $C = \equivalenceClass{E}{c}$.
+    Take $b$ such that $b\in A$ and $B = \equivalenceClass{E}{b}$ by \cref{quotient}.
+    Take $c$ such that $c\in A$ and $C = \equivalenceClass{E}{c}$ by \cref{quotient}.
     Then $B$ is disjoint from $C$ by \cref{equivalenceon_equivclasses_diseq_implies_disjoint}.
 \end{proof}
 
@@ -178,8 +209,8 @@
     Then $C$ is inhabited.
 \end{proposition}
 \begin{proof}
-    Take $a\in A$ such that $C = \equivalenceClass{E}{a}$.
-    Then $a\in \equivalenceClass{E}{a}$.
+    Take $a$ such that $a\in A$ and $C = \equivalenceClass{E}{a}$ by \cref{quotient}.
+    Then $a\in \equivalenceClass{E}{a}$ by \cref{equivclasses_inhabited_equivalenceon}.
     $C$ is inhabited by \cref{quotient,equivclasses_inhabited}.
 \end{proof}
 
@@ -189,7 +220,7 @@
     Then $a\in A$.
 \end{proposition}
 \begin{proof}
-    Take $b\in A$ such that $C = \equivalenceClass{E}{b}$
+    Take $b$ such that $b\in A$ and $C = \equivalenceClass{E}{b}$
         by \cref{quotient}.
     Then $a\mathrel{E} b$.
     Thus $a\in A$ by \cref{times_tuple_elim,subseteq}.
@@ -200,14 +231,19 @@
     Let $E$ be an equivalence on $A$.
     $\emptyset\notin\quotient{A}{E}$.
 \end{corollary}
+\begin{proof}
+    Follows by \cref{quotient_elems_inhabited,emptyset}.
+\end{proof}
 
 \begin{proposition}\label{quotient_partition}
     Let $E$ be an equivalence on $A$.
     $\quotient{A}{E}$ is a partition.
 \end{proposition}
 \begin{proof}
-    $\emptyset\notin\quotient{A}{E}$.
-    For all $B, C\in \quotient{A}{E}$ such that $B\neq C$ we have $B$ is disjoint from $C$.
+    $\emptyset\notin\quotient{A}{E}$ by \cref{quotient_notni_emptyset}.
+    For all $B, C\in \quotient{A}{E}$ such that $B\neq C$
+        we have $B$ is disjoint from $C$ by \cref{quotient_elems_disjoint}.
+    Follows by \cref{partition}.
 \end{proof}
 
 \begin{proposition}\label{quotient_partition_of}
@@ -215,7 +251,13 @@
     $\quotient{A}{E}$ is a partition of $A$.
 \end{proposition}
 \begin{proof}
-    $\unions{(\quotient{A}{E})} = A$ by set extensionality.
+    We have for all $a\in\unions{(\quotient{A}{E})}$
+        we have $a\in A$ by \cref{unions_iff,quotient_elems_type}.
+    We have for all $a\in A$
+        we have $a\in\unions{(\quotient{A}{E})}$
+        by \cref{unions_iff,quotient,equivclasses_inhabited_equivalenceon}.
+    Thus $\unions{(\quotient{A}{E})} = A$ by set extensionality.
+    Follows by \cref{quotient_partition}.
 \end{proof}
 
 
@@ -230,11 +272,17 @@
     Suppose $a,b\in C\in P$.
     Then $a\mathrel{\equivfrompartition{P}{A}} b$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{equivalence_from_partition}.
+\end{proof}
 
 \begin{proposition}\label{equivalence_from_partition_reflexive}
     Let $P$ be a partition of $A$.
     $\equivfrompartition{P}{A}$ is reflexive on $A$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{reflexive_on,equivalence_from_partition_intro,partition,unions_iff}.
+\end{proof}
 
 \begin{proposition}\label{equivalence_from_partition_symmetric}
     Let $P$ be a partition.