feat(data/finset): add card_insert_of_mem (#3137)

src/data/finset.lean

@@ -1404,6 +1404,9 @@ by cases s; simp only [multiset.card_eq_one, finset.card, ← val_inj, singleton
 by simpa only [card_cons, card, insert_val] using
 congr_arg multiset.card (ndinsert_of_not_mem h)
 
+theorem card_insert_of_mem [decidable_eq α] {a : α} {s : finset α}
+  (h : a ∈ s) : card (insert a s) = card s := by rw insert_eq_of_mem h
+
 theorem card_insert_le [decidable_eq α] (a : α) (s : finset α) : card (insert a s) ≤ card s + 1 :=
 by by_cases a ∈ s; [{rw [insert_eq_of_mem h], apply nat.le_add_right},
 rw [card_insert_of_not_mem h]]