feat(library/data/finset/{basic,card,comb}.lean: add theorems, including card of an injective image

library/data/finset/basic.lean

@@ -463,6 +463,12 @@ quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h₁ h₂, h₁ a h₂)
 theorem subset_of_forall {s₁ s₂ : finset A} : (∀x, x ∈ s₁ → x ∈ s₂) → s₁ ⊆ s₂ :=
 quot.induction_on₂ s₁ s₂ (λ l₁ l₂ H, H)
 
+theorem subset_insert [h : decidable_eq A] (s : finset A) (a : A) : s ⊆ insert a s :=
+subset_of_forall (take x, assume H : x ∈ s, mem_insert_of_mem _ H)
+
+theorem eq_of_subset_of_subset {s₁ s₂ : finset A} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
+ext (take x, iff.intro (assume H, mem_of_subset_of_mem H₁ H) (assume H, mem_of_subset_of_mem H₂ H))
+
 /- upto -/
 section upto
 definition upto (n : nat) : finset nat :=

library/data/finset/card.lean

@@ -5,14 +5,14 @@ Author: Jeremy Avigad
 
 Cardinality calculations for finite sets.
 -/
-import data.finset.comb
+import data.finset.to_set data.set.function
 open nat eq.ops
 
 namespace finset
 
-variable {A : Type}
+variables {A B : Type}
-variable [deceq : decidable_eq A]
+variables [deceqA : decidable_eq A] [deceqB : decidable_eq B]
-include deceq
+include deceqA
 
 theorem card_add_card (s₁ s₂ : finset A) : card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) :=
 finset.induction_on s₂
@@ -58,4 +58,34 @@ calc
       ... = card s₁ + card (s₂ \ s₁) : card_union_of_disjoint H1
       ... ≥ card s₁                  : le_add_right
 
+section card_image
+open set
+include deceqB
+
+theorem card_image_eq_of_inj_on {f : A → B} {s : finset A} :
+  inj_on f (ts s) → card (image f s) = card s :=
+finset.induction_on s
+  (assume H : inj_on f (ts empty), calc
+    card (image f empty) = 0          : card_empty
+                     ... = card empty : card_empty)
+  (take t a,
+    assume H : a ∉ t,
+    assume IH : inj_on f (ts t) → card (image f t) = card t,
+    assume H1 : inj_on f (ts (insert a t)),
+    have H2 : ts t ⊆ ts (insert a t), by rewrite [-subset_eq_to_set_subset]; apply subset_insert,
+    have H3 : card (image f t) = card t, from IH (inj_on_of_inj_on_of_subset H1 H2),
+    have H4 : f a ∉ image f t,
+      proof
+        assume H5 : f a ∈ image f t,
+        obtain x (H6 : x ∈ t ∧ f x = f a), from exists_of_mem_image H5,
+        have H7 : x = a, from H1 (mem_insert_of_mem _ (and.left H6)) !mem_insert (and.right H6),
+        show false, from H (H7 ▸ and.left H6)
+      qed,
+    calc
+      card (image f (insert a t)) = card (insert (f a) (image f t)) : image_insert
+                              ... = card (image f t) + 1            : card_insert_of_not_mem H4
+                              ... = card t + 1                      : H3
+                              ... = card (insert a t)               : card_insert_of_not_mem H)
+end card_image
+
 end finset

library/data/finset/comb.lean

@@ -27,6 +27,11 @@ rfl
 theorem mem_image_of_mem (f : A → B) {s : finset A} {a : A} : a ∈ s → f a ∈ image f s :=
 quot.induction_on s (take l, assume H : a ∈ elt_of l, mem_to_finset (mem_map f H))
 
+theorem mem_image_of_mem_of_eq {f : A → B} {s : finset A} {a : A} {b : B}
+    (H1 : a ∈ s) (H2 : f a = b) :
+  b ∈ image f s :=
+eq.subst H2 (mem_image_of_mem f H1)
+
 theorem exists_of_mem_image {f : A → B} {s : finset A} {b : B} :
   b ∈ image f s → ∃a, a ∈ s ∧ f a = b :=
 quot.induction_on s
@@ -37,10 +42,39 @@ theorem mem_image_iff (f : A → B) {s : finset A} {y : B} : y ∈ image f s ↔
 iff.intro exists_of_mem_image
   (assume H,
     obtain x (H1 : x ∈ s ∧ f x = y), from H,
-    eq.subst (and.right H1) (mem_image_of_mem f (and.left H1)))
+    mem_image_of_mem_of_eq (and.left H1) (and.right H1))
 
 theorem mem_image_eq (f : A → B) {s : finset A} {y : B} : y ∈ image f s = ∃x, x ∈ s ∧ f x = y :=
 propext (mem_image_iff f)
+
+theorem mem_image_of_mem_image_of_subset {f : A → B} {s t : finset A} {y : B}
+    (H1 : y ∈ image f s) (H2 : s ⊆ t) : y ∈ image f t :=
+obtain x (H3: x ∈ s ∧ f x = y), from exists_of_mem_image H1,
+have H4 : x ∈ t, from mem_of_subset_of_mem H2 (and.left H3),
+show y ∈ image f t, from mem_image_of_mem_of_eq H4 (and.right H3)
+
+theorem image_insert [h' : decidable_eq A] (f : A → B) (s : finset A) (a : A) :
+  image f (insert a s) = insert (f a) (image f s) :=
+ext (take y, iff.intro
+  (assume H : y ∈ image f (insert a s),
+    obtain x (H1 : x ∈ insert a s ∧ f x = y), from exists_of_mem_image H,
+    have H2 : x = a ∨ x ∈ s, from eq_or_mem_of_mem_insert (and.left H1),
+    or.elim H2
+      (assume H3 : x = a,
+        have H4 : f a = y, from eq.subst H3 (and.right H1),
+        show y ∈ insert (f a) (image f s), from eq.subst H4 !mem_insert)
+      (assume H3 : x ∈ s,
+        have H4 : f x = y, from and.right H1,
+        have H5 : f x ∈ image f s, from mem_image_of_mem f H3,
+        show y ∈ insert (f a) (image f s), from eq.subst H4 (mem_insert_of_mem _ H5)))
+  (assume H : y ∈ insert (f a) (image f s),
+    have H1 : y = f a ∨ y ∈ image f s, from eq_or_mem_of_mem_insert H,
+    or.elim H1
+      (assume H2 : y = f a,
+        have H3 : f a ∈ image f (insert a s), from mem_image_of_mem f !mem_insert,
+        show y ∈ image f (insert a s), from eq.subst (eq.symm H2) H3)
+      (assume H2 : y ∈ image f s,
+        show y ∈ image f (insert a s), from mem_image_of_mem_image_of_subset H2 !subset_insert)))
 end image
 
 /- filter and set-builder notation -/

library/data/set/function.lean

@@ -96,6 +96,12 @@ assume  H1 : g (f x1) = g (f x2),
 have    H2 : f x1 = f x2, from Hg fx1b fx2b H1,
 show x1 = x2, from Hf x1a x2a H2
 
+theorem inj_on_of_inj_on_of_subset {f : X → Y} {a b : set X} (H1 : inj_on f b) (H2 : a ⊆ b) :
+  inj_on f a :=
+take x1 x2 : X, assume (x1a : x1 ∈ a) (x2a : x2 ∈ a),
+assume H : f x1 = f x2,
+show x1 = x2, from H1 (H2 x1a) (H2 x2a) H
+
 /- surjectivity -/
 
 definition surj_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := b ⊆ f '[a]