Simplify exact function proofs

1 files changed, 6 insertions, 36 deletions

diff --git a/library/function.tex b/library/function.tex
index 8ae3759..5d2839f 100644
--- a/library/function.tex
+++ b/library/function.tex
@@ -78,18 +78,8 @@
     Then $f\subseteq g$.
 \end{proposition}
 \begin{proof}
-    For all $x,y$ such that $(x,y)\in f$ we have $x\in\dom{f}$
-        by \cref{dom_iff}.
-    For all $x,y$ such that $(x,y)\in f$ we have $x\in\dom{g}$
-        by \cref{subseteq}.
-    For all $x,y$ such that $(x,y)\in f$ we have $f(x) = y$
-        by \cref{function_apply_intro}.
-    For all $x,y$ such that $(x,y)\in f$ we have $f(x) = g(x)$
-        by assumption.
-    For all $x,y$ such that $(x,y)\in f$ we have $(x,g(x))\in g$
-        by \cref{function_apply_elim}.
     For all $x,y$ such that $(x,y)\in f$ we have $(x,y)\in g$
-        by assumption.
+        by \cref{dom_iff,subseteq,function_apply_intro,function_apply_elim}.
     Follows by \cref{subseteq,relation}.
 \end{proof}
 
@@ -100,12 +90,7 @@
     Then $f = g$.
 \end{proposition}
 \begin{proof}
-    $\dom{f}\subseteq \dom{g}$ by \cref{subseteq}.
-    $\dom{g}\subseteq \dom{f}$ by \cref{subseteq}.
-    For all $x\in\dom{f}$ we have $f(x) = g(x)$ by assumption.
-    Thus $f\subseteq g$ by \cref{fun_subseteq}.
-    For all $x\in\dom{g}$ we have $f(x) = g(x)$ by assumption.
-    Thus $g\subseteq f$ by \cref{fun_subseteq}.
+    $f\subseteq g$ and $g\subseteq f$ by \cref{fun_subseteq,subseteq}.
     Follows by \cref{subseteq_antisymmetric}.
 \end{proof}
 
@@ -286,11 +271,7 @@
     $\img{f}{X} = \{ f(x) \mid x\in\dom{f}\inter X\}$.
 \end{proposition}
 \begin{proof}
-    Every element of $\img{f}{X}$ is an element of
-        $\{ f(x) \mid x\in\dom{f}\inter X\}$ by \cref{img_of_function_elim}.
-    Every element of $\{ f(x) \mid x\in\dom{f}\inter X\}$ is an element of
-        $\img{f}{X}$ by \cref{img_of_function_intro}.
-    Follows by set extensionality.
+    Follows by \cref{setext,img_of_function_intro,img_of_function_elim}.
 \end{proof}
 
 \subsection{Families of functions}
@@ -392,11 +373,7 @@
     $\dom{g\circ f} = \preimg{f}{\dom{g}}$.
 \end{proposition}
 \begin{proof}
-    Every element of $\dom{g\circ f}$ is an element of $\preimg{f}{\dom{g}}$
-        by \cref{dom_iff,preimg_iff,circ_iff}.
-    Every element of $\preimg{f}{\dom{g}}$ is an element of $\dom{g\circ f}$
-        by \cref{dom_iff,preimg_iff,circ_iff}.
-    Follows by set extensionality.
+    Follows by \cref{setext,dom_iff,preimg_iff,circ_iff}.
 \end{proof}
 
 \begin{proposition}\label{dom_circ_exact}
@@ -405,10 +382,7 @@
     $\dom{g\circ f} = \dom{f}$.
 \end{proposition}
 \begin{proof}
-    Every element of $\dom{g\circ f}$ is an element of $\dom{f}$
-        by \cref{dom_iff,circ_iff}.
-    Every element of $\dom{f}$ is an element of $\dom{g\circ f}$ by \cref{circ_iff,ran_iff,dom_iff}.
-    Follows by set extensionality.
+    Follows by \cref{setext,circ_iff,ran_iff,dom_iff}.
 \end{proof}
 
 \begin{proposition}\label{ran_of_circ_intro}
@@ -445,11 +419,7 @@
     Then $\ran{g\circ f} = \img{g}{\ran{f}}$.
 \end{proposition}
 \begin{proof}
-    Every element of $\ran{g\circ f}$ is an element of $\img{g}{\ran{f}}$
-        by \cref{ran_of_circ_elim}.
-    Every element of $\img{g}{\ran{f}}$ is an element of $\ran{g\circ f}$
-        by \cref{ran_of_circ_intro}.
-    Follows by set extensionality.
+    Follows by \cref{setext,ran_of_circ_intro,ran_of_circ_elim}.
 \end{proof}
 
 \begin{proposition}\label{ran_circ_exact}