simp only [totalDegree_X_pow, ← two_mul]
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ ((s.toEnumFinset.attach.sup fun i => (X i ^ (p - 1)).totalDegree) +
      s.toEnumFinset.attach.sup fun a => (X a ^ (p - 1)).totalDegree) <
    2 * p - 1
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ (2 * s.toEnumFinset.attach.sup fun i => p - 1) < 2 * p - 1