Isomorphism of RHoms in condensed mathematics In Proposition 5.7 on page 34 in lectures on condensed mathematics Peter Scholze shows that $\mathbb{Z}[S]^\blacksquare$ is solid. He shows that the two relevant expressions are isomorphic, however, in the definition of solidity it says that the isomorphism has to come from the natural map $\mathbb{Z}[S]\to\mathbb{Z}[S]^\blacksquare$. Can somebody tell me where this is proved?
 A: I guess that this basically follows from keeping track of isomorphisms. Seemingly it is a bit harder to trace the following isomorphisms, due to the occurrence of the shift $\require{AMScd}\DeclareMathOperator\Hom{Hom}\DeclareMathOperator\iHom{\underline{Hom}}\DeclareMathOperator\fin{fin}\DeclareMathOperator\colim{colim}\mathbb Z[-1]$:
\begin{align*}
R\Hom(\prod_J\mathbb R/\mathbb Z,\mathbb Z)&=\bigoplus_J\mathbb Z[-1]\\
R\Hom(\prod_J\mathbb Z,\mathbb Z)&=\bigoplus_J\mathbb Z
\end{align*}
I am not sure what the author of these notes had in mind then, but one can cook up an argument by adapting the proof of Thm 4.3 as follows.
Claim. The canonical map $\bigoplus_J\mathbb Z\to R\iHom(\prod_J\mathbb Z,\mathbb Z)$ is an isomorphism. Namely, $\bigoplus_J\mathbb Z$ is (derived condensed) reflexive.
Proof. We examine the morphism
\begin{CD}
\colim_{I\subseteq_{\fin}J}R\Hom(\prod_I\mathbb R/\mathbb Z,\mathbb Z)@>>>\colim_{I\subseteq_{\fin}J}R\Hom(\prod_I\mathbb R,\mathbb Z)@>>>\colim_{I\subseteq_{\fin}J}R\Hom(\prod_I\mathbb Z,\mathbb Z)\\
@VVV@VVV@VVV\\
R\Hom(\prod_J\mathbb R/\mathbb Z,\mathbb Z)@>>>R\Hom(\prod_J\mathbb R,\mathbb Z)@>>>R\Hom(\prod_J\mathbb Z,\mathbb Z)
\end{CD}
of fiber sequences. By the proof Thm 4.3, the middle terms are all zeros, and the left-most vertical map is an isomorphism, thus so is the right-most map.
In Prop 5.7, note that, for profinite sets $T$, the map $\mathbb Z[T]\to\mathbb Z[T]^\blacksquare$ can be rewritten as the canonoical double dual map $\mathbb Z[T]\to \mathbb Z[T]^{\vee\vee}$, where $(-)^\vee:=R\iHom(-,\mathbb Z)$, and it suffices to check that this induces an equivalence $\mathbb Z[T]^{\vee\vee\vee}\to\mathbb Z[T]^\vee$ after taking a further dual $(-)^\vee$, and this should follow formally from the reflexivity of $\mathbb Z[T]^\vee$.
