diff --git a/algebra/big_operators.lean b/algebra/big_operators.lean
index 54142921b6338..881df6eff0fe1 100644
--- a/algebra/big_operators.lean
+++ b/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
diff --git a/algebra/group_power.lean b/algebra/group_power.lean
index 5c0b2856f1267..296a19618604f 100644
--- a/algebra/group_power.lean
+++ b/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
diff --git a/algebra/module.lean b/algebra/module.lean
index 1cfe84bdd59f3..2208be2632fdc 100644
--- a/algebra/module.lean
+++ b/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
diff --git a/data/cardinal.lean b/data/cardinal.lean
index 3218c54eb867b..80a89d085ea5b 100644
--- a/data/cardinal.lean
+++ b/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
diff --git a/data/finset.lean b/data/finset.lean
index aa8f48f4e0b4f..8631c18362895 100644
--- a/data/finset.lean
+++ b/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
diff --git a/data/fintype.lean b/data/fintype.lean
index 6fe04f71d6461..ae4696d83650e 100644
--- a/data/fintype.lean
+++ b/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,22 +111,50 @@ 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} β)) _
@@ -103,6 +162,10 @@ instance (α : Type u) (β : Type v) [fintype α] [fintype β] : 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
 
diff --git a/data/list/basic.lean b/data/list/basic.lean
index 69e64636c10cf..b51bef56db23f 100644
--- a/data/list/basic.lean
+++ b/data/list/basic.lean
@@ -1049,6 +1049,10 @@ by have := mem_map.1 (by rw [attach_map_val]; exact h);
   {l H b} : b ∈ pmap f l H ↔ ∃ a (h : a ∈ l), f a (H a h) = b :=
 by simp [pmap_eq_map_attach]
 
+@[simp] theorem length_pmap {p : α → Prop} {f : Π a, p a → β}
+  {l H} : length (pmap f l H) = length l :=
+by induction l; simp *
+
 /- find -/
 
 section find
@@ -2410,6 +2414,10 @@ pairwise_iff_nth_le.trans
   .resolve_right (λ h', H _ _ h₁ h' h.symm),
  λ H i j h₁ h₂ h, ne_of_lt h₂ (H _ _ _ _ h)⟩
 
+@[simp] theorem nth_le_index_of [decidable_eq α] {l : list α} (H : nodup l) (n h) : index_of (nth_le l n h) l = n :=
+nodup_iff_nth_le_inj.1 H _ _ _ h $
+index_of_nth_le $ index_of_lt_length.2 $ nth_le_mem _ _ _
+
 theorem nodup_iff_count_le_one [decidable_eq α] {l : list α} : nodup l ↔ ∀ a, count a l ≤ 1 :=
 nodup_iff_sublist.trans $ forall_congr $ λ a,
 have [a, a] <+ l ↔ 1 < count a l, from (@le_count_iff_repeat_sublist _ _ a l 2).symm,
diff --git a/data/multiset.lean b/data/multiset.lean
index 210d4d15f053f..ebffd9475cec4 100644
--- a/data/multiset.lean
+++ b/data/multiset.lean
@@ -475,6 +475,9 @@ quotient.induction_on₂ s t $ λ l₁ l₂, congr_arg coe $ map_append _ _ _
   b ∈ map f s ↔ ∃ a, a ∈ s ∧ f a = b :=
 quot.induction_on s $ λ l, mem_map
 
+@[simp] theorem card_map (f : α → β) (s) : card (map f s) = card s :=
+quot.induction_on s $ λ l, length_map _ _
+
 theorem mem_map_of_mem (f : α → β) {a : α} {s : multiset α} (h : a ∈ s) : f a ∈ map f s :=
 mem_map.2 ⟨_, h, rfl⟩
 
@@ -596,6 +599,9 @@ sum_add _ _
 multiset.induction_on S (by simp) $
   by simp [or_and_distrib_right, exists_or_distrib] {contextual := tt}
 
+@[simp] theorem card_join (S) : card (@join α S) = sum (map card S) :=
+multiset.induction_on S (by simp) (by simp)
+
 /- bind -/
 def bind (s : multiset α) (f : α → multiset β) : multiset β :=
 join (map f s)
@@ -616,6 +622,9 @@ by simp [bind]
 by simp [bind]; simp [-exists_and_distrib_right, exists_and_distrib_right.symm];
    rw exists_swap; simp [and_assoc]
 
+@[simp] theorem card_bind (s) (f : α → multiset β) : card (bind s f) = sum (map (card ∘ f) s) :=
+by simp [bind]
+
 /- product -/
 def product (s : multiset α) (t : multiset β) : multiset (α × β) :=
 s.bind $ λ a, t.map $ prod.mk a
@@ -644,6 +653,9 @@ multiset.induction_on s (λ t u, rfl) $ λ a s IH t u,
 @[simp] theorem mem_product {s t} : ∀ {p : α × β}, p ∈ @product α β s t ↔ p.1 ∈ s ∧ p.2 ∈ t
 | (a, b) := by simp [product, and.left_comm]
 
