no goals
n : ℕ
⊢ ¬(n + 1, 0) ∈
      map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
        (antidiagonal n)
simp
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (n + 1, 0)
        (map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        (_ :
          ¬(n + 1, 0) ∈
              map
                (Function.Embedding.prodMap (Function.Embedding.refl ℕ)
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))).val
n : ℕ
⊢ antidiagonal (n + 1) =
    cons (n + 1, 0)
      (map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
        (antidiagonal n))
      (_ :
        ¬(n + 1, 0) ∈
            map
              (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
              (antidiagonal n))
apply eq_of_veq
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map
        (↑(Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (n + 1, 0)
        (map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        (_ :
          ¬(n + 1, 0) ∈
              map
                (Function.Embedding.prodMap (Function.Embedding.refl ℕ)
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))).val
rw [cons_val, map_val]
no goals
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map
        (↑(Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val
exact Multiset.Nat.antidiagonal_succ'