∀ {α : Type u_1} (a : α) (s : Multiset α),
  (a ::ₘ s).antidiagonal =
    Multiset.map (Prod.map id (Multiset.cons a)) s.antidiagonal +
      Multiset.map (Prod.map (Multiset.cons a) id) s.antidiagonal