Homotopy fiber of a map between classifying spaces

Question

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$.

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

2. 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:

1. 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$.

2. 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.

Answer 1

One source for some of this is section 8 of May's "Classifying spaces and fibrations"

He has G and H interchanged, unfortunately uses a coset notation for what turns out to be the homotopy fibre, and doesn't talk about the special cases you are after (his interest was more in the topological monoid case).

May is using the two-sided bar construction.

Your sketch doesn't say very much about the topologies involved, and I did wonder if, for example, you need $im f$ closed for your coset space identification.