feat(Data): add List.length_eq_succ_iff and Multiset.card_eq_succ_iff (leanprover-community#38271)

We already have the Finset version, this PR adds the List and Multiset versions.

Author: b-mehta

Mathlib/Data/List/Basic.lean

@@ -95,6 +95,10 @@ theorem exists_of_length_succ {n} : ∀ l : List α, l.length = n + 1 → ∃ h
   | [], H => absurd H.symm <| succ_ne_zero n
   | h :: t, _ => ⟨h, t, rfl⟩
 
+theorem length_eq_succ_iff {n} {l : List α} :
+    l.length = n + 1 ↔ ∃ h t, h :: t = l ∧ t.length = n := by
+  grind [cases List]
+
 @[simp] lemma length_injective_iff : Injective (List.length : List α → ℕ) ↔ Subsingleton α := by
   constructor
   · intro h; refine ⟨fun x y => ?_⟩; (suffices [x] = [y] by simpa using this); apply h; rfl

Mathlib/Data/Multiset/ZeroCons.lean

@@ -466,6 +466,11 @@ theorem card_eq_four {s : Multiset α} : card s = 4 ↔ ∃ x y z w, s = {x, y,
         Exists.imp fun _b => Exists.imp fun _c => Exists.imp fun _d => congr_arg _,
     fun ⟨_a, _b, _c, _d, e⟩ => e.symm ▸ rfl⟩
 
+theorem card_eq_succ_iff {s : Multiset α} {n : ℕ} :
+    card s = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ card t = n := by
+  refine ⟨?_, by aesop⟩
+  induction s using Multiset.induction generalizing n with aesop
+
 /-! ### Map for partial functions -/
 
 @[simp]