+@[simp] theorem card_product (s : multiset α) (t : multiset β) : card (product s t) = card s * card t :=
+by simp [product, (∘), mul_comm]
+
 /- sigma -/
 section
 variable {σ : α → Type*}
@@ -677,6 +689,10 @@ multiset.induction_on s (λ t u, rfl) $ λ a s IH t u,
   p ∈ @multiset.sigma α σ s t ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
 | ⟨a, b⟩ := by simp [multiset.sigma, and_assoc, and.left_comm]
 
+@[simp] theorem card_sigma (s : multiset α) (t : Π a, multiset (σ a)) :
+  card (s.sigma t) = sum (map (λ a, card (t a)) s) :=
+by simp [multiset.sigma, (∘)]
+
 end
 
 /- map for partial functions -/
@@ -725,6 +741,10 @@ quot.induction_on s $ λ l, mem_attach _
   {s H b} : b ∈ pmap f s H ↔ ∃ a (h : a ∈ s), f a (H a h) = b :=
 quot.induction_on s (λ l H, mem_pmap) H
 
+@[simp] theorem card_pmap {p : α → Prop} (f : Π a, p a → β)
+  (s H) : card (pmap f s H) = card s :=
+quot.induction_on s (λ l H, length_pmap) H
+
 /- subtraction -/
 section
 variables [decidable_eq α] {s t u : multiset α} {a b : α}
diff --git a/data/ordinal.lean b/data/ordinal.lean
index 46bbb3c1d3246..b3bfa7789daf4 100644
--- a/data/ordinal.lean
+++ b/data/ordinal.lean
@@ -37,6 +37,9 @@ def is_trichotomous.swap (r) [is_trichotomous α r] : is_trichotomous α (swap r
 def is_strict_total_order'.swap (r) [is_strict_total_order' α r] : is_strict_total_order' α (swap r) :=
 ⟨is_trichotomous.swap r, is_strict_order.swap r⟩
 
+instance [linear_order α] : is_strict_total_order' α (<) :=
+⟨⟨lt_trichotomy⟩, ⟨lt_irrefl⟩, ⟨@lt_trans _ _⟩⟩
+
 @[algebra] class is_order_connected (α : Type u) (lt : α → α → Prop) : Prop :=
 (conn : ∀ a b c, lt a c → lt a b ∨ lt b c)
 
@@ -74,6 +77,9 @@ def empty_relation.is_well_order [subsingleton α] : is_well_order α empty_rela
   ⟨λ a, id⟩, ⟨λ a b c, false.elim⟩⟩,
   ⟨λ a, ⟨_, λ y, false.elim⟩⟩⟩
 
+instance nat.lt.is_well_order : is_well_order ℕ (<) :=
+⟨by apply_instance, nat.lt_wf⟩
+
 instance sum.lex.is_well_order [is_well_order α r] [is_well_order β s] : is_well_order (α ⊕ β) (sum.lex r s) :=
 ⟨⟨⟨λ a b, by cases a; cases b; simp; apply trichotomous⟩,
   ⟨λ a, by cases a; simp; apply irrefl⟩,
@@ -280,11 +286,12 @@ theorem eq_of_to_fun_eq : ∀ {e₁ e₂ : r ≃o s}, (e₁ : α → β) = e₂
 @[refl] protected def refl (r : α → α → Prop) : r ≃o r :=
 ⟨equiv.refl _, λ a b, iff.rfl⟩
 
-@[symm] protected def symm : r ≃o s → s ≃o r
-| ⟨f, o⟩ := ⟨f.symm, λ a b, by rw o; simp⟩
+@[symm] protected def symm (f : r ≃o s) : s ≃o r :=
+⟨f.to_equiv.symm, λ a b, by cases f with f o; rw o; simp⟩
 
-@[trans] protected def trans : r ≃o s → s ≃o t → r ≃o t
-| ⟨f₁, o₁⟩ ⟨f₂, o₂⟩ := ⟨f₁.trans f₂, λ a b, by rw [o₁, o₂]; simp⟩
+@[trans] protected def trans (f₁ : r ≃o s) (f₂ : s ≃o t) : r ≃o t :=
+⟨f₁.to_equiv.trans f₂.to_equiv, λ a b,
+  by cases f₁ with f₁ o₁; cases f₂ with f₂ o₂; rw [o₁, o₂]; simp⟩
 
 @[simp] theorem coe_fn_symm_mk (f o) : ((@order_iso.mk _ _ r s f o).symm : β → α) = f.symm :=
 rfl
