feat(group_theory): add a little bit of group theory; prove of Lagran…

…ge's theorem

data/equiv.lean

@@ -8,7 +8,7 @@ We say two types are equivalent if they are isomorphic.
 
 Two equivalent types have the same cardinality.
 -/
-import data.prod data.nat.pairing logic.function tactic data.set.basic
+import data.prod data.nat.pairing logic.function tactic data.set.lattice
 import algebra.group
 open function
 
@@ -476,6 +476,12 @@ def subtype_equiv_of_subtype {p : α → Prop} : Π (e : α ≃ β), {a : α //
    assume p, by simp [map_comp, l.f_g_eq_id]; rw [map_id]; refl,
    assume p, by simp [map_comp, r.f_g_eq_id]; rw [map_id]; refl⟩
 
+def subtype_subtype_equiv_subtype {α : Type u} (p : α → Prop) (q : subtype p → Prop) :
+  subtype q ≃ {a : α // ∃h:p a, q ⟨a, h⟩ } :=
+⟨λ⟨⟨a, ha⟩, ha'⟩, ⟨a, ha, ha'⟩,
+  λ⟨a, ha⟩, ⟨⟨a, ha.cases_on $ assume h _, h⟩, by cases ha; exact ha_h⟩,
+  assume ⟨⟨a, ha⟩, h⟩, rfl, assume ⟨a, h₁, h₂⟩, rfl⟩
+
 end
 
 namespace set
@@ -502,7 +508,7 @@ protected def singleton {α} (a : α) : ({a} : set α) ≃ unit :=
 ⟨λ _, (), λ _, ⟨a, mem_singleton _⟩,
  λ ⟨x, h⟩, by simp at h; subst x,
  λ ⟨⟩, rfl⟩
- 
+
 protected def insert {α} {s : set.{u} α} [decidable_pred s] {a : α} (H : a ∉ s) :
   (insert a s : set α) ≃ (s ⊕ unit) :=
 by rw ← union_singleton; exact
@@ -559,6 +565,29 @@ begin
   simp [set.set_coe_cast, (∘), set.range_iff_surjective.2 hg.2],
 end
 
+section
+open set
+set_option eqn_compiler.zeta true
+
+noncomputable def set.bUnion_eq_sigma_of_disjoint {α β} {s : set α} {t : α → set β}
+  (h : pairwise_on s (disjoint on t)) : (⋃i∈s, t i) ≃ (Σi:s, t i.val) :=
+let f : (Σi:s, t i.val) → (⋃i∈s, t i) := λ⟨⟨a, ha⟩, ⟨b, hb⟩⟩, ⟨b, mem_bUnion ha hb⟩ in
+have injective f,
+  from assume ⟨⟨a₁, ha₁⟩, ⟨b₁, hb₁⟩⟩ ⟨⟨a₂, ha₂⟩, ⟨b₂, hb₂⟩⟩ eq,
+  have b_eq : b₁ = b₂, from congr_arg subtype.val eq,
+  have a_eq : a₁ = a₂, from classical.by_contradiction $ assume ne,
+    have b₁ ∈ t a₁ ∩ t a₂, from ⟨hb₁, b_eq.symm ▸ hb₂⟩,
+    have t a₁ ∩ t a₂ ≠ ∅, from ne_empty_of_mem this,
+    this $ h _ ha₁ _ ha₂ ne,
+  sigma.eq (subtype.eq a_eq) (subtype.eq $ by subst b_eq; subst a_eq),
+have surjective f,
+  from assume ⟨b, hb⟩,
+  have ∃a∈s, b ∈ t a, by simpa using hb,
+  let ⟨a, ha, hb⟩ := this in ⟨⟨⟨a, ha⟩, ⟨b, hb⟩⟩, rfl⟩,
+(equiv.of_bijective ⟨‹injective f›, ‹surjective f›⟩).symm
+
+end
+
 section swap
 variable [decidable_eq α]
 open decidable

data/finset.lean

@@ -668,6 +668,8 @@ theorem card_erase_of_mem [decidable_eq α] {a : α} {s : finset α} : a ∈ s 
 
 theorem card_range (n : ℕ) : card (range n) = n := card_range n
 
+theorem card_attach {s : finset α} : card (attach s) = card s := multiset.card_attach
+
 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 :=
 by simp [card, image_val_of_inj_on H]
@@ -676,6 +678,24 @@ theorem card_image_of_injective [decidable_eq β] {f : α → β} (s : finset α
   (H : function.injective f) : card (image f s) = card s :=
 card_image_of_inj_on $ λ x _ y _ h, H h
 
+lemma card_eq_of_bijective [decidable_eq α] {s : finset α} {n : ℕ}
+  (f : ∀i, i < n → α)
+  (hf : ∀a∈s, ∃i, ∃h:i<n, f i h = a) (hf' : ∀i (h : i < n), f i h ∈ s)
+  (f_inj : ∀i j (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) :
+  card s = n :=
+have ∀ (a : α), a ∈ s ↔ ∃i (hi : i ∈ range n), f i (mem_range.1 hi) = a,
+  from assume a, ⟨assume ha, let ⟨i, hi, eq⟩ := hf a ha in ⟨i, mem_range.2 hi, eq⟩,
+    assume ⟨i, hi, eq⟩, eq ▸ hf' i (mem_range.1 hi)⟩,
+have s = ((range n).attach.image $ λi, f i.1 (mem_range.1 i.2)),
+  by simpa [ext],
+calc card s = card ((range n).attach.image $ λi, f i.1 (mem_range.1 i.2)) :
+    by rw [this]
+  ... = card ((range n).attach) :
+    card_image_of_injective _ $ assume ⟨i, hi⟩ ⟨j, hj⟩ eq,
+      subtype.eq $ f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq
+  ... = card (range n) : card_attach
+  ... = n : card_range n
+
 lemma card_eq_succ [decidable_eq α] {s : finset α} {a : α} {n : ℕ} :
   s.card = n + 1 ↔ (∃a t, a ∉ t ∧ insert a t = s ∧ card t = n) :=
 iff.intro
@@ -694,6 +714,20 @@ eq_of_veq $ multiset.eq_of_le_of_card_le (val_le_iff.mpr h) h₂
 lemma card_lt_card [decidable_eq α] {s t : finset α} (h : s ⊂ t) : s.card < t.card :=
 card_lt_of_lt (val_lt_iff.2 h)
 
+lemma card_le_card_of_inj_on [decidable_eq α] [decidable_eq β] {s : finset α} {t : finset β}
+  (f : α → β) (hf : ∀a∈s, f a ∈ t) (f_inj : ∀a₁∈s, ∀a₂∈s, f a₁ = f a₂ → a₁ = a₂) :
+  card s ≤ card t :=
+calc card s = card (s.image f) : by rw [card_image_of_inj_on f_inj]
+  ... ≤ card t : card_le_of_subset $
+    assume x hx, match x, finset.mem_image.1 hx with _, ⟨a, ha, rfl⟩ := hf a ha end
+
+lemma card_le_of_inj_on [decidable_eq α] {n} {s : finset α}
+  (f : ℕ → α) (hf : ∀i<n, f i ∈ s) (f_inj : ∀i j, i<n → j<n → f i = f j → i = j) : n ≤ card s :=
+calc n = card (range n) : (card_range n).symm
+  ... ≤ card s : card_le_card_of_inj_on f
+    (by simp; assumption)
+    (by simp; exact assume a₁ h₁ a₂ h₂, f_inj a₁ a₂ h₁ h₂)
+
 @[elab_as_eliminator] lemma strong_induction_on {p : finset α → Sort*} :
   ∀ (s : finset α), (∀s, (∀t ⊂ s, p t) → p s) → p s
 | ⟨s, nd⟩ ih := multiset.strong_induction_on s

data/fintype.lean

@@ -179,6 +179,14 @@ instance (α β : Type*) [fintype α] [fintype β] : fintype (α × β) :=
   fintype.card (α × β) = fintype.card α * fintype.card β :=
 card_product _ _
 
+def fintype.fintype_prod_left {α β} [decidable_eq α] [fintype (α × β)] [nonempty β] : fintype α :=
+⟨(fintype.elems (α × β)).image prod.fst,
+  assume a, let ⟨b⟩ := ‹nonempty β› in by simp; exact ⟨b, fintype.complete _⟩⟩
+
+def fintype.fintype_prod_right {α β} [decidable_eq β] [fintype (α × β)] [nonempty α] : fintype β :=
+⟨(fintype.elems (α × β)).image prod.snd,
+  assume b, let ⟨a⟩ := ‹nonempty α› in by simp; exact ⟨a, fintype.complete _⟩⟩
+
 instance (α : Type*) [fintype α] : fintype (ulift α) :=
 fintype.of_equiv _ equiv.ulift.symm
 

data/int/basic.lean

@@ -80,6 +80,20 @@ sub_lt_iff_lt_add.trans lt_add_one_iff
 theorem le_sub_one_iff {a b : ℤ} : a ≤ b - 1 ↔ a < b :=
 le_sub_iff_add_le
 
+protected lemma induction_on {p : ℤ → Prop}
+  (i : ℤ) (hz : p 0) (hp : ∀i, p i → p (i + 1)) (hn : ∀i, p i → p (i - 1)) : p i :=
+begin
+  induction i,
+  { induction i,
+    { exact hz },
+    { exact hp _ i_ih } },
+  { have : ∀n:ℕ, p (- n),
+    { intro n, induction n,
+      { simp [hz] },
+      { have := hn _ n_ih, simpa } },
+    exact this (i + 1) }
+end
+
 /- /  -/
 
 theorem of_nat_div (m n : nat) : of_nat (m / n) = (of_nat m) / (of_nat n) := rfl

data/multiset.lean

@@ -877,6 +877,8 @@ quot.induction_on s (λ l H, mem_pmap) H
   (s H) : card (pmap f s H) = card s :=
 quot.induction_on s (λ l H, length_pmap) H
 
+@[simp] theorem card_attach {m : multiset α} : card (attach m) = card m := card_pmap _ _ _
+
 @[simp] lemma attach_zero : (0 : multiset α).attach = 0 := rfl
 
 lemma attach_cons (a : α) (m : multiset α) :

data/set/finite.lean

@@ -13,7 +13,6 @@ open set lattice function
 universes u v w
 variables {α : Type u} {β : Type v} {ι : Sort w}
 
-
 namespace set
 
 /-- A set is finite if the subtype is a fintype, i.e. there is a
@@ -261,4 +260,26 @@ by simp [set.set_eq_def]
 @[simp] lemma coe_to_finset {s : set α} {hs : set.finite s} : ↑(hs.to_finset) = s :=
 by simp [set.set_eq_def]
 
-end finset
+end finset
+
+namespace set
+
+lemma infinite_univ_nat : infinite (univ : set ℕ) :=
+assume (h : finite (univ : set ℕ)),
+let ⟨n, hn⟩ := finset.exists_nat_subset_range h.to_finset in
+have n ∈ finset.range n, from finset.subset_iff.mpr hn $ by simp,
+by simp * at *
+
+lemma not_injective_nat_fintype [fintype α] [decidable_eq α] {f : ℕ → α} : ¬ injective f :=
+assume (h : injective f),
+have finite (f '' univ),
+  from finite_subset (finset.finite_to_set $ fintype.elems α) (assume a h, fintype.complete a),
+have finite (univ : set ℕ), from finite_of_finite_image h this,
+infinite_univ_nat this
+
+lemma not_injective_int_fintype [fintype α] [decidable_eq α] {f : ℤ → α} : ¬ injective f :=
+assume hf,
+have injective (f ∘ (coe : ℕ → ℤ)), from injective_comp hf $ assume i j, int.of_nat_inj,
+not_injective_nat_fintype this
+
+end set