Every definition comes with a cost: if you're making a definition then you need to make API for it. Would you be happy with the following approach?

lemma Vec.add_def {α n} [Add α] {v₁ v₂ : Vec α n} : v₁ + v₂ = Vec.add v₁ v₂ := rfl

theorem Vec.add_comm {α n} [AddCommMonoid α] {v₁ v₂ : Vec α n}
    : v₁ + v₂ = v₂ + v₁ := by
  rw [add_def]
  sorry