α : Type u
⊢ Multiset.toFinset
      (Multiset.map (Prod.map ↑Multiset.toFinsupp ↑Multiset.toFinsupp) (Multiset.antidiagonal (↑toMultiset 0))) =
    {(0, 0)}
α : Type u
⊢ antidiagonal 0 = {(0, 0)}
rw [antidiagonal, antidiagonal', Multiset.toFinsupp_support]
no goals
α : Type u
⊢ Multiset.toFinset
      (Multiset.map (Prod.map ↑Multiset.toFinsupp ↑Multiset.toFinsupp) (Multiset.antidiagonal (↑toMultiset 0))) =
    {(0, 0)}
rfl