refine (add_le_add (totalDegree_finset_sum _ _) $ (totalDegree_finset_sum _ _).trans $
  Finset.sup_mono_fun fun a _ ↦ totalDegree_smul_le _ _).trans_lt ?_
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ (ZMod.f₁ s).totalDegree + (ZMod.f₂ s).totalDegree < 2 * p - 1
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