Using a mélange of mathematical syntaxes, we mechanize some exercises from Tao's excellent book
Ouverture
Let us informally define sets and set membership $\in$. A set is an unordered collection of objects, with the set itself being an object. Set membership checks whether a given object is contained within a set:
$$ \begin{align} \forall x, x \in A \vee x \not\in A \tag{law of excluded middle} \\ A \in C \wedge A = B \rightarrow B \in C \tag{axiom of substitution} \end{align} $$
The axiom of substition uses the definition of equality:
$$ \begin{matrix} A = B & \leftrightarrow & \forall x, x \in A \rightarrow x \in B \\ && \wedge \\ && \forall x, x \in B \rightarrow x \in A \end{matrix} $$
The axiom of substition is preserved for all sets only defined in terms of $\in$ and $=$.
Verify that set equality is reflexive, symmetric, and transitive.
Goal:
$$ \begin{matrix} \textrm{reflexive} & \forall A, A = A \\ \textrm{symmetric} & \forall A B, A = B \leftrightarrow B = A \\ \textrm{transitive} & \forall A B C, (A = B) \wedge (B = C) \rightarrow (A = C) \end{matrix} $$
Hypothesis:
$$ \begin{matrix} A = B & \leftrightarrow & \forall x, x \in A \leftrightarrow x \in B \tag{eq} \end{matrix} $$
Proof.
$$ \begin{matrix} A = A & \leftrightarrow & \forall x, x \in A \leftrightarrow x \in A & \textrm{by (eq)} \\ A = B & \leftrightarrow & \forall x, x \in A \rightarrow x \in B & \\ && \wedge & \\ && \forall x, x \in B \rightarrow x \in A & \\ & \leftrightarrow & B = A & \textrm{by (eq)} \\ A = B &&& \\ \wedge &&& \\ B = C & \rightarrow & \forall x, x \in A \rightarrow x \in B & \textrm{(1)} \\ && \wedge & \\ && \forall x, x \in B \rightarrow x \in A & \textrm{(2)} \\ && \wedge & \\ && \forall x, x \in B \rightarrow x \in C & \textrm{(3)} \\ && \wedge & \\ && \forall x, x \in C \rightarrow x \in B & \textrm{(4)} \\ & \rightarrow & \forall x, x \in A \rightarrow x \in C & \textrm{by (1) and (3)} \\ && \wedge & \\ && \forall x, x \in C \rightarrow x \in A & \textrm{by (4) and (2)} \\ & \rightarrow & A = C & \textrm{by (eq)} \end{matrix} $$
Qed.
Prove that the following sets are distinct: $\emptyset, \{\emptyset\}, \{\{\emptyset\}\}, \{\emptyset, \{\emptyset\}\}$.
Hypothesis:
$$ \begin{align} A = B & \leftrightarrow & \forall x, x \in A \leftrightarrow x \in B \tag{eq} \\ \forall x, x & \not\in & \emptyset \tag{phi} \\ \forall x, x \in \{a\} & \leftrightarrow & x = a \tag{build-a} \\ \forall x, x \in \{a, b\} & \leftrightarrow & (x = a) \vee (x = b) \tag{build-b} \end{align} $$
Lemma:
$$ \begin{matrix} A \neq B & \leftrightarrow & \exists x, (x \in A \wedge x \not\in B) \vee (x \not\in A \wedge x \in B) & \textrm{by (eq)} \end{matrix} $$
Proof.
$$ \begin{matrix} \emptyset & \neq & \textrm{any other set} & \textrm{by (phi) and (eq)} \\ \textrm{Plugging } x = \{\emptyset\} \textrm{ in (lemma)} & \rightarrow & \{\{\emptyset\}\} \neq \{\emptyset\} & \textrm{by (build-a)} \\ \textrm{Plugging } x = \{\emptyset\} \textrm{ in (lemma)} & \rightarrow & \{\emptyset, \{\emptyset\}\} \neq \{\emptyset\} & \textrm{by (build-a) and (build-b)} \\ \textrm{Plugging } x = \emptyset \textrm{ in (lemma)} & \rightarrow & \{\emptyset, \{\emptyset\}\} \neq \{\{\emptyset\}\} & \textrm{by (build-a) and (build-b)} \end{matrix} $$
Qed.
Show that, for any set $A$, $A \cup A = A \cup \emptyset = \emptyset \cup A = A$.
Hypothesis:
$$ \begin{align} A = B \leftrightarrow \forall x, x \in A \leftrightarrow x \in B \tag{eq} \\ \forall x, x \in A \cup B \leftrightarrow x \in A \vee x \in B \tag{union} \\ \forall x, x \not\in \emptyset \tag{phi} \end{align} $$
Proof.
$$ \begin{matrix} A \cup A = A & \leftrightarrow \forall x, x \in A \vee x \in A \leftrightarrow x \in A & \textrm{by (eq) and (union)} \\ & \leftrightarrow \forall x, x \in A \leftrightarrow x \in A & \textrm{by intuition} \\ \\ A \cup \emptyset = A & \leftrightarrow \forall x, x \in A \vee x \in \emptyset \leftrightarrow x \in A & \textrm{by (eq) and (union)} \\ & \leftrightarrow \forall x, x \in A \leftrightarrow x \in A & \textrm{by (phi) and intuition} \\ \\ \emptyset \cup A = A && \textrm{by similar argument} \end{matrix} $$
Qed.
Show that, for any three sets $A, B, C$, $A \subseteq B \wedge B \subseteq A \rightarrow A = B$, and $A \subsetneq B \subsetneq C \rightarrow A \subsetneq C$.
Hypothesis:
$$ \begin{align} A = B & \leftrightarrow & \forall x, x \in A \leftrightarrow x \in B \tag{eq} \\ A \neq B & \leftrightarrow & \exists x, (x \in A \wedge x \not\in B) \vee (x \not\in A \wedge x \in B) \tag{neq} \\ A \subseteq B & \leftrightarrow & \forall x, x \in A \rightarrow x \in B \tag{subset-eq} \\ A \subsetneq B & \leftrightarrow & A \subseteq B \wedge A \neq B \tag{subset-neq} \end{align} $$
Proof.
$$ \begin{matrix} A \subseteq B \wedge B \subseteq A & \rightarrow & \forall x, x \in A \leftrightarrow x \in B & \textrm{by (subset-eq) and intuition} \\ & \leftrightarrow & A = B & \textrm{by (eq)} \\ \\ A \subsetneq B & \leftrightarrow & A \subseteq B \wedge A \neq B & \textrm{by (subset-neq)} \\ & \leftrightarrow & \forall x, x \in A \rightarrow x \in B & \\ & & \wedge & \\ & & \exists x, (x \in A \wedge x \not\in B) \vee (x \in B \wedge x \not\in A) & \textrm{by (subset-eq) and (neq)} \\ & \rightarrow & \forall x, x \in A \rightarrow x \in B \wedge \exists x, x \in B \wedge x \not\in A & \textrm{by intuition} \\ \\\\ B \subsetneq C & \rightarrow & \forall x, x \in B \rightarrow x \in C & \\ & & \wedge & \\ & & \exists x, x \in C \wedge x \not\in B & \textrm{by similar argument} \\ \\\\ A \subsetneq B \wedge B \subsetneq C & \rightarrow & \forall x, x \in A \rightarrow x \in C & \\ & & \wedge & \\ & & \exists x, x \in C \wedge x \not\in A & \textrm{by intuition} \\ & \rightarrow & A \subseteq C \wedge C \neq A & \textrm{by (subset-eq) and (neq)} \\ & \rightarrow & A \subsetneq C & \textrm{by (subset-neq)} \end{matrix} $$
Qed.
Show that, for any two sets $A, B$, $$A \subseteq B \leftrightarrow A \cup B = B \leftrightarrow A \cap B = A$$
Hypothesis:
$$ \begin{align} A \subseteq B & = & \forall x &, x \in A \rightarrow x \in B \tag{subset-eq} \\ A \cup B & = & \forall x &, x \in A \vee x \in B \tag{union} \\ A \cap B & = & \forall x &, x \in A \wedge x \in B \tag{intersect} \end{align} $$
Proof.
$$ \begin{matrix} A \cup B = B & \leftrightarrow & \forall x, x \in A \cup B \leftrightarrow x \in A \vee x \in B = B & \textrm{by (union)} \\ & \leftrightarrow & \forall x, x \in A \vee x \in B \leftrightarrow x \in B & \textrm{by intuition} \\ & \leftrightarrow & \forall x, x \in A \rightarrow x \in B & \textrm{by intuition} \\ & \leftrightarrow & A \subseteq B & \textrm{by (subset-eq)} \\ \\\\ A \cap B = A & \leftrightarrow & \forall x, x \in A \wedge x \in B \leftrightarrow x \in A & \textrm{by (intersect) and intuition} \\ & \leftrightarrow & \forall x \in A \rightarrow x \in B & \textrm{by intuition} \\ & \leftrightarrow & A \subseteq B & \textrm{by (subset-eq)} \end{matrix} $$
Qed.
(3.3.4) Show that injective corresponds to left-cancelable, and dually, surjective corresponds to right-cancelable, in function composition.
For this proof, we use natural deductions, as introduced in Dowek's Proofs in Theories Ch. 1.
where $\Gamma = g \texttt{ is injective} \wedge g f = g \tilde{f}$.