An induction formula for spectral Mackey functors, and a fake proof I'm trying to get a grasp of Barwick's model for genuine $G$-spectra, that is, spectral Mackey functors 1. There's a classical formula about induction, that should be easy to prove,  that I was trying to prove in this model; but I failed, and it's worse than that because it's not just that my proof isn't conclusive, it proves that the formula fails.
So I'm trying to understand where my proof went wrong: the rest of my question is devoted to presenting said proof, and the question is :

Where is the mistake ?

I apologize in advance for the long proof, but I wanted to make sure all the details were there - of course if I say "one easily sees that" too much, then the mistake is bound to be in those moments.
So here goes:
$\newcommand{\ind}{\mathrm{Ind}} \newcommand{\Hom}{\mathrm{Hom}} \newcommand{\map}{\mathrm{map}} \newcommand{\Map}{\mathrm{Map}} \newcommand{\Mack}{\mathbf{Mack}} \newcommand{\res}{\mathrm{res}}$
My conventions are as follows: $\map$ denotes the mapping space, $\Map$ denotes the mapping spectrum between two objects in a stable $\infty$-category, and in the category $\Mack_G$ (of spectral Mackey functors), $\Hom_G$ will denote the internal hom, defined by adjunction with the Green tensor product (defined in 2). $G$ will be a fixed finite group.
$A^{eff}(G)$ is the effective Burnside category, defined in 1.
I will say "$G$-spectrum" to mean "spectral Mackey functor on $A^{eff}(G)$".
The claim in question is that for any subgroup $H$, $H$-spectrum $Y$, and $G$-spectrum $X$, $\ind_H^GY\otimes X\simeq \ind_H^G(Y\otimes \res_H^GX$). This is a pretty basic claim, analogous to the situation in $1$-category theory, for representations over a commutative ring, so it should be true.
If the proof is correct, then maybe the mistake is in my assumption that the Green tensor product corresponds the usual smash product of genuine $G$-spectra ?

Is that the case ?

