[proofplan]
We first construct a minimizing sequence using the defining approximation property of the infimum. The compactness hypothesis gives a $\tau$-convergent subsequence, and sequential $\tau$-closedness places its limit back in the admissible class. Sequential lower semicontinuity then shows that the limiting value is no larger than the infimum, while the definition of the infimum gives the opposite inequality.
[/proofplan]
custom_env
admin
[step:Choose a minimizing sequence from the finite infimum]Set
\begin{align*}
m:=\inf_{v\in\mathcal A} I[v].
\end{align*}
Let $\mathbb N:=\{1,2,3,\dots\}$. Since $m<\infty$, for each $k\in\mathbb N$ there exists $u_k\in\mathcal A$ such that
\begin{align*}
I[u_k]<m+\frac{1}{k}.
\end{align*}
Because $m$ is a lower bound for the set $\{I[v]:v\in\mathcal A\}$, we also have
\begin{align*}
m\le I[u_k].
\end{align*}
Hence
\begin{align*}
m\le I[u_k]<m+\frac{1}{k}
\end{align*}
for every $k\in\mathbb N$, so $I[u_k]\to m$. Thus $(u_k)_{k=1}^{\infty}$ is a minimizing sequence in $\mathcal A$.[/step]
custom_env
admin
[guided]The purpose of this step is to turn the number $m$ into an actual sequence of admissible competitors. By definition,
\begin{align*}
m:=\inf_{v\in\mathcal A} I[v].
\end{align*}
Let $\mathbb N:=\{1,2,3,\dots\}$. The hypothesis $m<\infty$ ensures that, for each $k\in\mathbb N$, the upper approximating level
\begin{align*}
m+\frac{1}{k}
\end{align*}
is a finite real number. Since $m$ is the greatest lower bound of the values of $I$ on $\mathcal A$, no number larger than $m$ can remain a lower bound. Therefore, for each $k\in\mathbb N$, there must exist an element $u_k\in\mathcal A$ with
\begin{align*}
I[u_k]<m+\frac{1}{k}.
\end{align*}
At the same time, the lower-bound property of the infimum gives
\begin{align*}
m\le I[u_k].
\end{align*}
Combining the two inequalities gives
\begin{align*}
m\le I[u_k]<m+\frac{1}{k}.
\end{align*}
Let $\varepsilon>0$. Choose $K\in\mathbb N$ such that $1/K<\varepsilon$. For every $k\ge K$, the preceding estimate gives
\begin{align*}
|I[u_k]-m|<\varepsilon.
\end{align*}
Thus $I[u_k]\to m$. This is exactly the statement that $(u_k)_{k=1}^{\infty}$ is a minimizing sequence in $\mathcal A$.[/guided]
custom_env
admin
[step:Extract a $\tau$-convergent subsequence]
The sequence $(u_k)_{k=1}^{\infty}$ is a minimizing sequence in $\mathcal A$. By the compactness hypothesis, there exist a subsequence $(u_{k_j})_{j=1}^{\infty}$ and an element $u_*\in X$ such that
\begin{align*}
u_{k_j}\to u_*
\end{align*}
with respect to the topology $\tau$.
[/step]
custom_env
admin
[step:Use sequential closedness to recover admissibility of the limit]
For every $j\in\mathbb N$, $u_{k_j}\in\mathcal A$, and the subsequence satisfies $u_{k_j}\to u_*$ with respect to $\tau$. Since $\mathcal A$ is sequentially $\tau$-closed, it follows that
\begin{align*}
u_*\in\mathcal A.
\end{align*}
[/step]
custom_env
admin
[step:Apply lower semicontinuity to compare the limit with the infimum]
The sequence $(u_{k_j})_{j=1}^{\infty}$ lies in $\mathcal A$, its $\tau$-limit $u_*$ lies in $\mathcal A$, and $I$ is sequentially $\tau$-lower semicontinuous on $\mathcal A$. Therefore
\begin{align*}
I[u_*]\le \liminf_{j\to\infty} I[u_{k_j}].
\end{align*}
Since $I[u_k]\to m$, every subsequence of the real sequence $(I[u_k])_{k=1}^{\infty}$ also converges to $m$. Hence
\begin{align*}
\liminf_{j\to\infty} I[u_{k_j}]=m.
\end{align*}
Thus
\begin{align*}
I[u_*]\le m.
\end{align*}
[/step]
custom_env
admin
[step:Use the infimum lower bound to conclude minimality]
Because $u_*\in\mathcal A$ and $m=\inf_{v\in\mathcal A} I[v]$, the defining lower-bound property of the infimum gives
\begin{align*}
m\le I[u_*].
\end{align*}
Together with $I[u_*]\le m$, this yields
\begin{align*}
I[u_*]=m=\inf_{v\in\mathcal A} I[v].
\end{align*}
Therefore $u_*$ is a minimizer of $I$ over $\mathcal A$.
[/step]