Covariant derivative of a one-form

I follow Carroll's method of deriving this. So, we postulate that the covariant derivative is the partial derivative plus some correction (see Wald for a proof). We then have the following $$nabla_mu V^nu=partial_mu V^nu+Gamma^nu_{mulambda}V^lambda$$ Using similar reasoning to how we got the above, we postulate the following: $$nabla_mu V_nu=partial_mu V_nu+gamma^lambda_{munu}V_lambda$$ However, we as of yet have no justification on equating $gamma$ and $Gamma$ just yet. They transform the same (which I will not prove here), but that's all. To prove a relation between the two, we assume two more things about the covariant derivative in addition to linearity and the Leibniz product rule: that the covariant derivative of the Kronecker delta vanishes $nabla_mu delta^nu_lambda=0$ and that it reduces to the partial derivative on scalars $nabla_muphi=partial_muphi$. Using these, let's calculate the following: $nabla_mu(V_sigma W^sigma)$
$$begin{align} nabla_mu(V_sigma W^sigma)&=nabla_mu(delta_lambda^sigma V_sigma W^lambda) &=V_sigma W^lambdanabla_mudelta^sigma_lambda+V_sigmanabla_mu W^sigma+W^sigmanabla_mu V_sigma &=V_sigmapartial_mu W^sigma+W^sigmapartial_mu V_sigma+V_sigmaGamma^sigma_{mulambda}W^lambda+W^sigmagamma^lambda_{musigma}V_lambda end{align}$$ But, $V_sigma W^sigma$ is a scalar! Thus, by our second new property, it should reduce to the partial derivative. So, we also have $$ begin{align} nabla_mu(V_sigma W^sigma)&=partial_mu(V_sigma W^sigma) &=V_sigmapartial_mu W^sigma+W^sigmapartial_mu V_sigma end{align}$$ Equating terms, we immediately see that $$0=Gamma^sigma_{mulambda}V_sigma W^lambda+gamma^lambda_{musigma}W^sigma V_lambda$$ Relabeling indices, we see that $$gamma^lambda_{musigma}W^sigma V_lambda=-Gamma^lambda_{musigma}W^sigma V_lambda$$ Since $V_sigma$ and $W^sigma$ are completely arbitrary, we have in general that $$bbox[5px,border:1.5px solid black] { gamma^lambda_{musigma}=-Gamma^lambda_{musigma} }$$ So, after much ado, we finally have, for the covariant derivative of a one-form, $$nabla_mu V_nu=partial_mu V_nu-Gamma^lambda_{munu}V_lambda$$

The covariant derivative is at first a map $nabla:Gamma(TM)timesGamma(TM)toGamma(TM)$ taking two vector fields $(X,Y)$ to a third $nabla_X Y$ obeying some properties. In particular it has to be a tensor in the first entry $nabla_{fX}Y=fnabla_XY$ and must be a derivation in the second entry $nabla_{X}(fY)=X(f)Y+fnabla_X Y$.

Then we want to actually have maps $nabla : Gamma(TM)timesGamma(T^r_sM)toGamma(T^r_s M)$ which take now a vector field and a tensor field $(X,T)$ and give you a tensor field $nabla_X T$. These maps must clearly be built from the initial one you had for vector fields only.

Now all tensor fields with $r$ indices up and no index down, i.e., elements of $Gamma(T^r_0M)$ can be generated from vector fields by the tensor product. In that case if you demand that $$nabla_X(Totimes S)=nabla_X Totimes S+Totimes nabla_X S,tag{1}$$

then the initial map, which acts only on vector fields, already fixes all the maps $$nabla:Gamma(TM)times Gamma(T^r_0M)to Gamma(T^r_0M).tag{2}$$

Moreover property (1) is just again saying that $nabla$ acts as a derivative.

Now we also have all the tensor fields with $s$ indices down and no index up, i.e., elements of $Gamma(T^0_sM)$. All of these can be generated from the one-forms $Gamma(T^0_1M)$ and tensor products. So if we fix $nabla$ acting on forms, property (1) again fixes it once and for all in all $Gamma(T^0_sM)$.

The way we go here is by demanding that if $omegain Gamma(T^0_1M)$ is a one-form and $Yin Gamma(TM)$ is a vector field, we have $$nabla_{X}[omega(Y)]=(nabla_X omega)(Y)+omega(nabla_X Y)tag{3}.$$

This is again a Liebnitz rule of sorts, where we view the contraction $omega(Y)$ as a kind of product. Observe from (3) that since $nabla_X Y$ is already defined, and since $omega(Y)$ is just a smooth function, if we say how $nabla$ acts on smooth functions we are done, this formula fully defines $nabla_X omega$.

Now the most natural definition is to take $nabla_X f = X(f)$ for any smooth function. In particular, comparing the initial definition of $nabla$ on vector fields which demanded $nabla_X(fY)=X(f)Y+fnabla_X Y$ and property (1), we see that these are fully compatible once we identify that $fotimes Y = fY$.

Once this is done we have that $$nabla_Xomega(Y) = X(omega(Y))-omega(nabla_X Y),tag{4}$$

and as I said from (1) this extends to all $T^0_sM$. Clearly now everything also extends to all $T^r_sM$.

Now to compare. Introduce a coordinate system $x^mu$ with coordinate basis $partial_mu$. Denote $nabla_mu := nabla_{partial_mu}$. Then if $X$ is a vector field $X = X^nupartial_nu$ we have $$nabla_mu X = nabla_mu (X^nu partial_nu)=partial_mu X^nu + X^nu nabla_mu partial_nu=partial_mu X^nu partial_nu + X^nuGamma_{munu}^lambda partial_lambda=(partial_mu X^lambda + Gamma_{munu}^lambda X^nu)partial_lambdatag{5}.$$

Where I just have used the rules for $nabla$ and defined $Gamma_{munu}^lambda$ by means of $nabla_mu partial_nu = Gamma_{munu}^lambda partial_lambda$.

Finally using (4) we can evaluate the components of the one-form $nabla_mu omega$ in the coordinate basis $dx^nu$ by applying it to $partial_nu$. Recalling that $omega(partial_nu)=omega_nu$ we get $$nabla_muomega(partial_nu)=partial_mu omega_nu-omega(nabla_mu partial_nu)=partial_muomega_nu-omega(Gamma_{munu}^lambdapartial_lambda)=partial_muomega_nu-Gamma_{munu}^{lambda}omega_lambdatag{6}$$

as you suggested.

Finally all this would work for any covariant derivative $nabla$. It is only when you impose vanishing torsion and metric compatibility that you fix uniquely the Levi-Civita one and you are able to determine, in local coordinates, $Gamma_{munu}^lambda$ in terms of the metric.

So in summary it all boils down in how to define a covariant derivative. In particular in how we first define it on vectors and extends to tensors in the simples and most natural way.