Auxiliary file: tsum_one_div_w_mul_q_pow_c—Theorem 2 (p.1031)

The mass formula proper: for any set R of representatives of the isomorphism classes of the elements of sigma K n, the sum of 1 / ((w M.1 : ℝ≥0∞) * (q K : ℝ≥0∞) ^ c M.1) over M in R is 1 ([Serre 1978, Theorem 2, p.1031][Serre1978]). It is Theorem 1 regrouped along the partition of sigma K n into isomorphism classes:

• c is an invariant of the K-isomorphism class (c_eq_of_algEquiv): discIdeal is defined from the integral K-bases of the subextension alone, and a K-isomorphism carries the integral bases of the one field onto those of the other with the same discriminant (Algebra.discr_eq_discr_of_algEquiv), so discIdeal—hence d, hence c—transports, with no contact with integers or the ramification data.
• Grouping the terms of Theorem 1 by the representative of the class (ENNReal.tsum_fiberwise, over ℝ≥0∞ where no rearrangement needs justifying) makes each class contribute its cardinality times 1 / q ^ c; the class is finite of cardinality n / w by Remark 3° (ncard_isomorphic_mul_w), which is also what evaluates the constant inner sum.
• The regrouped identity reads n = the sum over R of (n / w M) * (1 / q ^ c M); cancelling n—legitimate in ℝ≥0∞ since 0 < n and n ≠ ⊤—is the theorem.

References

• [Serre1978] J-P. Serre, Une «formule de masse» pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris 286 (1978), Série A, 1031–1036.

theorem MassFormula.tsum_one_div_w_mul_q_pow_c (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) (R : Set (IntermediateField K (SeparableClosure K))) (hR : IsRepresentativeSet n R) : ∑' (M : ↑R), 1 / (↑(w ↑M) * ↑(q K) ^ c ↑M) = 1

The sum of 1 / ((w M.1 : ℝ≥0∞) * (q K : ℝ≥0∞) ^ c M.1) over any set R of representatives of the isomorphism classes of the elements of sigma K n is 1 ([Serre 1978, Theorem 2, p.1031][Serre1978]). Theorem 1 is regrouped along the fibers of the map sending a member of sigma K n to its representative: each fiber is the isomorphism class of its representative, finite of cardinality n / w by Remark 3° (ncard_isomorphic_mul_w), and c is constant on it (c_eq_of_algEquiv), so the fiber contributes (n / w) * (1 / q ^ c); cancelling n from the resulting identity is the claim.