@@ -305,9 +312,35 @@ def preimage (f : α ≃ β) (s : β → β → Prop) : f ⁻¹'o s ≃o s := 
 def of_surjective (f : r ≼o s) (H : surjective f) : r ≃o s :=
 ⟨equiv.of_bijective ⟨f.inj, H⟩, by simp [f.ord']⟩
 
-@[simp] theorem of_surjective_apply (f : r ≼o s) (H) (a : α) : of_surjective f H a = f a :=
+@[simp] theorem of_surjective_coe (f : r ≼o s) (H) : (of_surjective f H : α → β) = f :=
 by delta of_surjective; simp
 
+theorem sum_lex_congr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂}
+  (e₁ : @order_iso α₁ α₂ r₁ r₂) (e₂ : @order_iso β₁ β₂ s₁ s₂) :
+  sum.lex r₁ s₁ ≃o sum.lex r₂ s₂ :=
+⟨equiv.sum_congr e₁.to_equiv e₂.to_equiv, λ a b,
+ by cases e₁ with f hf; cases e₂ with g hg;
+    cases a; cases b; simp [hf, hg]⟩
+
+theorem prod_lex_congr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂}
+  (e₁ : @order_iso α₁ α₂ r₁ r₂) (e₂ : @order_iso β₁ β₂ s₁ s₂) :
+  prod.lex r₁ s₁ ≃o prod.lex r₂ s₂ :=
+⟨equiv.prod_congr e₁.to_equiv e₂.to_equiv,  λ a b, begin
+  cases e₁ with f hf; cases e₂ with g hg,
+  cases a with a₁ a₂; cases b with b₁ b₂,
+  suffices : prod.lex r₁ s₁ (a₁, a₂) (b₁, b₂) ↔
+    prod.lex r₂ s₂ (f a₁, g a₂) (f b₁, g b₂), {simpa [hf, hg]},
+  split,
+  { intro h, cases h with _ _ _ _ h _ _ _ h,
+    { left, exact hf.1 h },
+    { right, exact hg.1 h } },
+  { generalize e : f b₁ = fb₁,
+    intro h, cases h with _ _ _ _ h _ _ _ h,
+    { subst e, left, exact hf.2 h },
+    { have := f.bijective.1 e, subst b₁,
+      right, exact hg.2 h } }  
+end⟩
+
 end order_iso
 
 def set_coe_embedding {α : Type*} (p : set α) :
@@ -941,6 +974,9 @@ def card (o : ordinal) : cardinal :=
 quot.lift_on o (λ ⟨α, r, _⟩, ⟦α⟧) $
 λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨e⟩, quotient.sound ⟨e.to_equiv⟩
 
+@[simp] theorem card_type (r : α → α → Prop) [is_well_order α r] :
+  card (type r) = mk α := rfl
+
 theorem card_le_card {o₁ o₂ : ordinal} : o₁ ≤ o₂ → card o₁ ≤ card o₂ :=
 induction_on o₁ $ λ α r _, induction_on o₂ $ λ β s _ ⟨⟨⟨f, _⟩, _⟩⟩, ⟨f⟩
 
@@ -963,15 +999,38 @@ instance : has_add ordinal.{u} :=
 ⟨λo₁ o₂, quotient.lift_on₂ o₁ o₂
   (λ ⟨α, r, wo⟩ ⟨β, s, wo'⟩, ⟦⟨α ⊕ β, sum.lex r s, by exact sum.lex.is_well_order⟩⟧
     : Well_order → Well_order → ordinal) $
-λ ⟨α₁, r₁, o₁⟩ ⟨α₂, r₂, o₂⟩ ⟨β₁, s₁, p₁⟩ ⟨β₂, s₂, p₂⟩ ⟨⟨f, hf⟩⟩ ⟨⟨g, hg⟩⟩,
-quot.sound ⟨⟨equiv.sum_congr f g, λ a b,
-  by cases a; cases b; simp [hf, hg]⟩⟩⟩
+λ ⟨α₁, r₁, o₁⟩ ⟨α₂, r₂, o₂⟩ ⟨β₁, s₁, p₁⟩ ⟨β₂, s₂, p₂⟩ ⟨f⟩ ⟨g⟩,
+quot.sound ⟨order_iso.sum_lex_congr f g⟩⟩
 
 def succ (o : ordinal) : ordinal := o + 1
 
+theorem lt_succ_self (o : ordinal.{u}) : o < succ o :=
+induction_on o $ λ α r _,
+⟨begin
+  have := @empty_relation.is_well_order (ulift.{u 0} unit) _,
+  cases e : initial_seg.lt_or_eq
+    (@initial_seg.le_add α (ulift.{u 0} unit) r empty_relation) with f f,
+  { exact f },
+  { have := (initial_seg.of_iso f).eq (initial_seg.le_add _ _) (f.symm (sum.inr ⟨()⟩)),
+    simp at this, injection this }
+end⟩
+
+/-
+set_option pp.universes true
+theorem succ_le {a b : ordinal} : succ a ≤ b ↔ a < b :=
+⟨lt_of_lt_of_le (lt_succ_self _),
+induction_on a $ λ α r _, induction_on b $ λ β s _ ⟨⟨f, t, hf⟩⟩, begin
+  have := @empty_relation.is_well_order (ulift.{u 0} unit) _,
+  refine ⟨⟨order_embedding.of_monotone _ _, _⟩⟩
+end⟩
+-/
+
 @[simp] theorem card_add (o₁ o₂ : ordinal) : card (o₁ + o₂) = card o₁ + card o₂ :=
 induction_on o₁ $ λ α r _, induction_on o₂ $ λ β s _, rfl
 
