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