feat(data/ordinal): universe lifts, alephs

algebra/big_operators.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Some big operators for lists and finite sets.
 -/
-import data.list data.list.perm data.set.finite data.finset
+import data.list.basic data.list.perm data.finset
   algebra.group algebra.ordered_group algebra.group_power
 
 universes u v w
@@ -191,6 +191,10 @@ prod_hom has_inv.inv one_inv mul_inv
 
 end comm_group
 
+@[simp] theorem card_sigma {σ : α → Type*} (s : finset α) (t : Π a, finset (σ a)) :
+  card (s.sigma t) = s.sum (λ a, card (t a)) :=
+multiset.card_sigma _ _
+
 end finset
 
 namespace finset

algebra/group_power.lean

@@ -99,6 +99,9 @@ end monoid
 theorem nat.pow_eq_pow (p q : ℕ) : nat.pow p q = p ^ q :=
 by induction q; [refl, simp [nat.pow_succ, pow_succ, mul_comm, *]]
 
+@[simp] theorem nat.smul_eq_mul (m n : ℕ) : m • n = m * n :=
+by induction n; simp [smul_succ', nat.mul_succ, *]
+
 /- commutative monoid -/
 
 section comm_monoid

algebra/module.lean

@@ -6,7 +6,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl
 Modules over a ring.
 -/
 
-import algebra.ring algebra.big_operators data.set.basic
+import algebra.ring algebra.big_operators data.set.lattice
 open function
 
 universes u v w x

data/cardinal.lean

@@ -256,11 +256,19 @@ namespace cardinal
 
 def mk : Type u → cardinal := quotient.mk
 
+@[simp] theorem mk_def (α : Type u) : @eq cardinal ⟦α⟧ (mk α) := rfl
+
 instance : has_le cardinal.{u} :=
 ⟨λq₁ q₂, quotient.lift_on₂ q₁ q₂ (λα β, nonempty $ embedding α β) $
   assume α β γ δ ⟨e₁⟩ ⟨e₂⟩,
     propext ⟨assume ⟨e⟩, ⟨e.congr e₁ e₂⟩, assume ⟨e⟩, ⟨e.congr e₁.symm e₂.symm⟩⟩⟩
 
+theorem le_mk_iff_exists_set {c : cardinal} {α : Type u} :
+  c ≤ mk α ↔ ∃ p : set α, mk p = c :=
+⟨quotient.induction_on c $ λ β ⟨⟨f, hf⟩⟩,
+  ⟨set.range f, eq.symm $ quot.sound ⟨equiv.set.range f hf⟩⟩,
+λ ⟨p, e⟩, e ▸ ⟨⟨subtype.val, λ a b, subtype.eq⟩⟩⟩
+
 instance : linear_order cardinal.{u} :=
 { le          := (≤),
   le_refl     := assume a, quot.induction_on a $ λ α, ⟨embedding.refl _⟩,
@@ -276,6 +284,8 @@ instance : distrib_lattice cardinal.{u} := by apply_instance
 
 instance : has_zero cardinal.{u} := ⟨⟦ulift empty⟧⟩
 
+instance : inhabited cardinal.{u} := ⟨0⟩
+
 theorem ne_zero_iff_nonempty {α : Type u} : @ne cardinal ⟦α⟧ 0 ↔ nonempty α :=
 not_iff_comm.1
   ⟨λ h, quotient.sound ⟨(equiv.empty_of_not_nonempty h).trans equiv.ulift.symm⟩,
@@ -334,8 +344,6 @@ instance : comm_semiring cardinal.{u} :=
   right_distrib := assume a b c,
     by rw [mul_comm (a + b) c, left_distrib c a b, mul_comm c a, mul_comm c b] }
 
-def ω : cardinal.{u} := ⟦ulift ℕ⟧
-
 protected def power (a b : cardinal.{u}) : cardinal.{u} :=
 quotient.lift_on₂ a b (λα β, ⟦β → α⟧) $ assume α₁ α₂ β₁ β₂ ⟨e₁⟩ ⟨e₂⟩,
   quotient.sound ⟨equiv.arrow_congr e₂ e₁⟩
@@ -463,6 +471,33 @@ protected theorem wf : @well_founded cardinal.{u} (<) :=
 
 instance has_wf : @has_well_founded cardinal.{u} := ⟨(<), cardinal.wf⟩
 
+def succ (c : cardinal) : cardinal :=
+@min {c' // c < c'} ⟨⟨_, cantor _⟩⟩ subtype.val 
+
+theorem lt_succ_self (c : cardinal) : c < succ c :=
+by cases min_eq _ with s e; rw [succ, e]; exact s.2
+
+theorem succ_le {a b : cardinal} : succ a ≤ b ↔ a < b :=
+⟨lt_of_lt_of_le (lt_succ_self _), λ h,
+  by exact @min_le _ ⟨_⟩ _ (subtype.mk b h)⟩
+
+theorem add_one_le_succ (c : cardinal) : c + 1 ≤ succ c :=
+begin
+  refine quot.induction_on c (λ α, _) (lt_succ_self c),
+  refine quot.induction_on (succ (quot.mk setoid.r α)) (λ β h, _),
+  cases h.left with f,
+  have : ¬ surjective f := λ hn,
+    ne_of_lt h (quotient.sound ⟨equiv.of_bijective ⟨f.inj, hn⟩⟩),
+  cases classical.not_forall.1 this with b nex,
+  refine ⟨⟨sum.rec (by exact f) _, _⟩⟩,
+  { exact λ _, b },
+  { intros a b h, rcases a with a|⟨⟨⟨⟩⟩⟩; rcases b with b|⟨⟨⟨⟩⟩⟩,
+    { rw f.inj h },
+    { exact nex.elim ⟨_, h⟩ },
+    { exact nex.elim ⟨_, h.symm⟩ },
+    { refl } }
+end
+
 def sum {ι} (f : ι → cardinal) : cardinal := ⟦Σ i, (f i).out⟧
 
 theorem le_sum {ι} (f : ι → cardinal) (i) : f i ≤ sum f :=
@@ -479,4 +514,114 @@ theorem sup_le {ι} (f : ι → cardinal) (a) : sup f ≤ a ↔ ∀ i, f i ≤ a
 ⟨λ h i, le_trans (le_sup _ _) h,
  λ h, by dsimp [sup]; change a with (⟨a, h⟩:subtype _).1; apply min_le⟩
 
+def lift (c : cardinal.{u}) : cardinal.{max u v} :=
+quotient.lift_on c (λ α, ⟦ulift α⟧) $ λ α β ⟨e⟩,
+quotient.sound ⟨equiv.ulift.trans $ e.trans equiv.ulift.symm⟩
+
+theorem lift_mk (α) : lift.{u v} (mk α) = mk (ulift.{v u} α) := rfl
+
+theorem lift_umax : lift.{u (max u v)} = lift.{u v} :=
+funext $ λ a, quot.induction_on a $ λ α,
+quotient.sound ⟨equiv.ulift.trans equiv.ulift.symm⟩
+
+@[simp] theorem lift_id (a : cardinal) : lift a = a :=
+quot.induction_on a $ λ α, quot.sound ⟨equiv.ulift⟩
+
+@[simp] theorem lift_lift (a : cardinal) : lift.{(max u v) w} (lift.{u v} a) = lift.{u (max v w)} a :=
+quot.induction_on a $ λ α,
+quotient.sound ⟨equiv.ulift.trans $ equiv.ulift.trans equiv.ulift.symm⟩
+
+theorem lift_mk_le {α : Type u} {β : Type v} :
+  lift.{u (max v w)} (mk α) ≤ lift.{v (max u w)} (mk β) ↔ nonempty (embedding α β) :=
+⟨λ ⟨f⟩, ⟨embedding.congr equiv.ulift equiv.ulift f⟩,
+ λ ⟨f⟩, ⟨embedding.congr equiv.ulift.symm equiv.ulift.symm f⟩⟩
+
+theorem lift_mk_eq {α : Type u} {β : Type v} :
+  lift.{u (max v w)} (mk α) = lift.{v (max u w)} (mk β) ↔ nonempty (α ≃ β) :=
+quotient.eq.trans
+⟨λ ⟨f⟩, ⟨equiv.ulift.symm.trans $ f.trans equiv.ulift⟩,
+ λ ⟨f⟩, ⟨equiv.ulift.trans $ f.trans equiv.ulift.symm⟩⟩
+
+@[simp] theorem lift_le {a b : cardinal} : lift a ≤ lift b ↔ a ≤ b :=
+quotient.induction_on₂ a b $ λ α β, 
+by rw ← lift_umax; exact lift_mk_le
+
+@[simp] theorem lift_inj {a b : cardinal} : lift a = lift b ↔ a = b :=
+by simp [le_antisymm_iff]
+
+@[simp] theorem lift_lt {a b : cardinal} : lift a < lift b ↔ a < b :=
+by simp [lt_iff_le_not_le, -not_le]
+
+@[simp] theorem lift_zero : lift 0 = 0 :=
+quotient.sound ⟨equiv.ulift.trans $ equiv.ulift.trans equiv.ulift.symm⟩
+
+@[simp] theorem lift_one : lift 1 = 1 :=
+quotient.sound ⟨equiv.ulift.trans $ equiv.ulift.trans equiv.ulift.symm⟩
+
+@[simp] theorem lift_add (a b) : lift (a + b) = lift a + lift b :=
+quotient.induction_on₂ a b $ λ α β, 
+quotient.sound ⟨equiv.ulift.trans (equiv.sum_congr equiv.ulift equiv.ulift).symm⟩
+
+@[simp] theorem lift_mul (a b) : lift (a * b) = lift a * lift b :=
+quotient.induction_on₂ a b $ λ α β, 
+quotient.sound ⟨equiv.ulift.trans (equiv.prod_congr equiv.ulift equiv.ulift).symm⟩
+
+@[simp] theorem lift_power (a b) : lift (a ^ b) = lift a ^ lift b :=
+quotient.induction_on₂ a b $ λ α β, 
+quotient.sound ⟨equiv.ulift.trans (equiv.arrow_congr equiv.ulift equiv.ulift).symm⟩
+
+@[simp] theorem lift_min {ι} [inhabited ι] (f : ι → cardinal) : lift (min f) = min (lift ∘ f) :=
+le_antisymm (le_min.2 $ λ a, lift_le.2 $ min_le _ a) $
+let ⟨i, e⟩ := min_eq (lift ∘ f) in
+by rw e; exact lift_le.2 (le_min.2 $ λ j, lift_le.1 $
+by have := min_le (lift ∘ f) j; rwa e at this)
+
+def ω : cardinal.{u} := lift (mk ℕ)
+
+@[simp] theorem mk_fin : ∀ (n : ℕ), mk (fin n) = n
+| 0     := quotient.sound ⟨(equiv.empty_of_not_nonempty $
+  by exact λ ⟨h⟩, h.elim0).trans equiv.ulift.symm⟩
+| (n+1) := by rw [nat.cast_succ, ← mk_fin]; exact
+  quotient.sound (fintype.card_eq.1 $ by simp)
+
+@[simp] theorem lift_nat_cast (n : ℕ) : lift n = n :=
+by induction n; simp *
+
+theorem lift_mk_fin (n : ℕ) : lift (mk (fin n)) = n := by simp
+
+theorem fintype_card (α : Type u) [fintype α] : mk α = fintype.card α :=
+by rw [← lift_mk_fin.{u}, ← lift_id.{u u} (mk α), lift_mk_eq.{u 0 u}];
+   exact fintype.card_eq.1 (by simp)
+
+@[simp] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=
+by rw [← lift_mk_fin, ← lift_mk_fin, lift_le]; exact
+⟨λ ⟨⟨f, hf⟩⟩, begin
+  have : _ = fintype.card _ := finset.card_image_of_injective finset.univ hf,
+  simp at this,
+  rw [← fintype.card_fin n, ← this],
+  exact finset.card_le_of_subset (finset.subset_univ _)
+end,
+λ h, ⟨⟨λ i, ⟨i.1, lt_of_lt_of_le i.2 h⟩, λ a b h,
+  have _, from fin.veq_of_eq h, fin.eq_of_veq this⟩⟩⟩
+
+@[simp] theorem nat_cast_lt {m n : ℕ} : (m : cardinal) < n ↔ m < n :=
+by simp [lt_iff_le_not_le, -not_le]
+
+@[simp] theorem nat_cast_inj {m n : ℕ} : (m : cardinal) = n ↔ m = n :=
+by simp [le_antisymm_iff]
+
+@[simp] theorem nat_succ (n : ℕ) : succ n = n.succ :=
+le_antisymm (succ_le.2 $ nat_cast_lt.2 $ nat.lt_succ_self _) (add_one_le_succ _)
+
+theorem nat_lt_ω (n : ℕ) : (n : cardinal.{u}) < ω :=
+succ_le.1 $ by rw [nat_succ, ← lift_mk_fin, ω, lift_mk_le.{0 0 u}]; exact
+⟨⟨fin.val, λ a b, fin.eq_of_veq⟩⟩
+
+/-
+theorem lt_ω {c : cardinal} : c < ω ↔ ∃ n : ℕ, c = n :=
+⟨λ h, begin
+  cases le_mk_iff_exists_set.1 h.1 with S e, rw ← e,
+end, λ ⟨n, e⟩, e.symm ▸ nat_lt_ω _⟩
+-/
+
 end cardinal

data/finset.lean

@@ -641,6 +641,14 @@ 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_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]
+
+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_succ [decidable_eq α] {s : finset α} {a : α} {n : ℕ} :
   s.card = n + 1 ↔ (∃a t, a ∉ t ∧ insert a t = s ∧ card t = n) :=
 iff.intro