+@[simp] theorem card_nat (n : ℕ) : card.{u} n = n :=
+by induction n; simp *
+
 instance : add_monoid ordinal.{u} :=
 { add       := (+),
   zero      := 0,
@@ -1028,30 +1087,97 @@ instance : has_mul ordinal.{u} :=
 ⟨λo₁ o₂, quotient.lift_on₂ o₁ o₂
   (λ ⟨α, r, wo⟩ ⟨β, s, wo'⟩, ⟦⟨α × β, prod.lex r s, by exact prod.lex.is_well_order⟩⟧
     : Well_order → Well_order → ordinal) $
-λ ⟨α₁, r₁, o₁⟩ ⟨α₂, r₂, o₂⟩ ⟨β₁, s₁, p₁⟩ ⟨β₂, s₂, p₂⟩ ⟨⟨f, hf⟩⟩ ⟨⟨g, hg⟩⟩,
-quot.sound ⟨⟨equiv.prod_congr f g, λ a b, begin
-  cases a with a₁ a₂; cases b with b₁ b₂,
-  suffices : prod.lex r₁ r₂ (a₁, a₂) (b₁, b₂) ↔
-    prod.lex s₁ s₂ (f a₁, g a₂) (f b₁, g b₂), {simpa [hf, hg]},
-  split,
-  { intro h, cases h with _ _ _ _ h _ _ _ h,
-    { left, exact hf.1 h },
-    { right, exact hg.1 h } },
-  { generalize e : f b₁ = fb₁,
-    intro h, cases h with _ _ _ _ h _ _ _ h,
-    { subst e, left, exact hf.2 h },
-    { have := f.bijective.1 e, subst b₁,
-      right, exact hg.2 h } }  
-end⟩⟩⟩
-
-theorem type_le_of_order_embedding {α β} {r : α → α → Prop} {s : β → β → Prop}
-  [is_well_order α r] [is_well_order β s] (f : r ≼o s) : type r ≤ type s :=
-⟨f.collapse⟩
+λ ⟨α₁, r₁, o₁⟩ ⟨α₂, r₂, o₂⟩ ⟨β₁, s₁, p₁⟩ ⟨β₂, s₂, p₂⟩ ⟨f⟩ ⟨g⟩,
+quot.sound ⟨order_iso.prod_lex_congr f g⟩⟩
+
+def lift (o : ordinal.{u}) : ordinal.{max u v} :=
+quotient.lift_on o (λ ⟨α, r, wo⟩,
+  @type _ _ (@order_embedding.is_well_order _ _ (@equiv.ulift.{u v} α ⁻¹'o r) r
+    (order_iso.preimage equiv.ulift.{u v} r) wo)) $
+λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨f⟩,
+quot.sound ⟨(order_iso.preimage equiv.ulift r).trans $
+  f.trans (order_iso.preimage equiv.ulift s).symm⟩
+
+def ω : ordinal.{u} := lift $ @type ℕ (<) _
+
+theorem lift_umax : lift.{u (max u v)} = lift.{u v} :=
+funext $ λ a, induction_on a $ λ α r _,
+quotient.sound ⟨(order_iso.preimage equiv.ulift r).trans (order_iso.preimage equiv.ulift r).symm⟩
+
+@[simp] theorem lift_id (a : ordinal) : lift a = a :=
+induction_on a $ λ α r _,
+quotient.sound ⟨order_iso.preimage equiv.ulift r⟩
+
+@[simp] theorem lift_lift (a : ordinal) : lift.{(max u v) w} (lift.{u v} a) = lift.{u (max v w)} a :=
+induction_on a $ λ α r _,
+quotient.sound ⟨(order_iso.preimage equiv.ulift _).trans $
+  (order_iso.preimage equiv.ulift _).trans (order_iso.preimage equiv.ulift _).symm⟩
+
+theorem lift_type_le {α : Type u} {β : Type v} {r s} [is_well_order α r] [is_well_order β s] :
+  lift.{u (max v w)} (type r) ≤ lift.{v (max u w)} (type s) ↔ nonempty (r ≼i s) :=
+⟨λ ⟨f⟩, ⟨(initial_seg.of_iso (order_iso.preimage equiv.ulift r).symm).trans $
+    f.trans (initial_seg.of_iso (order_iso.preimage equiv.ulift s))⟩,
+ λ ⟨f⟩, ⟨(initial_seg.of_iso (order_iso.preimage equiv.ulift r)).trans $
+    f.trans (initial_seg.of_iso (order_iso.preimage equiv.ulift s).symm)⟩⟩
+
+theorem lift_type_eq {α : Type u} {β : Type v} {r s} [is_well_order α r] [is_well_order β s] :
+  lift.{u (max v w)} (type r) = lift.{v (max u w)} (type s) ↔ nonempty (r ≃o s) :=
+quotient.eq.trans
+⟨λ ⟨f⟩, ⟨(order_iso.preimage equiv.ulift r).symm.trans $
+    f.trans (order_iso.preimage equiv.ulift s)⟩,
+ λ ⟨f⟩, ⟨(order_iso.preimage equiv.ulift r).trans $
+    f.trans (order_iso.preimage equiv.ulift s).symm⟩⟩
+
+theorem lift_type_lt {α : Type u} {β : Type v} {r s} [is_well_order α r] [is_well_order β s] :
+  lift.{u (max v w)} (type r) < lift.{v (max u w)} (type s) ↔ nonempty (r ≺i s) :=
+by have := @order_embedding.is_well_order _ _ (@equiv.ulift.{u (max v w)} α ⁻¹'o r)
+     r (order_iso.preimage equiv.ulift.{u (max v w)} r) _;
+   have := @order_embedding.is_well_order _ _ (@equiv.ulift.{v (max u w)} β ⁻¹'o s)
+     s (order_iso.preimage equiv.ulift.{v (max u w)} s) _; exact
+⟨λ ⟨f⟩, ⟨(f.equiv_lt (order_iso.preimage equiv.ulift r).symm).lt_le
+    (initial_seg.of_iso (order_iso.preimage equiv.ulift s))⟩,
+ λ ⟨f⟩, ⟨(f.equiv_lt (order_iso.preimage equiv.ulift r)).lt_le
+    (initial_seg.of_iso (order_iso.preimage equiv.ulift s).symm)⟩⟩
+
+@[simp] theorem lift_le {a b : ordinal} : lift.{u v} a ≤ lift b ↔ a ≤ b :=
+induction_on a $ λ α r _, induction_on b $ λ β s _,
+by rw ← lift_umax; exact lift_type_le
+
+@[simp] theorem lift_inj {a b : ordinal} : lift a = lift b ↔ a = b :=
+by simp [le_antisymm_iff]
+
+@[simp] theorem lift_lt {a b : ordinal} : lift a < lift b ↔ a < b :=
+by simp [lt_iff_le_not_le, -not_le]
+
+@[simp] theorem lift_zero : lift 0 = 0 :=
+quotient.sound ⟨(order_iso.preimage equiv.ulift _).trans
+ ⟨equiv.ulift.trans equiv.ulift.symm, λ a b, iff.rfl⟩⟩
+
+@[simp] theorem lift_one : lift 1 = 1 :=
+quotient.sound ⟨(order_iso.preimage equiv.ulift _).trans
+ ⟨equiv.ulift.trans equiv.ulift.symm, λ a b, iff.rfl⟩⟩
+
+@[simp] theorem lift_add (a b) : lift (a + b) = lift a + lift b :=
+quotient.induction_on₂ a b $ λ ⟨α, r, _⟩ ⟨β, s, _⟩, 
+quotient.sound ⟨(order_iso.preimage equiv.ulift _).trans
+ (order_iso.sum_lex_congr (order_iso.preimage equiv.ulift _)
+   (order_iso.preimage equiv.ulift _)).symm⟩
+
+@[simp] theorem lift_mul (a b) : lift (a * b) = lift a * lift b :=
+quotient.induction_on₂ a b $ λ ⟨α, r, _⟩ ⟨β, s, _⟩, 
+quotient.sound ⟨(order_iso.preimage equiv.ulift _).trans
+ (order_iso.prod_lex_congr (order_iso.preimage equiv.ulift _)
+   (order_iso.preimage equiv.ulift _)).symm⟩
+
+@[simp] theorem lift_ω : lift ω = ω := lift_lift _
+
+theorem type_le' {α β} {r : α → α → Prop} {s : β → β → Prop}
+  [is_well_order α r] [is_well_order β s] : type r ≤ type s ↔ nonempty (r ≼o s) :=
+⟨λ ⟨f⟩, ⟨f⟩, λ ⟨f⟩, ⟨f.collapse⟩⟩
 
 theorem le_add_left (o₁ o₂ : ordinal) : o₁ ≤ o₂ + o₁ :=
 induction_on o₁ $ λ α₁ r₁ _, induction_on o₂ $ λ α₂ r₂ _,
-by exact type_le_of_order_embedding
-⟨⟨sum.inr, λ _ _, sum.inr.inj⟩, λ a b, by simp⟩
+by exact type_le'.2 ⟨⟨⟨sum.inr, λ _ _, sum.inr.inj⟩, λ a b, by simp⟩⟩
 
 theorem le_total (o₁ o₂ : ordinal) : o₁ ≤ o₂ ∨ o₂ ≤ o₁ :=
 match lt_or_eq_of_le (le_add_left o₂ o₁), lt_or_eq_of_le (le_add_right o₁ o₂) with
@@ -1068,8 +1194,17 @@ end
 instance : linear_order ordinal :=
 { le_total := le_total, ..ordinal.partial_order }
 
-instance : is_well_order ordinal (<) :=
-⟨⟨⟨lt_trichotomy⟩, ⟨lt_irrefl⟩, ⟨@lt_trans _ _⟩⟩, wf⟩
+instance : is_well_order ordinal (<) := ⟨by apply_instance, wf⟩
+
+def typein.principal_seg {α : Type u} (r : α → α → Prop) [is_well_order α r] :
+  @principal_seg α ordinal.{u} r (<) :=
+⟨order_embedding.of_monotone (typein r)
+  (λ a b, (typein_lt_typein r).2), type r, λ b,
+    ⟨λ h, ⟨enum r _ h, typein_enum r h⟩,
+    λ ⟨a, e⟩, e ▸ typein_lt_type _ _⟩⟩
+
+@[simp] theorem typein.principal_seg_coe (r : α → α → Prop) [is_well_order α r] :
+  (typein.principal_seg r : α → ordinal) = typein r := rfl
 
 def min {ι} [inhabited ι] (f : ι → ordinal) : ordinal :=
 wf.min (set.range f) (set.ne_empty_of_mem (set.mem_range_self (default _)))
@@ -1084,7 +1219,79 @@ theorem le_min {ι} [inhabited ι] {f : ι → ordinal} {a} : a ≤ min f ↔ 
 ⟨λ h i, le_trans h (min_le _ _),
  λ h, let ⟨i, e⟩ := min_eq f in e.symm ▸ h i⟩
 
+@[simp] theorem lift_min {ι} [inhabited ι] (f : ι → ordinal) : 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)
+
+theorem lift_down {a : ordinal.{u}} {b : ordinal.{max u v}} :
+  b ≤ lift a → ∃ a', lift a' = b :=
+induction_on a $ λ α r _, induction_on b $ λ β s _,
+by rw [← lift_id (type s), ← lift_umax, ← lift_umax.{u v}, lift_type_le]; exact
+λ ⟨f⟩, ⟨type (subrel r (set.range f)), eq.symm $ lift_type_eq.2
+  ⟨order_iso.of_surjective
+    (order_embedding.cod_restrict _ f set.mem_range_self)
+    $ λ ⟨a, ⟨b, e⟩⟩, ⟨b, subtype.eq e⟩⟩⟩
+
+def lift.initial_seg : @initial_seg ordinal.{u} ordinal.{max u v} (<) (<) :=
+⟨⟨⟨lift.{u v}, λ a b, lift_inj.1⟩, λ a b, lift_lt.symm⟩,
+  λ a b h, lift_down (le_of_lt h)⟩
+
+@[simp] theorem lift.initial_seg_coe : (lift.initial_seg : ordinal → ordinal) = lift := rfl
+
+def lift.principal_seg : @principal_seg ordinal.{u} ordinal.{max (u+1) v} (<) (<) :=
+⟨↑lift.initial_seg.{u (max (u+1) v)}, lift.{(u+1) v} (@type ordinal.{u} (<) _), begin
+  refine λ b, induction_on b _, intros β s _,
+  rw ← lift_umax, split; intro h,
+  { rw ← lift_id.{(max (u+1) v) (max (u+1) v)} (type s) at h ⊢,
+    cases lift_type_lt.1 h with f, cases f with f a hf,
+    existsi a, revert hf,
+    apply induction_on a, intros α r _ hf,
+    refine lift_type_eq.{u (max (u+1) v) (max (u+1) v)}.2
+      ⟨(order_iso.of_surjective (order_embedding.of_monotone _ _) _).symm⟩,
+    { exact λ b, enum r (f b) ((hf _).2 ⟨_, rfl⟩) },
+    { refine λ a b h, (typein_lt_typein r).1 _,
+      rw [typein_enum, typein_enum],
+      exact f.ord'.1 h },
+    { intro a', cases (hf _).1 (typein_lt_type _ a') with b e,
+      existsi b, simp, simp [e] } },
+  { cases h with a e, rw [← e],
+    apply induction_on a, intros α r _,
+    exact lift_type_lt.{u (u+1) (max (u+1) v)}.2
+      ⟨typein.principal_seg r⟩ }
+end⟩
+
+@[simp] theorem lift.principal_seg_coe :
+  (lift.principal_seg.{u v} : ordinal → ordinal) = lift.{u (max (u+1) v)} := rfl
+
+@[simp] theorem lift.principal_seg_top :
+  lift.principal_seg.{u v}.top = lift.{(u+1) v} (@type ordinal.{u} (<) _) := rfl
+
+theorem lift.principal_seg_top' :
+  lift.principal_seg.{u (u+1)}.top = @type ordinal.{u} (<) _ :=
+by simp [lift_id.{(u+1) (u+1)}]
+
+end ordinal
+
+def order.cof (r : α → α → Prop) [is_refl α r] : cardinal :=
+@cardinal.min {S : set α // ∀ a, ∃ b ∈ S, r a b}
+  ⟨⟨set.univ, λ a, ⟨a, ⟨⟩, refl _⟩⟩⟩
+  (λ S, mk S)
+
 /-
+theorem order_iso.cof.aux {α : Type u} {β : Type v} {r s}
+  [is_refl α r] [is_refl β s] (f : r ≃o s) :
+  cardinal.lift.{u (max u v)} (order.cof r) ≤
+  cardinal.lift.{v (max u v)} (order.cof s) :=
+_
+
+theorem order_iso.cof {α : Type u} {β : Type v} {r s}
+  [is_refl α r] [is_refl β s] (f : r ≃o s) :
+  cardinal.lift.{u (max u v)} (order.cof r) =
+  cardinal.lift.{v (max u v)} (order.cof s) :=
+le_antisymm (order_iso.cof.aux f) (order_iso.cof.aux f.symm)
+
 def cof (o : ordinal) : cardinal :=
 let f : Well_order → cardinal := λ ⟨α, r, _⟩,
   @cardinal.min {S : set α // ∀ a, ∃ b ∈ S, ¬ r b a}
@@ -1097,8 +1304,6 @@ suffices ∀ {a b : Well_order}, a ≈ b → f a ≤ f b, from
 _
 -/
 
-end ordinal
-
 namespace cardinal
 
 def ord (c : cardinal) : ordinal :=
@@ -1118,34 +1323,134 @@ begin
   exact ordinal.min_le (λ i:ι α, ⟦⟨α, i.1, i.2⟩⟧) ⟨_, _⟩
 end
 
-instance : has_coe cardinal ordinal := ⟨ord⟩
-
-theorem ord_eq_min (α : Type u) : (mk α : ordinal.{u}) =
+theorem ord_eq_min (α : Type u) : ord (mk α) =
   @ordinal.min _ ⟨classical.indefinite_description _ well_ordering_thm⟩
     (λ i:{r // is_well_order α r}, ⟦⟨α, i.1, i.2⟩⟧) := rfl
 
 theorem ord_eq (α) : ∃ (r : α → α → Prop) [wo : is_well_order α r],
-  @ordinal.type α r wo = mk α :=
+  ord (mk α) = @ordinal.type α r wo :=
 let ⟨⟨r, wo⟩, h⟩ := @ordinal.min_eq _
   ⟨classical.indefinite_description _ well_ordering_thm⟩
   (λ i:{r // is_well_order α r}, ⟦⟨α, i.1, i.2⟩⟧) in
-⟨r, wo, h.symm⟩
+⟨r, wo, h⟩
 
-theorem ord_le {α : Type u} (r : α → α → Prop) [is_well_order α r] : (mk α : ordinal.{u}) ≤ ordinal.type r :=
+theorem ord_le_type (r : α → α → Prop) [is_well_order α r] : ord (mk α) ≤ ordinal.type r :=
 @ordinal.min_le _
   ⟨classical.indefinite_description _ well_ordering_thm⟩
   (λ i:{r // is_well_order α r}, ⟦⟨α, i.1, i.2⟩⟧) ⟨r, _⟩
 
-@[simp] theorem ord_le_ord {c₁ c₂ : cardinal.{u}} : (c₁ : ordinal.{u}) ≤ c₂ ↔ c₁ ≤ c₂ :=
-quotient.induction_on₂ c₁ c₂ $ λ α β,
-let ⟨r, _, e⟩ := ord_eq α, ⟨s, _, e'⟩ := ord_eq β in by exact
-⟨λ h, let ⟨f⟩ := show ordinal.type r ≤ ordinal.type s, from
-    e.symm ▸ e'.symm ▸ h in ⟨f.to_embedding⟩,
-λ ⟨f⟩, show (mk α : ordinal.{u}) ≤ mk β, begin
-  rw ← e',
-  have g := order_embedding.preimage f s,
-  have := order_embedding.is_well_order g,
-  exact le_trans (ord_le _) (ordinal.type_le_of_order_embedding g)
-end⟩
+theorem ord_le {c o} : ord c ≤ o ↔ c ≤ o.card :=
+quotient.induction_on c $ λ α, ordinal.induction_on o $ λ β s _,
+let ⟨r, _, e⟩ := ord_eq α in begin
+  simp, split; intro h,
+  { rw e at h, exact let ⟨f⟩ := h in ⟨f.to_embedding⟩ },
+  { cases h with f,
+    have g := order_embedding.preimage f s,
+    have := order_embedding.is_well_order g,
+    exact le_trans (ord_le_type _) (ordinal.type_le'.2 ⟨g⟩) }
+end
+
+theorem lt_ord {c o} : o < ord c ↔ o.card < c :=
+by rw [← not_le, ← not_le, ord_le]
+
+@[simp] theorem card_ord (c : cardinal) : (ord c).card = c :=
+quotient.induction_on c $ λ α,
+let ⟨r, _, e⟩ := ord_eq α in by simp [e]
+
+@[simp] theorem ord_le_ord {c₁ c₂ : cardinal.{u}} : ord c₁ ≤ ord c₂ ↔ c₁ ≤ c₂ :=
+by simp [ord_le]
+
+@[simp] theorem ord_lt_ord {c₁ c₂ : cardinal.{u}} : ord c₁ < ord c₂ ↔ c₁ < c₂ :=
+by simp [lt_ord]
+
+@[simp] theorem ord_zero : ord 0 = 0 :=
+le_antisymm (ord_le.2 $ cardinal.zero_le _) (ordinal.zero_le _)
+
+/-
+@[simp] theorem ord_nat (n : ℕ) : ord.{u} n = n :=
+le_antisymm (ord_le.2 $ by simp) $
+begin
+  rcases ord_eq _ with ⟨r, _, e⟩,
+  rw [← lift_mk_fin, lift_mk, e],
+end
+-/
+
+def ord.order_embedding : @order_embedding cardinal ordinal (<) (<) :=
+order_embedding.of_monotone cardinal.ord $ λ a b, cardinal.ord_lt_ord.2
+
+@[simp] theorem ord.order_embedding_coe :
+  (ord.order_embedding : cardinal → ordinal) = ord := rfl
+
+def aleph_idx.initial_seg : @initial_seg cardinal ordinal (<) (<) :=
+@order_embedding.collapse cardinal ordinal (<) (<) _ cardinal.ord.order_embedding
+
+def aleph_idx : cardinal → ordinal := aleph_idx.initial_seg
 
-end cardinal
\ No newline at end of file
+@[simp] theorem aleph_idx.initial_seg_coe :
+  (aleph_idx.initial_seg : cardinal → ordinal) = aleph_idx := rfl
+
+@[simp] theorem aleph_idx_lt {a b} : aleph_idx a < aleph_idx b ↔ a < b :=
+aleph_idx.initial_seg.to_order_embedding.ord'.symm
+
+@[simp] theorem aleph_idx_le {a b} : aleph_idx a ≤ aleph_idx b ↔ a ≤ b :=
+by rw [← not_lt, ← not_lt, aleph_idx_lt]
+
+theorem aleph_idx.init {a b} : b < aleph_idx a → ∃ c, aleph_idx c = b :=
+aleph_idx.initial_seg.init _ _
+
+def aleph_idx.order_iso : @order_iso cardinal.{u} ordinal.{u} (<) (<) :=
+@order_iso.of_surjective cardinal.{u} ordinal.{u} (<) (<) aleph_idx.initial_seg.{u} $
+(initial_seg.eq_or_principal aleph_idx.initial_seg.{u}).resolve_right $
+λ ⟨o, e⟩, begin
+  have : ∀ c, aleph_idx c < o := λ c, (e _).2 ⟨_, rfl⟩,
+  refine ordinal.induction_on o _ this, intros α r _ h,
+  let s := sup.{u u} (λ a:α, inv_fun aleph_idx (ordinal.typein r a)),
+  apply not_le_of_gt (lt_succ_self s),
+  have I : injective aleph_idx := aleph_idx.initial_seg.to_embedding.inj,
+  simpa [left_inverse_inv_fun I (succ s)] using
+    le_sup.{u u} (λ a, inv_fun aleph_idx (ordinal.typein r a))
+      (ordinal.enum r _ (h (succ s))),
+end
+
+@[simp] theorem aleph_idx.order_iso_coe :
+  (aleph_idx.order_iso : cardinal → ordinal) = aleph_idx :=
+by delta aleph_idx.order_iso; simp
+
+end cardinal
+
+namespace ordinal
+
+theorem ord_card_le (o : ordinal) : (card o).ord ≤ o :=
+cardinal.ord_le.2 (le_refl _)
+
+def aleph'.order_iso := cardinal.aleph_idx.order_iso.symm
+
+def aleph' : ordinal → cardinal := aleph'.order_iso
+
+@[simp] theorem aleph'.order_iso_coe :
+  (aleph'.order_iso : ordinal → cardinal) = aleph' := rfl
+
+@[simp] theorem aleph'_lt {o₁ o₂ : ordinal.{u}} : aleph' o₁ < aleph' o₂ ↔ o₁ < o₂ :=
+aleph'.order_iso.ord'.symm
+
+@[simp] theorem aleph'_le {o₁ o₂ : ordinal.{u}} : aleph' o₁ ≤ aleph' o₂ ↔ o₁ ≤ o₂ :=
+by rw [← not_lt, ← not_lt, aleph'_lt]
+
+@[simp] theorem aleph'_aleph_idx (c : cardinal.{u}) : aleph' c.aleph_idx = c :=
+by simpa using cardinal.aleph_idx.order_iso.to_equiv.inverse_apply_apply c
+
+@[simp] theorem aleph_idx_aleph' (o : ordinal.{u}) : o.aleph'.aleph_idx = o :=
+by simpa using cardinal.aleph_idx.order_iso.to_equiv.apply_inverse_apply o
+
+/-
+@[simp] theorem aleph'_succ {o : ordinal.{u}} : aleph' (succ o) = (aleph' o).succ :=
+le_antisymm
+ (cardinal.aleph_idx_le.1 $ begin
+    rw [aleph_idx_aleph', succ_le]
+  end)
+ (succ_le.2 $ aleph'_lt.2 $ ordinal.lt_succ_self _)
+-/
+
+def aleph (o : ordinal) : cardinal := aleph' (ω + o)
+
+end ordinal