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}$.
