feat(data/finset): inj on of image card eq (#6785)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/finset/basic.lean

@@ -1724,7 +1724,7 @@ theorem image_to_finset [decidable_eq α] {s : multiset α} :
   s.to_finset.image f = (s.map f).to_finset :=
 ext $ λ _, by simp only [mem_image, multiset.mem_to_finset, exists_prop, multiset.mem_map]
 
-theorem image_val_of_inj_on (H : ∀x∈s, ∀y∈s, f x = f y → x = y) : (image f s).1 = s.1.map f :=
+theorem image_val_of_inj_on (H : set.inj_on f s) : (image f s).1 = s.1.map f :=
 multiset.erase_dup_eq_self.2 (nodup_map_on H s.2)
 
 @[simp]
@@ -1995,9 +1995,27 @@ theorem card_image_le [decidable_eq β] {f : α → β} {s : finset α} : card (
 by simpa only [card_map] using (s.1.map f).to_finset_card_le
 
 theorem card_image_of_inj_on [decidable_eq β] {f : α → β} {s : finset α}
-  (H : ∀x∈s, ∀y∈s, f x = f y → x = y) : card (image f s) = card s :=
+  (H : set.inj_on f s) : card (image f s) = card s :=
 by simp only [card, image_val_of_inj_on H, card_map]
 
+theorem inj_on_of_card_image_eq [decidable_eq β] {f : α → β} {s : finset α}
+  (H : card (image f s) = card s) :
+  set.inj_on f s :=
+begin
+  change (s.1.map f).erase_dup.card = s.1.card at H,
+  have : (s.1.map f).erase_dup = s.1.map f,
+  { apply multiset.eq_of_le_of_card_le,
+    { apply multiset.erase_dup_le },
+    rw H,
+    simp only [multiset.card_map] },
+  rw multiset.erase_dup_eq_self at this,
+  apply inj_on_of_nodup_map this,
+end
+
+theorem card_image_eq_iff_inj_on [decidable_eq β] {f : α → β} {s : finset α} :
+  (s.image f).card = s.card ↔ set.inj_on f s :=
+⟨inj_on_of_card_image_eq, card_image_of_inj_on⟩
+
 theorem card_image_of_injective [decidable_eq β] {f : α → β} (s : finset α)
   (H : injective f) : card (image f s) = card s :=
 card_image_of_inj_on $ λ x _ y _ h, H h

src/data/list/nodup.lean

@@ -127,6 +127,23 @@ theorem nodup_map_on {f : α → β} {l : list α} (H : ∀x∈l, ∀y∈l, f x
   (d : nodup l) : nodup (map f l) :=
 pairwise_map_of_pairwise _ (by exact λ a b ⟨ma, mb, n⟩ e, n (H a ma b mb e)) (pairwise.and_mem.1 d)
 
+theorem inj_on_of_nodup_map {f : α → β} {l : list α} (d : nodup (map f l)) :
+  ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → f x = f y → x = y :=
+begin
+  induction l with hd tl ih,
+  { simp },
+  { simp only [map, nodup_cons, mem_map, not_exists, not_and, ←ne.def] at d,
+    rintro _ (rfl | h₁) _ (rfl | h₂) h₃,
+    { refl },
+    { apply (d.1 _ h₂ h₃.symm).elim },
+    { apply (d.1 _ h₁ h₃).elim },
+    { apply ih d.2 h₁ h₂ h₃ } }
+end
+
+theorem nodup_map_iff_inj_on {f : α → β} {l : list α} (d : nodup l) :
+  nodup (map f l) ↔ (∀ (x ∈ l) (y ∈ l), f x = f y → x = y) :=
+⟨inj_on_of_nodup_map, λ h, nodup_map_on h d⟩
+
 theorem nodup_map {f : α → β} {l : list α} (hf : injective f) : nodup l → nodup (map f l) :=
 nodup_map_on (assume x _ y _ h, hf h)
 

src/data/multiset/nodup.lean

@@ -94,6 +94,14 @@ theorem nodup_map {f : α → β} {s : multiset α} (hf : function.injective f)
   nodup s → nodup (map f s) :=
 nodup_map_on (λ x _ y _ h, hf h)
 
+theorem inj_on_of_nodup_map {f : α → β} {s : multiset α} :
+  nodup (map f s) → ∀ (x ∈ s) (y ∈ s), f x = f y → x = y :=
+quot.induction_on s $ λ l, inj_on_of_nodup_map
+
+theorem nodup_map_iff_inj_on {f : α → β} {s : multiset α} (d : nodup s) :
+  nodup (map f s) ↔ (∀ (x ∈ s) (y ∈ s), f x = f y → x = y) :=
+⟨inj_on_of_nodup_map, λ h, nodup_map_on h d⟩
+
 theorem nodup_filter (p : α → Prop) [decidable_pred p] {s} : nodup s → nodup (filter p s) :=
 quot.induction_on s $ λ l, nodup_filter p