\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{Handling Obelix}

I work with the free multiplicative group $G$ on countably many generators, but an additive (abelian) free group also works.  The functional equation for Obelix is 
\[
f(f^2(h)f(h)^{-1})=hf(h)^{-1}.
\]
Think of this as saying that if $(a,b),(b,c)\in f$, then we must have $(cb^{-1},ab^{-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 an injective function.
    \item[(3)] $(1,1)\in E$.
    \item[(4)] If $(a,b),(b,c)\in E$, then $(cb^{-1},ab^{-1})\in E$.
    \item[(5)] If $(a,b)\in E$ and $a=b$, then $a=b=1$.
    \item[(6)] If $(a,b)\in E$ and $b\notin {\rm dom}(E)$, then $ab^{-1}\notin {\rm dom}(E)\cup{\rm im}(E)$.
\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}
{\bf Case 1}: Assume $(a,b)\in E$ for some $b\in G$.

If $b\in {\rm dom}(E)$, then by condition (4) we are already done.  So reduce to the case when $b\notin {\rm dom}(E)$.  In particular, by (2) and (3) we know $a,b\neq 1$, and also by (6) we know that $ab^{-1}\notin {\rm dom}(E)\cup{\rm im}(E)$ (and is not $1$).

Take $c$ to be a generator of $G$ not appearing in the reduced form of any entry in $E$, and set $E':=E\cup\{(b,c),(cb^{-1},ab^{-1}\}$.  Conditions (1), (3), and (5) are immediate.  Condition (2) is also clear, where injectivity needs $ab^{-1}\notin {\rm im}(E)$.   Condition (4) is also easy to check, using the fact that $E$ is injective, $cb^{-1}\neq c$, and $ab^{-1}\notin {\rm dom}(E)$.  

Finally, for condition (6), a finite check works.  The main case is checking that $ca^{-1}\notin {\rm dom}(E')\cup {\rm im}(E')$.  This is clear since $a\neq 1$ and $a\neq b$ (by condition (5) for $E$).

{\bf Case 2}: Assume $a\notin {\rm dom}(E)$.  If $(x,a)\in E$ for some (unique by (2)) $x\in G$, then applying Case 1 to $x$, we reduce to the case when $a\in {\rm dom}(E)$.

Thus, we may consider the case when $a\notin {\rm dom}(E)\cup {\rm im}(E)$.  Fixing $b$ to be a generator of $G$ not appearing in the reduced forms for the entries in $E$, nor in $a$, then after passing to $E\cup\{(a,b)\}\in \mathscr{E}$ we again reduce to Case 1.
\end{proof}

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

\end{document} 

