Coarea inequality, Eilenberg inequality The general statement of the coarea inequality known also as the Eilenberg inequality is:

Theorem. If $f:X\to Y$ is a Lipschitz map between metric spaces and $A\subset X$, $0\leq m\leq n$, then $$
 \int_Y^*\mathcal{H}^{n-m}(f^{-1}(y)\cap A)\, d\mathcal{H}^m(y)\leq 
 (\operatorname{Lip}
 f)^m\frac{\omega_{n-m}\omega_m}{\omega_n}\mathcal{H}^n(A). $$

Federer proved it (Theorem 2.10.25 in [2]) under additional assumptions. Then Davies [1] showed that these additional assumptions are not necessary and a reader may find a detailed proof in [3].
For a related discussion, see
Open problems in Federer's Geometric Measure Theory
My questions is that I am not exactly sure what are the assumptions in the theorem:

Question 1. Is it assumed here that the spaces $X$ and $Y$ are separable?
Question 2. Are $0\leq m\leq n$ any real numbers of just integers?

[1] R. O. Davies, Increasing sequences of sets and Hausdorff measure, Proc.  London  Math.  Soc. 20(1970), 222-236.
[2] H. Federer, Geometric  measure  theory. Die  Grundlehren  der  mathematischen  Wissenschaften,Band 153 Springer-Verlag New York Inc., New York 1969.
[3] L. P. Reichel, The coarea formula for metric space valued maps, Ph.D. thesis, ETH Z ̈urich, 2009.
http://e-collection.library.ethz.ch/eserv/eth:289/eth-289-02.pdf.
Edit. $X$ and $Y$ can be any metric spaces and $0\leq m\leq n$ any real numbers. For a complete and detailed proof as well as historical account see:
[4] B. Esmayli, P. Hajlasz, The Coarea Inequality.
https://arxiv.org/abs/2006.00419.
The proof presented in [4] is elementary thanks to Fedja's help through Mathoverflow: Bounding an "integral" from below by the Hausdorff measure of the domain.
 A: The theorem, as stated, is true for arbitrary metric spaces and for any pair of non-negative real numbers. Precisely,
Theorem (Co-area Inequality). If $f:X\to Y$ is a Lipschitz map between any metric spaces and an $0\leq m\leq n < \infty$ are any any pair of real numbers, then for any $ A \subset X$,
$$
 \int_Y^*\mathcal{H}^{n-m}(f^{-1}(y)\cap A)\, d\mathcal{H}^m(y)\leq 
 (\operatorname{Lip}
 f)^m\frac{\omega_{n-m}\omega_m}{\omega_n}\mathcal{H}^n(A) \, . 
$$
Federer [1, 2.10.25] proved the theorem under the assumption that $Y$ is boundedly compact, that is, every bounded and closed set in $Y$ is compact. He needed this assumption because he proved the following lemma [1, 2.10.22] only under the same restriction. The lemma is needed in the proof of the coarea inequality.
Lemma (increasing sets lemma). Let $(X,d)$ be any metric space,  $0 \leq s < \infty$ and $ 0 < \delta < \infty$. Then for any increasing set of subset $E_1 \subset E_2 \subset \cdots $,
$$
\mathcal{H}^s_\delta (\bigcup_{i=1}^\infty E_i) = \lim_{i \to \infty} \mathcal{H}^s_\delta (E_i) \, .
$$ 
Years later, Davies proved this lemma under no restrictions on the metric space and commented that Federer tells him that this makes the extra assumptions for his co-area inequality "superfluous."
A well-written exposition of the proof of the co-area inequality can be found in Reichel's thesis [2], where he follows Federer's original proof while using the result of Davies.
[1] H. Federer, Geometric  measure  theory. Die  Grundlehren  der  mathematischen  Wissenschaften,Band 153 Springer-Verlag New York Inc., New York 1969.
[2] L. P. Reichel, The coarea formula for metric space valued maps, Ph.D. thesis, ETH Z ̈urich, 2009.
http://e-collection.library.ethz.ch/eserv/eth:289/eth-289-02.pdf
