feat(Data/Fintype/Card): existsUnique_notMem_image_of_injective_of_card_succ (#37720)

This pull requests adds a small theorem `existsUnique_notMem_image_of_injective_of_card_succ` to `Mathlib/Data/Fintype/Card` that says given an injective map f : α → β such that β has cardinality one more than α, there exists a unique element of β not in the image of f. 

This can be viewed as going in the opposite direction of `card_lt_of_injective_of_notMem`. 

This little fact is needed for our Latin Square PR #36698.

Co-authored-by: Christopher J. R. Lloyd <cjl8zf@virginia.edu>
Co-authored-by: George H. Seelinger <ghseeli@gmail.com>

Author: cjrl

Mathlib/Data/Finset/Card.lean

@@ -680,6 +680,9 @@ theorem card_eq_one : #s = 1 ↔ ∃ a, s = {a} := by
   cases s
   simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]
 
+theorem card_eq_one_iff_existsUnique : #s = 1 ↔ ∃! a, a ∈ s := by
+  simp [card_eq_one, Finset.singleton_iff_unique_mem]
+
 theorem exists_eq_insert_iff [DecidableEq α] :
     (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t := by
   constructor
@@ -738,6 +741,16 @@ theorem one_lt_card_iff_nontrivial : 1 < #s ↔ s.Nontrivial := by
   rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
     not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]
 
+/-- Given an injective map `f : α → β` for finite sets `s ⊂ α` and `t ⊂ β` such that `t` has
+    cardinality one more than `s`, there exists a unique element of `t` not in `f(s)`. -/
+theorem existsUnique_notMem_image_of_injOn_of_card_eq_add_one
+    {t : Finset β} [DecidableEq β]
+    (hf : Set.InjOn f s) (hf' : Set.MapsTo f s t) (h : #t = #s + 1) :
+    ∃! x, x ∈ t ∧ x ∉ s.image f := by
+  have : #(t \ s.image f) = 1 := by
+    grind [card_sdiff_of_subset hf'.finsetImage_subset, card_image_of_injOn hf]
+  simpa [card_eq_one_iff_existsUnique] using this
+
 /-- If a Finset in a Pi type is nontrivial (has at least two elements), then
   its projection to some factor is nontrivial, and the fibers of the projection
   are proper subsets. -/

Mathlib/Data/Fintype/Card.lean

@@ -255,6 +255,13 @@ theorem card_lt_of_injective_of_notMem (f : α → β) (h : Function.Injective f
       Finset.card_lt_univ_of_notMem (x := b) <| by
         rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]
 
+/-- Given an injective map `f : α → β` such that `β` has cardinality one more
+than `α`, there exists a unique element of `β` not in the image of `f`. -/
+theorem existsUnique_notMem_image_of_injective_of_card_eq_add_one [DecidableEq β]
+    (f : α → β) (hf : f.Injective) (h : card β = card α + 1) : ∃! x, x ∉ univ.image f := by
+    simpa using existsUnique_notMem_image_of_injOn_of_card_eq_add_one
+      (s := .univ) (t := .univ) (Set.injOn_of_injective hf) (by simp) (by simpa)
+
 theorem card_lt_of_injective_not_surjective (f : α → β) (h : Function.Injective f)
     (h' : ¬Function.Surjective f) : card α < card β :=
   let ⟨_y, hy⟩ := not_forall.1 h'