Vandermonde's identity

import Mathlib

theorem vandermonde (m n r : ℕ) : Nat.choose (m + n) r = ∑ k ∈ Finset.range (r + 1), Nat.choose m k * Nat.choose n (r - k) :=by
  rw [Nat.add_choose_eq]
  rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]