@@ -702,7 +710,7 @@ theorem bind_to_finset [decidable_eq α] (s : multiset α) (t : α → multiset
   (s.bind t).to_finset = s.to_finset.bind (λa, (t a).to_finset) :=
 ext.2 $ by simp
 
-lemma bind_mono  {t₁ t₂ : α → finset β} (h : ∀a∈s, t₁ a ⊆ t₂ a) : s.bind t₁ ⊆ s.bind t₂ :=
+lemma bind_mono {t₁ t₂ : α → finset β} (h : ∀a∈s, t₁ a ⊆ t₂ a) : s.bind t₁ ⊆ s.bind t₂ :=
 have ∀b a, a ∈ s → b ∈ t₁ a → (∃ (a : α), a ∈ s ∧ b ∈ t₂ a),
   from assume b a ha hb, ⟨a, ha, finset.mem_of_subset (h a ha) hb⟩,
 by simpa [finset.subset_iff]
@@ -725,6 +733,9 @@ theorem product_eq_bind [decidable_eq α] [decidable_eq β] (s : finset α) (t :
  s.product t = s.bind (λa, t.image $ λb, (a, b)) :=
 ext.2 $ by simp [and.left_comm]
 
+@[simp] theorem card_product (s : finset α) (t : finset β) : card (s.product t) = card s * card t :=
+multiset.card_product _ _
+
 end prod
 
 section sigma

data/fintype.lean

@@ -5,7 +5,7 @@ Author: Mario Carneiro
 
 Finite types.
 -/
-import data.finset data.equiv
+import data.finset data.equiv algebra.big_operators
 universes u v
 
 variables {α : Type*} {β : Type*} {γ : Type*}
@@ -19,12 +19,16 @@ variable [fintype α]
 
 def univ : finset α := fintype.elems α
 
-@[simp] theorem mem_univ [fintype α] (x : α) : x ∈ (univ : finset α) :=
+@[simp] theorem mem_univ (x : α) : x ∈ (univ : finset α) :=
 fintype.complete x
 
-@[simp] theorem mem_univ_val [fintype α] : ∀ x, x ∈ (univ : finset α).1 := mem_univ
+@[simp] theorem mem_univ_val : ∀ x, x ∈ (univ : finset α).1 := mem_univ
 
 theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
+
+theorem eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s :=
+by simp [ext]
+
 end finset
 
 open finset
@@ -71,7 +75,34 @@ def of_bijective [fintype α] (f : α → β) (H : function.bijective f) : finty
 def of_surjective [fintype α] [decidable_eq β] (f : α → β) (H : function.surjective f) : fintype β :=
 ⟨univ.image f, λ b, let ⟨a, e⟩ := H b in e ▸ mem_image_of_mem _ (mem_univ _)⟩
 
-def of_equiv (α : Type*) [fintype α] (f : α ≃ β) : fintype β := of_bijective _ f.bijective 
+def of_equiv (α : Type*) [fintype α] (f : α ≃ β) : fintype β := of_bijective _ f.bijective
+
+theorem of_equiv_card [fintype α] (f : α ≃ β) :
+  @card β (of_equiv α f) = card α :=
+multiset.card_map _ _
+
+theorem card_congr {α β} [fintype α] [fintype β] (f : α ≃ β) : card α = card β :=
+by rw ← of_equiv_card f; congr
+
+theorem card_eq {α β} [F : fintype α] [G : fintype β] : card α = card β ↔ nonempty (α ≃ β) :=
+⟨λ e, match F, G, e with ⟨⟨s, nd⟩, h⟩, ⟨⟨s', nd'⟩, h'⟩, e' := begin
+  change multiset.card s = multiset.card s' at e',
+  revert nd nd' h h' e',
+  refine quotient.induction_on₂ s s' (λ l₁ l₂
+    (nd₁ : l₁.nodup) (nd₂ : l₂.nodup)
+    (h₁ : ∀ x, x ∈ l₁) (h₂ : ∀ x, x ∈ l₂)
+    (e : l₁.length = l₂.length), _),
+  have := classical.dec_eq α,
+  refine ⟨equiv.of_bijective ⟨_, _⟩⟩,
+  { refine λ a, l₂.nth_le (l₁.index_of a) _,
+    rw ← e, exact list.index_of_lt_length.2 (h₁ a) },
+  { intros a b h, simpa [h₁] using congr_arg l₁.nth
+      (list.nodup_iff_nth_le_inj.1 nd₂ _ _ _ _ h) },
+  { have := classical.dec_eq β,
+    refine λ b, ⟨l₁.nth_le (l₂.index_of b) _, _⟩,
+    { rw e, exact list.index_of_lt_length.2 (h₂ b) },
+    { simp [nd₁] } }
+end end, λ ⟨f⟩, card_congr f⟩
 
 end fintype
 
@@ -80,29 +111,61 @@ instance (n : ℕ) : fintype (fin n) :=
   list.nodup_pmap (λ a _ b _, congr_arg fin.val) (list.nodup_range _)⟩,
 λ ⟨m, h⟩, list.mem_pmap.2 ⟨m, list.mem_range.2 h, rfl⟩⟩
 
+@[simp] theorem fintype.card_fin (n : ℕ) : fintype.card (fin n) = n :=
+by rw [fin.fintype]; simp [fintype.card, card, univ]
+
 instance : fintype empty := ⟨∅, empty.rec _⟩
 
+@[simp] theorem fintype.univ_empty : @univ empty _ = ∅ := rfl
+
+@[simp] theorem fintype.card_empty : fintype.card empty = 0 := rfl
+
 instance : fintype unit := ⟨⟨()::0, by simp⟩, λ ⟨⟩, by simp⟩
 
+@[simp] theorem fintype.univ_unit : @univ unit _ = {()} := rfl
+
+@[simp] theorem fintype.card_unit : fintype.card unit = 1 := rfl
+
 instance : fintype bool := ⟨⟨tt::ff::0, by simp⟩, λ x, by cases x; simp⟩
 
+@[simp] theorem fintype.univ_bool : @univ bool _ = {ff, tt} := rfl
+
+@[simp] theorem fintype.card_bool : fintype.card bool = 2 := rfl
+
 instance {α : Type*} (β : α → Type*)
   [fintype α] [∀ a, fintype (β a)] : fintype (sigma β) :=
 ⟨univ.sigma (λ _, univ), λ ⟨a, b⟩, by simp⟩
 
+@[simp] theorem fintype.card_sigma {α : Type*} (β : α → Type*)
+  [fintype α] [∀ a, fintype (β a)] :
+  fintype.card (sigma β) = univ.sum (λ a, fintype.card (β a)) :=
+card_sigma _ _
+
 instance (α β : Type*) [fintype α] [fintype β] : fintype (α × β) :=
 ⟨univ.product univ, λ ⟨a, b⟩, by simp⟩
 
+@[simp] theorem fintype.card_prod (α β : Type*) [fintype α] [fintype β] :
+  fintype.card (α × β) = fintype.card α * fintype.card β :=
+card_product _ _
+
 instance (α : Type*) [fintype α] : fintype (ulift α) :=
 fintype.of_equiv _ equiv.ulift.symm
 
+@[simp] theorem fintype.card_ulift (α : Type*) [fintype α] :
+  fintype.card (ulift α) = fintype.card α :=
+fintype.of_equiv_card _
+
 instance (α : Type u) (β : Type v) [fintype α] [fintype β] : fintype (α ⊕ β) :=
 @fintype.of_equiv _ _ (@sigma.fintype _
     (λ b, cond b (ulift α) (ulift.{(max u v) v} β)) _
     (λ b, by cases b; apply ulift.fintype))
   ((equiv.sum_equiv_sigma_bool _ _).symm.trans
     (equiv.sum_congr equiv.ulift equiv.ulift))
 
+@[simp] theorem fintype.card_sum (α β : Type*) [fintype α] [fintype β] :
+  fintype.card (α ⊕ β) = fintype.card α + fintype.card β :=
+by rw [sum.fintype, fintype.of_equiv_card]; simp
+
 instance list.subtype.fintype [decidable_eq α] (l : list α) : fintype {x // x ∈ l} :=
 fintype.of_list l.attach l.mem_attach