I understand that
$$ \frac{\mathrm d}{\mathrm dt} \langle\psi|\psi\rangle =\left[\frac{\mathrm d}{\mathrm dt} \langle\psi|\right]|\psi\rangle + \langle\psi|\left[\frac{\mathrm d}{\mathrm dt}|\psi\rangle\right]$$
and that this can be established by a direct application of the definition of the derivative; but it is not clear to me why
$$\frac{\mathrm d}{\mathrm d t} |\psi\rangle \;=\; -i H |\psi\rangle\implies\left[\frac{\mathrm d}{\mathrm dt} \langle\psi|\right]=i\langle\psi|H^\dagger$$
given only a linear vector space and the properties of an inner product.
Should I be able to derive the above conclusion from just the properties of a linear vector space with an inner product, or is more needed?
Since the bra-vector is just the Hermitian conjugate of the ket-vector$\newcommand{\ddt}{\frac{\mathrm d}{\mathrm dt}}$ $$ \langle\psi| = |\psi\rangle^\dagger $$ $$ \ddt \langle\psi| = \ddt |\psi\rangle^\dagger =\left(\ddt |\psi\rangle\right)^\dagger= \Big(-i H |\psi\rangle\Big)^\dagger =-|\psi\rangle^\dagger H^\dagger i^\dagger = i\langle\psi|H^\dagger$$ If we assume $H$ is a linear operator defined on proper space.
For example: If $|\psi\rangle = (c_1,\ldots,c_n)^T$ is a column vector with $n$ complex entries, then $\langle\psi| = (c_1^*,\ldots,c_n^*) $ is a row vector whose entries are the complex conjugate of $c_i$, and then $H$ is an $n\times n$ complex matrix. If $|\psi\rangle$ is a function in $H^1_0$, then $\langle\psi|$ is a bounded linear functional on $H^1_0$, and $H$ is a bounded linear operator like Laplacian.
EDIT: As OP pointed out, the reason why bra-vector is the Hermitian conjugate of the ket-vector is Riesz representation theorem. In short: any Hilbert and its dual space has a 1-1 correspondence, moreover the correspondence is nice in that it preserves the norm (isometry). If $|\psi\rangle \in V$, then its dual is a bounded linear function on $V$, the space we denote it as $V'$. For any $|\psi\rangle$, we can associate a unique linear functional $l_{\psi}$, and $ \langle\psi|\phi\rangle:= l_{\psi}(\phi)$, in other words, $\langle\psi|$ is this linear functional, just different notation.
A translation from physics:
If using the functional analysis notation, translating from bra-ket notation, the problem should be:
For any $\phi \in V$, by the definition induced by Riesz: $$ \ddt l_{\psi}(\phi) = \ddt\langle \psi,\phi\rangle $$ A possible choice for the inner product is the integration of the first input's complex conjugate times second input with respect to properly defined measure (it doesn't have to be this, can be others): $$ \langle f,g\rangle = \int_X f\overline{g} $$ Then: $$ \ddt\langle \psi,\phi\rangle = \langle \ddt\psi,\phi\rangle = \langle-i H\psi,\phi\rangle $$ If the Hermitian conjugate (adjoint) of the linear operator $H$ is denoted as $H^*$: $$ \langle-i H\psi,\phi\rangle = \langle \psi,(iH^*)\phi\rangle = l_{\psi}(iH^*\phi) $$ Therefore: $$ \ddt l_{\psi}(\phi) = l_{\psi}(iH^*\phi), \quad \forall \phi\in V. $$ This is the same as: $$ \ddt\langle\psi| = i\langle\psi|H^\dagger $$ just one using functional analysis notation and the other using bra-ket notation.