[proofplan] Let $m$ denote the infimum of $I$ over the admissible class $\mathcal A$. If $m=+\infty$, then every admissible point has energy $+\infty$, so any element of $\mathcal A$ is a minimizer. If $m<+\infty$, the definition of infimum gives a minimizing sequence; the compactness hypothesis gives a convergent subsequence with limit in $\mathcal A$, and the assumed lower semicontinuity along that subsequence forces the limit energy to be at most $m$. Since $m$ is a lower bound for all admissible energies, equality follows. [/proofplan] [step:Separate the extended-real case where the infimum is $+\infty$] Define the extended-real number $m:=\inf_{v\in\mathcal A} I[v]$. Because $I$ is bounded below and takes values in $\mathbb R\cup\{+\infty\}$, we have $m\in\mathbb R\cup\{+\infty\}$. Assume first that $m=+\infty$. Since $m$ is the infimum of the set $\{I[v]:v\in\mathcal A\}$ and no value of $I$ exceeds $+\infty$, it follows that $I[v]=+\infty$ for every $v\in\mathcal A$. The set $\mathcal A$ is nonempty, so choose $u_*\in\mathcal A$. Then $I[u_*]=+\infty=m=\inf_{v\in\mathcal A}I[v]$, so $u_*$ is a minimizer. It remains to treat the case $m\in\mathbb R$. [/step] [step:Choose a minimizing sequence from the definition of the infimum] Assume $m\in\mathbb R$. For each $k\in\mathbb N$, the number $m+\frac{1}{k}$ is strictly larger than $m$. By the defining property of the infimum, there exists $u_k\in\mathcal A$ such that $I[u_k]<m+\frac{1}{k}$. Since $m$ is a lower bound for $\{I[v]:v\in\mathcal A\}$, we also have $m\le I[u_k]$. Thus $m\le I[u_k]<m+\frac{1}{k}$. By the squeeze property for real sequences, $I[u_k]\to m$. Therefore $(u_k)_{k=1}^{\infty}$ is a minimizing sequence in $\mathcal A$. [guided] We need an actual minimizing sequence, not just the abstract value of the infimum. Define $m:=\inf_{v\in\mathcal A}I[v]$, and in this step we are working under the assumption $m\in\mathbb R$. The defining property of the infimum says that $m$ is a lower bound and that no number larger than $m$ can still be a lower bound. Hence, for each $k\in\mathbb N$, the number $m+\frac{1}{k}$ is not a lower bound for the set of admissible energies. Therefore there exists a point $u_k\in\mathcal A$ satisfying $I[u_k]<m+\frac{1}{k}$. At the same time, because $m$ is a lower bound, every admissible point has energy at least $m$. Applying this to the particular point $u_k\in\mathcal A$ gives $m\le I[u_k]$. Combining the two inequalities yields $m\le I[u_k]<m+\frac{1}{k}$. The right endpoint $m+\frac{1}{k}$ converges to $m$, and the left endpoint is constantly $m$. The squeeze property for real sequences therefore gives $I[u_k]\to m$. This is exactly the definition of a minimizing sequence for $I$ on $\mathcal A$. [/guided] [/step] [step:Extract an admissible limit using compactness of minimizing sequences] Since $(u_k)_{k=1}^{\infty}$ is a minimizing sequence in $\mathcal A$, the compactness hypothesis gives a strictly increasing sequence of indices $(k_j)_{j=1}^{\infty}$ in $\mathbb N$ and a point $u\in\mathcal A$ such that $u_{k_j}\to u$ in the topology of $X$. [/step] [step:Apply lower semicontinuity along the convergent minimizing subsequence] The subsequence $(u_{k_j})_{j=1}^{\infty}$ arises from the minimizing sequence $(u_k)_{k=1}^{\infty}$ and converges in $X$ to $u\in\mathcal A$. Therefore the lower semicontinuity hypothesis gives $I[u]\le \liminf_{j\to\infty} I[u_{k_j}]$. Since $I[u_k]\to m$ as $k\to\infty$, every subsequence of the real sequence $(I[u_k])_{k=1}^{\infty}$ also converges to $m$. Hence $\liminf_{j\to\infty} I[u_{k_j}]=m$. Consequently, $I[u]\le m$. [/step] [step:Use the lower-bound property of the infimum to identify the minimizer] Because $u\in\mathcal A$ and $m=\inf_{v\in\mathcal A}I[v]$, the number $m$ is a lower bound for all admissible energies. In particular, $m\le I[u]$. Together with the inequality $I[u]\le m$ obtained above, this gives $I[u]=m=\inf_{v\in\mathcal A}I[v]$. Setting $u_*:=u$, we have found $u_*\in\mathcal A$ such that $I[u_*]=\inf_{v\in\mathcal A}I[v]$. Thus $I$ attains its infimum on $\mathcal A$. [/step]