I'm looking for a reference (and precise hypothesis if more are needed) for the following facts (or a correction, if I'm just plain wrong):

Let $G$ and $H$ be topological groups and $f : G \to H$ be a continuous homomorphism. Applying the classifying space functor gives a map $Bf: BG \to BH$.

The homotopy fiber of $Bf$ is the homotopy orbit space $H_{hG}$ where $G$ acts on $H$ via $g \cdot h = f(g)h$.

The canonical map $H_{hG} \to H/G = H/\mathrm{im} f$ has homotopy fiber given by $BK$ where $K = \ker f$.

Maybe more well-known that those are the corollaries for when $f$ is either injective or surjective:

If $G$ is a subgroup of $H$, the homotopy fiber of the map induced by the inclusion $BG \to BH$ is the coset space $H/G$.

If $1 \to K \to G \to H \to 1$ is a short exact sequence of topological groups, applying the classifying space functor gives a fiber sequence $BK \to BG \to BH$.

**EDIT**: I sketched a proof here. I'm mostly looking for references, but would also appreciate alternate proofs (specially a proof that avoids using the generalized Mather cube property on a diagram whose shape is not a 1-category).

**EDIT 2**: Tyler Lawson's nice example shows that more hypothesis are needed for part 2 of the "fact" and for corollary 1. My current guess is that for corollary 1, it is enough that $H \to H/G$ locally have a section.