\documentclass[12pt,oneside,leqno]{amsart}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage[hidelinks]{hyperref}
\usepackage{tikz}
\usetikzlibrary{cd}
\usepackage{mathrsfs}

\newenvironment{nouppercase}{%
  \let\uppercase\relax%
  \renewcommand{\uppercasenonmath}[1]{}}{}

\usepackage{comment}

\makeatletter
\renewcommand{\eqref}[1]{\textup{(\ignorespaces\ref{#1}\unskip\@@italiccorr)}}
\def\maketag@@@#1{\hbox{\m@th\normalfont\bfseries#1}}
\makeatother

% THEOREMS -------------------------------------------------------

\numberwithin{equation}{section}
\numberwithin{figure}{section}

\theoremstyle{plain}
\newtheorem{thm}[equation]{Theorem}
\newtheorem{lemma}[equation]{Lemma}
\newtheorem{cor}[equation]{Corollary}
\newtheorem{prop}[equation]{Proposition}
\newtheorem{example}[equation]{Example}

\theoremstyle{definition}
\newtheorem{definition}[equation]{Definition}
\newtheorem{question}[equation]{Question}
\newtheorem{remark}[equation]{Remark}



% MATH -----------------------------------------------------------
\newcommand{\Q}{\ensuremath \mathbb{Q}}
\newcommand{\R}{\ensuremath \mathbb{R}}
\newcommand{\C}{\ensuremath \mathbb{C}}
\newcommand{\Z}{\ensuremath \mathbb{Z}}
\newcommand{\N}{\ensuremath \mathbb{N}}
\newcommand{\M}{\ensuremath \mathbb{M}}
\newcommand{\F}{\ensuremath \mathbb{F}}

\newcommand\subsetsim{\mathrel{\substack{
  \textstyle\subset\\[-0.2ex]\textstyle\sim}}}

\begin{document}

\section{1516 does not imply 1489}

This proof is very similar to the one that handled Obelix.  I'll thus be somewhat brief.  The functional equation for 1516 is
\[
f(f^{2}(h)h^{-1}f(1)^{-1})=h^{-1}f(1)^{-1}
\]
Throughout, we'll take $(1,1)$ for simplicity.  Think of this functional equation as saying that if $(a,b),(b,c)\in f$, then we must have $(ca^{-1},a^{-1})\in f$.

Define $\mathscr{E}$ as the collection of sets $E\subseteq G^2$ satisfying the following properties.
\begin{itemize}
    \item[(1)] $E$ is finite.
    \item[(2)] $E$ is a function.
    \item[(3)] $(1,1)\in E$.
    \item[(4)] If $(a,b),(b,c)\in E$, then $(ca^{-1},a^{-1})\in E$.
    \item[(5)] If $(a,b),(a',b),(a^{-1},d),(a'^{-1},d')\in E$ and $da=d'a'$, then $a=a'$.
    \item[(6)] If $(a,a^{-1})\in E$, then $a=1$.
    \item[(7)] If $(a,b),(a',b),(a^{-1},d)\in E$, then $ad\neq a'$.
    \item[(8)] If $(a,1)\in E$, then $a=1$.
\end{itemize}

\begin{lemma}
For any $E\in \mathscr{E}$ and any $a\in G$, there is an extension $E\subseteq E'\in \mathscr{E}$ where the functional equation holds for $a$.
\end{lemma}
\begin{proof}
Do a case analysis as in my other files.  The main case is when $(a,b)\in E$ but $b\notin{\rm dom}(E)$.  In that case $a,b\neq 1$.

Fix the finite list of first coordinates $a_1,a_2,\ldots, a_n$ that map to $b$ in $E$.  Also, fix the set $S$ to consist of the indices $j$ where $(a_j^{-1},d_j)\in E$ for some $d_j\in G$.  Taking $c$ to be a new generator of the (countably-generated free) group $G$, fix
\[
E':=E\cup\{(b,c)\}\cup\{(ca_i^{-1},a_i^{-1}\}_{i\in [1,n]}\cup\{d_ja_j c^{-1},a_jc^{-1}\}_{j\in S}.
\]
The last four conditions defining $\mathscr{E}$ help make the case analysis work.
\end{proof}

The functional equation for 1489 is $f(f(f(h^{-1})h)f(h)^{-1})=hf(h)^{-1}$.  Taking the seed
\[
\{(1,1),(x_1,x_2),(x_1^{-1},x_3),(x_3x_1,x_4),(x_4x_2^{-1},x_5)\}\in \mathscr{E}
\]
works to contradict this equation.

\end{document} 

