Gauge fixing, Lorentz invariance and positive definite metric of Hilbert space Updated 0n ${\bf 02.04.2020}$

$\large{\bf Context}$ 
In the first $3$ minutes of this video lecture (based on the presentation here) on the subject matter of Goldstone theorem without Lorentz invariance by Hitoshi Murayama, he recalls that the derivation of Goldstone theorem relies on (i) Lorentz invariance of the theory and (ii) the positive definite metric of the Hilbert space.
Then he asserts that the Higgs mechanism either (i) violates Lorentz invariance by gauge fixing or (ii) violates positive definiteness of the metric to maintain Lorentz invariance.
Here is the Nobel Lecture: Evading Goldstone theorem by Peter Higgs, where he makes a similar remark:

There was an obstacle to the success of the Nambu-Goldstone program.

and then quotes from a paper by Goldstone, Salam and Weinberg,

''In a manifestly Lorentz-invariant quantum field theory, if there is a continuous symmetry under which the Lagrangian is invariant, then either the vacuum state is also invariant or there must exist spinless particles of zero mass.''

Given this context, I have a few questions.

$\large{\bf Questions}$ 
$1$.  Frankly speaking, I am not sure which step(s) of the derivation of Goldstone theorem requires the assumptions (i) and (ii) and how it fails in the description of the Higgs mechanism. Maybe someone can point it out before answering questions $1$ and $2$. The derivation that I am familiar with can be found in page $540$ of Quantum Field Theory by Itzykson and Zuber.
Is there better proof in the literature which makes clear use of the assumptions (i) and (ii)?
$2.$ He says that gauge fixing breaks Lorentz invariance. But in what sense? Ordinarily, spacetime symmetries are not allowed to be spontaneously broken in a Lorentz-invariant theory. Does he have something like Coumob gauge in mind (as AccidentalFourierTransform points out in his comment) which lacks manifest Lorentz invariance?
$3.$ How is it that if Lorentz invariance needs to be maintained, as in the positive definiteness of the metric of the Hilbert space has to be sacrificed? Does he refer to here covariant quantization in Lorentz gauge?
 A: It is difficult to extract precise statements from a couple of sentences in a talk. FWIW, we have the following comments: 


*

*The standard Goldstone theorem assumes Lorentz covariance, e.g. to have a relativistic dispersion relation.

*A QFT must have a positive definite physical Hilbert space ${\cal H}_{\rm phys}$ to begin with in order to be consistent and have non-negative$^1$ probabilities. 
In other words this requirement is at a more fundamental level than Goldstone's theorem, and must in principle always be assumed whenever we discuss various aspects of QFT, such as, Goldstone's theorem. 
That said, when we consider the standard proof of Goldstone's theorem in a (possibly extended) Hilbert space ${\cal H}$ that is not necessarily positive definite, we still deduce a massless mode in ${\cal H}$. The caveat is of course that the massless mode could belong to an unphysical sector of the (extended) Hilbert space ${\cal H}$, cf. the BRST formalism.  
--
$^1$ That only requires a semi-positive definite Hilbert space, but one can always take quotient with the seminorm kernel to get a positive definite Hilbert space. 
A: A simpler discussion can be found in the following articles:
$1.$ Scholarpedia article titled Englert-Brout-Higgs-Guralnik-Hagen-Kibble mechanism by Tom Kibble,
$2.$ Spontaneous symmetry breaking in gauge theories by Tom Kibble,
$3.$ SSB and the Brout Englert Higgs Mechanism Beyond the Standard Model-a video lecture by Jean Iliopoulos. 

The proof of (quantum) Goldstone's theorem requires (i) manifest Lorentz variance and (ii) positive definite metric of the Hilbert space of states. Now consider the ${\rm U(1)}$ gauge theory where the gauge field $A_\mu$ is coupled to complex scalar field $\phi$. However, quantization of a gauge theory requires us to fix a gauge. But exists is no choice of gauge where both the conditions (i) and (ii) are simultaneously satisfied. 
For the choice of Coulomb gauge, though the Hilbert space contains only physical states, the gauge itself is not manifestly covariant. In this case, the continuity equation $\partial_\mu j^\mu=0$ does not imply $k^\mu f_\mu(k)=0$ where $$f_\mu(k)=-i\int d^4x e^{ikx}\langle 0|[\hat{j}^\mu(x),\hat{\phi}(0)]|0\rangle\tag{1}$$ because certain commutator does not vanish large spacelike intervals! This is how Goldstone theorem is evaded in this gauge. For further references, see page $210$, Gauge Theories in Particle Physics by Aitchison and Hey and references therein [Guralnik et al ($1968$) and Bernstein ($1974$)].
The Lorenz gauge, though manifestly Lorentz covariant, quantization with Gupta-Bleuler method leads to a Hilbert space that necessarily consists of states of unphysical scalar and longitudinal photons. Here, Goldstone theorem does apply but the scalar Goldstone mode is unphysical (for example, the pole of the propagator i.e., the mass, is gauge-dependent).
For completeness, it's worth to mention that the gauge symmetry cannot be spontaneously broken because the after the gauge fixing term is added to the Lagrangian, it no longer has gauge invariance, and therfore, the question of its spontaneous breakdown does not arise. Please see 1 and 2. 
