feat(Data/Finset): add InjOn variants of image_{subset,eq}_image_iff (#39556)

These are useful for set family combinatorics

Author: b-mehta

Mathlib/Data/Finset/Image.lean

@@ -397,6 +397,17 @@ theorem image_subset_image_iff {t : Finset α} (hf : Injective f) :
     s.image f ⊆ t.image f ↔ s ⊆ t :=
   mod_cast Set.image_subset_image_iff hf (s := s) (t := t)
 
+/-- Variant of `Finset.image_subset_image_iff` under an `InjOn` rather than `Injective`
+hypothesis. -/
+theorem image_subset_image_iff_of_injOn {s₁ s₂ : Finset α} (ht : (s : Set α).InjOn f)
+    (h₁ : s₁ ⊆ s) (h₂ : s₂ ⊆ s) : s₁.image f ⊆ s₂.image f ↔ s₁ ⊆ s₂ := by
+  exact_mod_cast ht.image_subset_image_iff (mod_cast h₁) (mod_cast h₂)
+
+/-- Variant of `Finset.image_inj` under an `InjOn` rather than `Injective` hypothesis. -/
+theorem image_eq_image_iff_of_injOn {s₁ s₂ : Finset α} (ht : (s : Set α).InjOn f)
+    (h₁ : s₁ ⊆ s) (h₂ : s₂ ⊆ s) : s₁.image f = s₂.image f ↔ s₁ = s₂ := by
+  exact_mod_cast ht.image_eq_image_iff (mod_cast h₁) (mod_cast h₂)
+
 lemma image_ssubset_image {t : Finset α} (hf : Injective f) : s.image f ⊂ t.image f ↔ s ⊂ t := by
   simp_rw [← lt_iff_ssubset]
   exact lt_iff_lt_of_le_iff_le' (image_subset_image_iff hf) (image_subset_image_iff hf)

Mathlib/Data/Finset/Powerset.lean

@@ -78,6 +78,13 @@ theorem image_injOn_powerset_of_injOn {β : Type*} [DecidableEq β] {f : α →
   have {z a} (_ : z ⊆ s) (_ : a ∈ s) : a ∈ z ↔ f a ∈ z.image f := by grind [H.eq_iff]
   exact fun _ _ _ _ _ => by grind
 
+/-- Variant of `Finset.image_injOn_powerset_of_injOn` for a family `S` of finsets whose
+union supports an `InjOn` hypothesis, rather than the full powerset of a set. -/
+theorem injOn_image_of_biUnion_injOn {β : Type*} [DecidableEq α] [DecidableEq β]
+    {S : Finset (Finset α)} {f : α → β} (hf : (S.biUnion id : Set α).InjOn f) :
+    (S : Set (Finset α)).InjOn (·.image f) :=
+  (image_injOn_powerset_of_injOn hf).mono (by aesop (add simp Set.subset_def))
+
 /-- `s.biUnion id ⊆ t` iff every member of `s` is a subset of `t`, i.e. `s ⊆ t.powerset`. -/
 lemma biUnion_id_subset_iff_subset_powerset [DecidableEq α] {s : Finset (Finset α)} :
     s.biUnion id ⊆ t ↔ s ⊆ t.powerset := by