Note that $\ind_H^G$ is defined to be left adjoint to $\res_H^G$, while $\res_H^G$ is defined by restriction along $A^{eff}(H)\to A^{eff}(G)$ given informally by $L\mapsto G\times_H L$ (this is a functor $F_H\to F_G$ which preserves pullbacks and coproducts, so it induces an additive functor on the effective Burnside categories)
Then, $$\map(\ind_H^GY\otimes X,Z) \simeq \map(\ind_H^GY, \Hom_G(X,Z))\simeq \map(Y,\res_H^G\Hom_G(X,Z))$$
where all the equivalences are natural in $X,Y,Z$, and also
$$\map(\ind_H^G(Y\otimes \res_H^GX),Z)\simeq \map(Y\otimes \res_H^GX,\res_H^GZ)\simeq \map(Y, \Hom_H(\res_H^GX,\res_H^GZ))$$
so the claim is equivalent to $\res_H^G\Hom_G(X,Y)\simeq \Hom_H(\res_H^GX,\res_H^GZ)$, which is a reasonable claim, and again, valid in the analogous situation in $1$-category theory.
So to prove this claim I tried to compute the value of $\res_H^G\Hom_G(X,Z)$ on $H/K$ for $K\leq H$. This is the same as $\Hom_G(X,Z)(G/K)$ by definition, and so I wanted to compute the values of $\Hom_G(X,Z)$.
Note that $ev_{G/K}\circ \Hom_G(X,-)$ is right adjoint to $X\otimes i_!(-)$, where $i : \{G/K\}\to A^{eff}(G)$ is the inclusion, and $i_!$ is left Kan extension along $i$ followed by the left adjoint to the inclusion $\Mack_G\to Fun(A^{eff}(G),Sp)$.
So, naturally in $X,Y,Z$, $\map_{\Mack_G}(X\otimes i_!(Y), Z) \simeq \map_{Fun(A^{eff}(G),Sp)}(X\otimes_{Day} i_! Y,Z)$ by definition of the Green tensor product; then by definition of the Day tensor product, this is $\simeq \map_{Fun(A^{eff}(G)\times A^{eff}(G),Sp)}(X(-) \boxtimes i_!Y(\bullet),Z(-\times \bullet)$ where $(X\boxtimes i_!Y)((L,L')) := X(L)\otimes (i_!Y)(L'))$.
So now we get $\map_{Fun(A^{eff}(G),Sp)}(i_!Y(\bullet), \Map(X(-), Z(-\times \bullet))$.
Let me specify what I mean here, as the notations are annoying: $\bullet$ being fixed, $Z(-\times \bullet)$ is a functor of $-$ so $\Map(X(-),Z(-\times \bullet))$, the mapping spectrum in the stable $\infty$-category $Fun(A^{eff}(G),Sp)$ is well-defined, and it's a functor of $\bullet$, which makes this meaningful.
Now finally, using the definition of $i_!$, and given that $\Map(X(-),Z(-\otimes \bullet))$ is an additive functor of $\bullet$, this mapping space is $\map_{Sp}(Y, \Map(X(-), Z(-\times G/K))$.
It follows that $ev_{G/K}\circ \Hom_G(X,Z)\simeq \Map(X,Z(-\times G/K))$.
Therefore, on the one hand,
$$\res_H^G\Hom_G(X,Y)(H/K)\simeq \Map(X,Z(-\times G/K))$$
and on the other hand,
$$\Hom_H(\res_H^GX,\res_H^GZ)(H/K) \simeq \Map(\res_H^GX, (\res_H^GZ)(-\times G/K)) \simeq \Map(\res_H^GX, Z(G\times_H(-)\times G/K)) \\
\simeq \Map(X,\mathrm{CoInd}_H^G(Z(G\times_H(-)\times G/K)))$$  the $\res_H^G\dashv \mathrm{CoInd}_H^G$ adjunction being automatically $Sp$-enriched.
To conclude, we must compute $\mathrm{CoInd}_H^G M$, for a $G$-spectrum $M$. But note that the forgetful functor $A^{eff}(G)\to A^{eff}(H)$ (induced by the forgetful $F_G\to F_H$) is left adjoint to $G\times_H -$ (as it is a right adjoint to it, and we have compatible equivalences $A^{eff}(G)^{op}\simeq A^{eff}(G))$), so that precomposing with it is right adjoint $Fun(A^{eff}(H),Sp)\to Fun(A^{eff}(G),Sp)$. But now both precompositions preserve the full subcategories of Mackey functors, so they induce an adjunction between $\Mack_G$ and $\Mack_H$, the left adjoint of which is precomposition with $G\times_H-$, i.e. $\res_H^G$.
So precomposition with the forgetful $U: A^{eff}(G)\to A^{eff}(H)$ is exactly coinduction (one can make a reality check of this by looking at what this means when we evaluate in $G=G/e$, which should yield the underlying spectrum); so that, in the end
$$\Hom_H(\res_H^GX,\res_H^GZ)(H/K)\simeq \Map(X, Z((G\times_H U(-)) \times G/K))$$
and those two spectra are simply not the same, as $G\times_H U(-)$ is not equivalent to the identity. Worse, one can make it pretty explicit : $G\times_H U(-)\simeq G/H\times -$, as one checks on $F_G$, so that the latter is $\Map(X,Z(G/H\times G/K\times -)$. Taking, e.g., $H=K=e$, by a usual trick you can make on of the $G$'s have a trivial action, and so this is $\bigoplus_{g\in G}\Map(X,Z(G\times -))$ which is, in general, different from $\Map(X,Z(G\times -))$.
But note that the reduction from the beginning was an equivalence, not only a sufficient condition, so this computation seems to not only mean I can't prove the claim, but actually that the claim is wrong ! However this is seemingly a well-known fact, and analogous to an easy $1$-categorical fact, so  I must be making a mistake.
1: Barwick, C. (2017). Spectral Mackey functors and equivariant algebraic K-theory (I). Advances in Mathematics, 304, 646-727.
2: Barwick, C., Glasman, S., & Shah, J. (2019). Spectral Mackey functors and equivariant algebraic K-theory, II. Tunisian Journal of Mathematics, 2(1), 97-146.
 A: $\newcommand{\Hom}{\mathrm{Hom}} \newcommand{\res}{\mathrm{res}}$
Ah, well, I found the mistake (at a surprising time: I'm more tired now than I was when I looked for it earlier) : $A^{eff}(H)\to A^{eff}(G)$ given by $G\times_H-$ preserves pullbacks, not products ! In particular, in my computation for $\Hom_H(\res_H^GX,\res_H^GZ)(H/K)$, I used $G\times_H(-\times H/K) \simeq G\times_H - \times G/K$, whereas it should be (apologies for the notation) $(G\times_H -) \times_{G/H} G/K$ (where of course $\times_H$ is not a pullback, but $\times_{G/H}$ is one)
This precisely solves the problem, as $G\times_H U(-) \simeq G/H\times -$ so this $G/H$ gets cancelled with the $\times_{G/H}$ and you get the same result, which makes the proof work.
As Dylan pointed out in the comments, there's a more direct, and perhaps more elegant proof using a reduction to $F_G$ and $F_H$ (which, I think, requires a lemma of the type $\Sigma^\infty_+\res_H^G\simeq \res_H^G\Sigma^\infty_+$, but this is not hard to prove). Of course, "my" proof is still interesting as it provides an explicit formula for $\Hom_G(X,Z)(G/K)$, which is perhaps interesting (although it was of course known in general for the internal hom in a Day convolutional symmetric monoidal structure)
