diff --git a/archive/100-theorems-list/16_abel_ruffini.lean b/archive/100-theorems-list/16_abel_ruffini.lean
index e525d87a7e1eb..37460d82ee589 100644
--- a/archive/100-theorems-list/16_abel_ruffini.lean
+++ b/archive/100-theorems-list/16_abel_ruffini.lean
@@ -158,7 +158,7 @@ begin
   introI h,
   refine equiv.perm.not_solvable _ (le_of_eq _)
     (solvable_of_surjective (gal_Phi a b hab h_irred).2),
-  rw_mod_cast [cardinal.fintype_card, complex_roots_Phi a b h_irred.separable],
+  rw_mod_cast [cardinal.mk_fintype, complex_roots_Phi a b h_irred.separable],
 end
 
 theorem not_solvable_by_rad' (x : ℂ) (hx : aeval x (Φ ℚ 4 2) = 0) :
diff --git a/archive/sensitivity.lean b/archive/sensitivity.lean
index 5e9393bd2eaa8..15341f03b2ff8 100644
--- a/archive/sensitivity.lean
+++ b/archive/sensitivity.lean
@@ -373,7 +373,7 @@ begin
     rw set.range_restrict at hdW,
     convert hdW,
     rw [← (dual_pair_e_ε _).coe_basis, cardinal.mk_image_eq (dual_pair_e_ε _).basis.injective,
-        cardinal.fintype_card] },
+        cardinal.mk_fintype] },
   rw ← finrank_eq_dim ℝ at ⊢ dim_le dim_add dimW,
   rw [← finrank_eq_dim ℝ, ← finrank_eq_dim ℝ] at dim_add,
   norm_cast at ⊢ dim_le dim_add dimW,
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
index 638a9482cdf11..c32486ab37b14 100644
--- a/src/data/fintype/basic.lean
+++ b/src/data/fintype/basic.lean
@@ -1055,6 +1055,8 @@ instance Prop.fintype : fintype Prop :=
 ⟨⟨true ::ₘ false ::ₘ 0, by simp [true_ne_false]⟩,
  classical.cases (by simp) (by simp)⟩
 
+@[simp] lemma fintype.card_Prop : fintype.card Prop = 2 := rfl
+
 instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=
 fintype.subtype (univ.filter p) (by simp)
 
@@ -1923,6 +1925,22 @@ begin
     refine of_equiv e (h_option ih), },
 end
 
+/-- An induction principle for finite types, analogous to `nat.rec`. It effectively says
+that every `fintype` is either `empty` or `option α`, up to an `equiv`. -/
+@[elab_as_eliminator]
+lemma induction_empty_option' {P : Π (α : Type u) [fintype α], Prop}
+  (of_equiv : ∀ α β [fintype β] (e : α ≃ β), @P α (@fintype.of_equiv α β ‹_› e.symm) → @P β ‹_›)
+  (h_empty : P pempty)
+  (h_option : ∀ α [fintype α], by exactI P α → P (option α))
+  (α : Type u) [fintype α] : P α :=
+begin
+  obtain ⟨p⟩ := @trunc_rec_empty_option (λ α, ∀ h, @P α h)
+    (λ α β e hα hβ, @of_equiv α β hβ e (hα _)) (λ _i, by convert h_empty)
+    _ α _ (classical.dec_eq α),
+  { exact p _ },
+  { rintro α hα - Pα hα', resetI, convert h_option α (Pα _) }
+end
+
 /-- An induction principle for finite types, analogous to `nat.rec`. It effectively says
 that every `fintype` is either `empty` or `option α`, up to an `equiv`. -/
 lemma induction_empty_option {P : Type u → Prop}
@@ -1931,9 +1949,8 @@ lemma induction_empty_option {P : Type u → Prop}
   (h_option : ∀ {α} [fintype α], P α → P (option α))
   (α : Type u) [fintype α] : P α :=
 begin
-  haveI := classical.dec_eq α,
-  obtain ⟨p⟩ := trunc_rec_empty_option @of_equiv h_empty (λ _ _ _, by exactI h_option) α,
-  exact p,
+  refine induction_empty_option' _ _ _ α,
+  exacts [λ α β _, of_equiv, h_empty, @h_option]
 end
 
 end fintype
diff --git a/src/field_theory/finite/polynomial.lean b/src/field_theory/finite/polynomial.lean
index f98353bb7df1d..2728230cb2c79 100644
--- a/src/field_theory/finite/polynomial.lean
+++ b/src/field_theory/finite/polynomial.lean
@@ -172,7 +172,7 @@ calc module.rank K (R σ K) =
     (equiv.arrow_congr (equiv.refl σ) (equiv.fin_equiv_subtype _).symm).cardinal_eq
   ... = #(σ → K) :
     (equiv.arrow_congr (equiv.refl σ) (fintype.equiv_fin K).symm).cardinal_eq
-  ... = fintype.card (σ → K) : cardinal.fintype_card _
+  ... = fintype.card (σ → K) : cardinal.mk_fintype _
 
 instance : finite_dimensional K (R σ K) :=
 is_noetherian.iff_fg.1 $ is_noetherian.iff_dim_lt_omega.mpr
diff --git a/src/field_theory/finiteness.lean b/src/field_theory/finiteness.lean
index e07eeebdd51fb..a4a25d8a491b9 100644
--- a/src/field_theory/finiteness.lean
+++ b/src/field_theory/finiteness.lean
@@ -13,7 +13,7 @@ import linear_algebra.dimension
 
 universes u v
 
-open_locale classical
+open_locale classical cardinal
 open cardinal submodule module function
 
 namespace is_noetherian
@@ -26,9 +26,9 @@ variables [is_noetherian_ring K]
 
 /--
 A module over a division ring is noetherian if and only if
-its dimension (as a cardinal) is strictly less than the first infinite cardinal `omega`.
+its dimension (as a cardinal) is strictly less than the first infinite cardinal `ω`.
 -/
-lemma iff_dim_lt_omega : is_noetherian K V ↔ module.rank K V < omega.{v} :=
+lemma iff_dim_lt_omega : is_noetherian K V ↔ module.rank K V < ω :=
 begin
   let b := basis.of_vector_space K V,
   rw [← b.mk_eq_dim'', lt_omega_iff_finite],
@@ -45,8 +45,8 @@ end
 variables (K V)
 
 /-- The dimension of a noetherian module over a division ring, as a cardinal,
-is strictly less than the first infinite cardinal `omega`. -/
-lemma dim_lt_omega : ∀ [is_noetherian K V], module.rank K V < omega.{v} :=
+is strictly less than the first infinite cardinal `ω`. -/
+lemma dim_lt_omega : ∀ [is_noetherian K V], module.rank K V < ω :=
 is_noetherian.iff_dim_lt_omega.1
 
 variables {K V}
diff --git a/src/field_theory/fixed.lean b/src/field_theory/fixed.lean
index 464c7fc42b991..a240704dcdfc7 100644
--- a/src/field_theory/fixed.lean
+++ b/src/field_theory/fixed.lean
@@ -244,13 +244,10 @@ instance separable : is_separable (fixed_points.subfield G F) F :=
   exact polynomial.separable_prod_X_sub_C_iff.2 (injective_of_quotient_stabilizer G x) }⟩
 
 lemma dim_le_card : module.rank (fixed_points.subfield G F) F ≤ fintype.card G :=
-begin
-  refine dim_le (λ s hs, cardinal.nat_cast_le.1 _),
-  rw [← @dim_fun' F G, ← cardinal.lift_nat_cast.{v (max u v)},
-    cardinal.finset_card, ← cardinal.lift_id (module.rank F (G → F))],
-  exact cardinal_lift_le_dim_of_linear_independent.{_ _ _ (max u v)}
+dim_le $ λ s hs, by simpa only [dim_fun', cardinal.mk_finset, finset.coe_sort_coe,
+  cardinal.lift_nat_cast, cardinal.nat_cast_le]
+  using cardinal_lift_le_dim_of_linear_independent'
     (linear_independent_smul_of_linear_independent G F hs)
-end
 
 instance : finite_dimensional (fixed_points.subfield G F) F :=
 is_noetherian.iff_fg.1 $ is_noetherian.iff_dim_lt_omega.2 $
diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean
index 02f6931b55c76..7bb914470371e 100644
--- a/src/linear_algebra/dimension.lean
+++ b/src/linear_algebra/dimension.lean
@@ -496,7 +496,7 @@ begin
     haveI : fintype (range v) := set.fintype_range ⇑v,
     haveI := basis_fintype_of_finite_spans _ v.span_eq v',
     -- We clean up a little:
-    rw [cardinal.fintype_card, cardinal.fintype_card],
+    rw [cardinal.mk_fintype, cardinal.mk_fintype],
     simp only [cardinal.lift_nat_cast, cardinal.nat_cast_inj],
     -- Now we can use invariant basis number to show they have the same cardinality.
     apply card_eq_of_lequiv R,
@@ -569,7 +569,7 @@ lemma basis_le_span' {ι : Type*} (b : basis ι R M)
 begin
   haveI := nontrivial_of_invariant_basis_number R,
   haveI := basis_fintype_of_finite_spans w s b,
-  rw cardinal.fintype_card ι,
+  rw cardinal.mk_fintype ι,
   simp only [cardinal.nat_cast_le],
   exact basis.le_span'' b s,
 end
@@ -585,7 +585,7 @@ theorem basis.le_span {J : set M} (v : basis ι R M)
 begin
   haveI := nontrivial_of_invariant_basis_number R,
   casesI fintype_or_infinite J,
-  { rw [←cardinal.lift_le, cardinal.mk_range_eq_of_injective v.injective, cardinal.fintype_card J],
+  { rw [←cardinal.lift_le, cardinal.mk_range_eq_of_injective v.injective, cardinal.mk_fintype J],
     convert cardinal.lift_le.{w v}.2 (basis_le_span' v hJ),
     simp, },
   { have := cardinal.mk_range_eq_of_injective v.injective,
@@ -608,7 +608,7 @@ begin
     suffices : #(⋃ j, S' j) < #(range v),
     { exact not_le_of_lt this ⟨set.embedding_of_subset _ _ hs⟩ },
     refine lt_of_le_of_lt (le_trans cardinal.mk_Union_le_sum_mk
-      (cardinal.sum_le_sum _ (λ _, cardinal.omega) _)) _,
+      (cardinal.sum_le_sum _ (λ _, ω) _)) _,
     { exact λ j, le_of_lt (cardinal.lt_omega_iff_finite.2 $ (finset.finite_to_set _).image _) },
     { simpa } },
 end
@@ -670,7 +670,7 @@ lemma linear_independent_le_span' {ι : Type*} (v : ι → M) (i : linear_indepe
   #ι ≤ fintype.card w :=
 begin
   haveI : fintype ι := linear_independent_fintype_of_le_span_fintype v i w s,
-  rw cardinal.fintype_card,
+  rw cardinal.mk_fintype,
   simp only [cardinal.nat_cast_le],
   exact linear_independent_le_span_aux' v i w s,
 end
@@ -747,7 +747,7 @@ begin
   -- We split into cases depending on whether `ι` is infinite.
   cases fintype_or_infinite ι; resetI,
   { -- When `ι` is finite, we have `linear_independent_le_span`,
-    rw cardinal.fintype_card ι,
+    rw cardinal.mk_fintype ι,
     haveI : nontrivial R := nontrivial_of_invariant_basis_number R,
     rw fintype.card_congr (equiv.of_injective b b.injective),
     exact linear_independent_le_span v i (range b) b.span_eq, },
@@ -810,14 +810,14 @@ cardinality of the basis. -/
 lemma dim_eq_card_basis {ι : Type w} [fintype ι] (h : basis ι R M) :
   module.rank R M = fintype.card ι :=
 by {haveI := nontrivial_of_invariant_basis_number R,
-  rw [←h.mk_range_eq_dim, cardinal.fintype_card, set.card_range_of_injective h.injective] }
+  rw [←h.mk_range_eq_dim, cardinal.mk_fintype, set.card_range_of_injective h.injective] }
 
 lemma basis.card_le_card_of_linear_independent {ι : Type*} [fintype ι]
   (b : basis ι R M) {ι' : Type*} [fintype ι'] {v : ι' → M} (hv : linear_independent R v) :
   fintype.card ι' ≤ fintype.card ι :=
 begin
   letI := nontrivial_of_invariant_basis_number R,
-  simpa [dim_eq_card_basis b, cardinal.fintype_card] using
+  simpa [dim_eq_card_basis b, cardinal.mk_fintype] using
     cardinal_lift_le_dim_of_linear_independent' hv
 end
 
@@ -844,7 +844,7 @@ by simpa using v.mk_eq_dim
 
 /-- If a module has a finite dimension, all bases are indexed by a finite type. -/
 lemma basis.nonempty_fintype_index_of_dim_lt_omega {ι : Type*}
-  (b : basis ι R M) (h : module.rank R M < cardinal.omega) :
+  (b : basis ι R M) (h : module.rank R M < ω) :
   nonempty (fintype ι) :=
 by rwa [← cardinal.lift_lt, ← b.mk_eq_dim,
         -- ensure `omega` has the correct universe
@@ -853,13 +853,13 @@ by rwa [← cardinal.lift_lt, ← b.mk_eq_dim,
 
 /-- If a module has a finite dimension, all bases are indexed by a finite type. -/
 noncomputable def basis.fintype_index_of_dim_lt_omega {ι : Type*}
-  (b : basis ι R M) (h : module.rank R M < cardinal.omega) :
+  (b : basis ι R M) (h : module.rank R M < ω) :
   fintype ι :=
 classical.choice (b.nonempty_fintype_index_of_dim_lt_omega h)
 
 /-- If a module has a finite dimension, all bases are indexed by a finite set. -/
 lemma basis.finite_index_of_dim_lt_omega {ι : Type*} {s : set ι}
-  (b : basis s R M) (h : module.rank R M < cardinal.omega) :
+  (b : basis s R M) (h : module.rank R M < ω) :
   s.finite :=
 finite_def.2 (b.nonempty_fintype_index_of_dim_lt_omega h)
 
@@ -919,7 +919,7 @@ variables [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁
 variables {K V}
 
 /-- If a vector space has a finite dimension, the index set of `basis.of_vector_space` is finite. -/
-lemma basis.finite_of_vector_space_index_of_dim_lt_omega (h : module.rank K V < cardinal.omega) :
+lemma basis.finite_of_vector_space_index_of_dim_lt_omega (h : module.rank K V < ω) :
   (basis.of_vector_space_index K V).finite :=
 finite_def.2 $ (basis.of_vector_space K V).nonempty_fintype_index_of_dim_lt_omega h
 
@@ -980,10 +980,10 @@ begin
 end
 
 lemma dim_span_of_finset (s : finset V) :
-  module.rank K (span K (↑s : set V)) < cardinal.omega :=
+  module.rank K (span K (↑s : set V)) < ω :=
 calc module.rank K (span K (↑s : set V)) ≤ #(↑s : set V) : dim_span_le ↑s
-                             ... = s.card : by rw [cardinal.finset_card, finset.coe_sort_coe]
-                             ... < cardinal.omega : cardinal.nat_lt_omega _
+                             ... = s.card : by rw [finset.coe_sort_coe, cardinal.mk_finset]
+                             ... < ω : cardinal.nat_lt_omega _
 
 theorem dim_prod : module.rank K (V × V₁) = module.rank K V + module.rank K V₁ :=
 begin
@@ -1015,12 +1015,12 @@ end
 
 lemma dim_fun {V η : Type u} [fintype η] [add_comm_group V] [module K V] :
   module.rank K (η → V) = fintype.card η * module.rank K V :=
-by rw [dim_pi, cardinal.sum_const', cardinal.fintype_card]
+by rw [dim_pi, cardinal.sum_const', cardinal.mk_fintype]
 
 lemma dim_fun_eq_lift_mul :
   module.rank K (η → V) = (fintype.card η : cardinal.{max u₁' v}) *
     cardinal.lift.{u₁'} (module.rank K V) :=
-by rw [dim_pi, cardinal.sum_const, cardinal.fintype_card, cardinal.lift_nat_cast]
+by rw [dim_pi, cardinal.sum_const, cardinal.mk_fintype, cardinal.lift_nat_cast]
 
 lemma dim_fun' : module.rank K (η → K) = fintype.card η :=
 by rw [dim_fun_eq_lift_mul, dim_self, cardinal.lift_one, mul_one, cardinal.nat_cast_inj]
diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean
index 969a7cdaff01e..bd44b98074b09 100644
--- a/src/linear_algebra/finite_dimensional.lean
+++ b/src/linear_algebra/finite_dimensional.lean
@@ -218,7 +218,7 @@ lemma finrank_eq_card_basis' [finite_dimensional K V] {ι : Type w} (h : basis 
 begin
   haveI : is_noetherian K V := iff_fg.2 infer_instance,
   haveI : fintype ι := fintype_basis_index h,
-  rw [cardinal.fintype_card, finrank_eq_card_basis h]
+  rw [cardinal.mk_fintype, finrank_eq_card_basis h]
 end
 
 /-- If a vector space has a finite basis, then its dimension is equal to the cardinality of the
@@ -269,7 +269,7 @@ end
 lemma fintype_card_le_finrank_of_linear_independent
   [finite_dimensional K V] {ι : Type*} [fintype ι] {b : ι → V} (h : linear_independent K b) :
   fintype.card ι ≤ finrank K V :=
-by simpa [fintype_card] using cardinal_mk_le_finrank_of_linear_independent h
+by simpa using cardinal_mk_le_finrank_of_linear_independent h
 
 lemma finset_card_le_finrank_of_linear_independent [finite_dimensional K V] {b : finset V}
   (h : linear_independent K (λ x, x : b → V)) :
@@ -454,7 +454,7 @@ lemma _root_.complete_lattice.independent.subtype_ne_bot_le_finrank
   [finite_dimensional K V] {ι : Type w} {p : ι → submodule K V}
   (hp : complete_lattice.independent p) [fintype {i // p i ≠ ⊥}] :
   fintype.card {i // p i ≠ ⊥} ≤ finrank K V :=
-by simpa [cardinal.fintype_card] using hp.subtype_ne_bot_le_finrank_aux
+by simpa using hp.subtype_ne_bot_le_finrank_aux
 
 section
 open_locale big_operators
@@ -1149,7 +1149,7 @@ lemma finrank_span_le_card (s : set V) [fin : fintype s] :
 begin
   haveI := span_of_finite K ⟨fin⟩,
   have : module.rank K (span K s) ≤ #s := dim_span_le s,
-  rw [←finrank_eq_dim, cardinal.fintype_card, ←set.to_finset_card] at this,
+  rw [←finrank_eq_dim, cardinal.mk_fintype, ←set.to_finset_card] at this,
   exact_mod_cast this
 end
 
@@ -1165,7 +1165,7 @@ begin
   haveI : finite_dimensional K (span K (set.range b)) := span_of_finite K (set.finite_range b),
   have : module.rank K (span K (set.range b)) = #(set.range b) := dim_span hb,
   rwa [←finrank_eq_dim, ←lift_inj, mk_range_eq_of_injective hb.injective,
-    cardinal.fintype_card, lift_nat_cast, lift_nat_cast, nat_cast_inj] at this,
+    cardinal.mk_fintype, lift_nat_cast, lift_nat_cast, nat_cast_inj] at this,
 end
 
 lemma finrank_span_set_eq_card (s : set V) [fin : fintype s]
@@ -1174,7 +1174,7 @@ lemma finrank_span_set_eq_card (s : set V) [fin : fintype s]
 begin
   haveI := span_of_finite K ⟨fin⟩,
   have : module.rank K (span K s) = #s := dim_span_set hs,
-  rw [←finrank_eq_dim, cardinal.fintype_card, ←set.to_finset_card] at this,
+  rw [←finrank_eq_dim, cardinal.mk_fintype, ←set.to_finset_card] at this,
   exact_mod_cast this
 end
 
diff --git a/src/linear_algebra/free_module/finite/rank.lean b/src/linear_algebra/free_module/finite/rank.lean
index 009206e8e2331..7b5ee1edee0b6 100644
--- a/src/linear_algebra/free_module/finite/rank.lean
+++ b/src/linear_algebra/free_module/finite/rank.lean
@@ -109,7 +109,7 @@ begin
   letI := nontrivial_of_invariant_basis_number R,
   have h := (linear_map.to_matrix (choose_basis R M) (choose_basis R N)),
   let b := (matrix.std_basis _ _ _).map h.symm,
-  rw [finrank, dim_eq_card_basis b, ← fintype_card, mk_to_nat_eq_card, finrank, finrank,
+  rw [finrank, dim_eq_card_basis b, ← mk_fintype, mk_to_nat_eq_card, finrank, finrank,
     rank_eq_card_choose_basis_index, rank_eq_card_choose_basis_index, mk_to_nat_eq_card,
     mk_to_nat_eq_card, card_prod, mul_comm]
 end
diff --git a/src/linear_algebra/matrix/to_lin.lean b/src/linear_algebra/matrix/to_lin.lean
index 1395bdd864373..96f36e4d631e7 100644
--- a/src/linear_algebra/matrix/to_lin.lean
+++ b/src/linear_algebra/matrix/to_lin.lean
@@ -239,7 +239,7 @@ begin
   rw [vec_mul_vec_eq, matrix.to_lin'_mul],
   refine le_trans (rank_comp_le1 _ _) _,
   refine le_trans (rank_le_domain _) _,
-  rw [dim_fun', ← cardinal.lift_eq_nat_iff.mpr (cardinal.fintype_card unit), cardinal.mk_unit],
+  rw [dim_fun', ← cardinal.lift_eq_nat_iff.mpr (cardinal.mk_fintype unit), cardinal.mk_unit],
   exact le_of_eq (cardinal.lift_one)
 end
 
diff --git a/src/set_theory/cardinal.lean b/src/set_theory/cardinal.lean
index 8b2c46c9a6d7f..70ee8fa61b9c5 100644
--- a/src/set_theory/cardinal.lean
+++ b/src/set_theory/cardinal.lean
@@ -238,7 +238,7 @@ instance : has_zero cardinal.{u} := ⟨#pempty⟩
 
 instance : inhabited cardinal.{u} := ⟨0⟩
 
-@[simp] lemma mk_eq_zero (α : Type u) [is_empty α] : #α = 0 :=
+lemma mk_eq_zero (α : Type u) [is_empty α] : #α = 0 :=
 (equiv.equiv_pempty α).cardinal_eq
 
 @[simp] theorem lift_zero : lift 0 = 0 := mk_congr (equiv.equiv_pempty _)
@@ -255,7 +255,7 @@ instance : has_one cardinal.{u} := ⟨⟦punit⟧⟩
 
 instance : nontrivial cardinal.{u} := ⟨⟨1, 0, mk_ne_zero _⟩⟩
 
-@[simp] lemma mk_eq_one (α : Type u) [unique α] : #α = 1 :=
+lemma mk_eq_one (α : Type u) [unique α] : #α = 1 :=
 mk_congr equiv_punit_of_unique
 
 theorem le_one_iff_subsingleton {α : Type u} : #α ≤ 1 ↔ subsingleton α :=
@@ -276,6 +276,15 @@ mk_congr ((equiv.ulift).symm.sum_congr (equiv.ulift).symm)
 @[simp] lemma mk_psum (α : Type u) (β : Type v) : #(psum α β) = lift.{v} (#α) + lift.{u} (#β) :=
 (mk_congr (equiv.psum_equiv_sum α β)).trans (mk_sum α β)
 
+@[simp] lemma mk_fintype (α : Type u) [fintype α] : #α = fintype.card α :=
+begin
+  refine fintype.induction_empty_option' _ _ _ α,
+  { introsI α β h e hα, letI := fintype.of_equiv β e.symm,
+    rwa [mk_congr e, fintype.card_congr e] at hα },
+  { refl },
+  { introsI α h hα, simp [hα] }
+end
+
 instance : has_mul cardinal.{u} := ⟨map₂ prod $ λ α β γ δ, equiv.prod_congr⟩
 
 theorem mul_def (α β : Type u) : #α * #β = #(α × β) := rfl
@@ -362,11 +371,9 @@ instance : comm_semiring cardinal.{u} :=
 @[simp] theorem one_power {a : cardinal} : 1 ^ a = 1 :=
 induction_on a $ assume α, (equiv.arrow_punit_equiv_punit α).cardinal_eq
 
-@[simp] theorem mk_bool : #bool = 2 :=
-mk_congr equiv.bool_equiv_punit_sum_punit
+@[simp] theorem mk_bool : #bool = 2 := by simp
 
-@[simp] theorem mk_Prop : #(Prop) = 2 :=
-equiv.Prop_equiv_bool.cardinal_eq.trans mk_bool
+@[simp] theorem mk_Prop : #(Prop) = 2 := by simp
 
 @[simp] theorem zero_power {a : cardinal} : a ≠ 0 → 0 ^ a = 0 :=
 induction_on a $ assume α heq, mk_eq_zero_iff.2 $ is_empty_pi.2 $
@@ -750,12 +757,9 @@ by rw [← lift_omega, lift_le]
 @[simp] theorem lift_le_omega {c : cardinal.{u}} : lift.{v} c ≤ ω ↔ c ≤ ω :=
 by rw [← lift_omega, lift_le]
 
-/- properties about the cast from nat -/
+/-! ### Properties about the cast from `ℕ` -/
 
-@[simp] theorem mk_fin : ∀ (n : ℕ), #(fin n) = n
-| 0     := mk_eq_zero _
-| (n+1) := by rw [nat.cast_succ, ← mk_fin]; exact
-  quotient.sound (fintype.card_eq.1 $ by simp)
+@[simp] theorem mk_fin (n : ℕ) : #(fin n) = n := by simp
 
 @[simp] theorem lift_nat_cast (n : ℕ) : lift n = n :=
 by induction n; simp *
@@ -769,16 +773,14 @@ by rw [← lift_nat_cast.{u v} n, lift_inj]
 
 theorem lift_mk_fin (n : ℕ) : lift (#(fin n)) = n := by simp
 
-theorem fintype_card (α : Type u) [fintype α] : #α = fintype.card α :=
-by rw [← lift_mk_fin.{u}, ← lift_id (#α), lift_mk_eq.{u 0 u}];
-   exact fintype.card_eq.1 (by simp)
+lemma mk_finset {α : Type u} {s : finset α} : #s = ↑(finset.card s) := by simp
 
 theorem card_le_of_finset {α} (s : finset α) :
   (s.card : cardinal) ≤ #α :=
 begin
   rw (_ : (s.card : cardinal) = #s),
   { exact ⟨function.embedding.subtype _⟩ },
-  rw [cardinal.fintype_card, fintype.card_coe]
+  rw [cardinal.mk_fintype, fintype.card_coe]
 end
 
 @[simp, norm_cast] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
@@ -838,9 +840,8 @@ theorem lt_omega {c : cardinal.{u}} : c < ω ↔ ∃ n : ℕ, c = n :=
   rcases lt_lift_iff.1 h with ⟨c, rfl, h'⟩,
   rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩,
   suffices : finite S,
-  { cases this, resetI,
-    existsi fintype.card S,
-    rw [← lift_nat_cast.{0 u}, lift_inj, fintype_card S] },
+  { lift S to finset ℕ using this,
+    simp },
   contrapose! h',
   haveI := infinite.to_subtype h',
   exact ⟨infinite.nat_embedding S⟩
@@ -858,7 +859,7 @@ lt_omega.trans ⟨λ ⟨n, e⟩, begin
   rw [← lift_mk_fin n] at e,
   cases quotient.exact e with f,
   exact ⟨fintype.of_equiv _ f.symm⟩
-end, λ ⟨_⟩, by exactI ⟨_, fintype_card _⟩⟩
+end, λ ⟨_⟩, by exactI ⟨_, mk_fintype _⟩⟩
 
 theorem lt_omega_iff_finite {α} {S : set α} : #S < ω ↔ finite S :=
 lt_omega_iff_fintype.trans finite_def.symm
@@ -991,9 +992,7 @@ lemma to_nat_surjective : surjective to_nat := to_nat_right_inverse.surjective
 lemma mk_to_nat_of_infinite [h : infinite α] : (#α).to_nat = 0 :=
 dif_neg (not_lt_of_le (infinite_iff.1 h))
 
-@[simp]
-lemma mk_to_nat_eq_card [fintype α] : (#α).to_nat = fintype.card α :=
-by simp [fintype_card]
+lemma mk_to_nat_eq_card [fintype α] : (#α).to_nat = fintype.card α := by simp
 
 @[simp]
 lemma zero_to_nat : to_nat 0 = 0 :=
@@ -1096,9 +1095,8 @@ begin
     (λ n, ⟨n, to_enat_cast n⟩),
 end
 
-@[simp]
 lemma mk_to_enat_eq_coe_card [fintype α] : (#α).to_enat = fintype.card α :=
-by simp [fintype_card]
+by simp
 
 lemma mk_int : #ℤ = ω := mk_denumerable ℤ
 
@@ -1207,11 +1205,7 @@ mk_congr ((equiv.of_injective f h).symm)
 
 lemma mk_range_eq_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : injective f) :
   lift.{u} (#(range f)) = lift.{v} (#α) :=
-begin
-  have := (@lift_mk_eq.{v u max u v} (range f) α).2 ⟨(equiv.of_injective f hf).symm⟩,
-  simp only [lift_umax.{u v}, lift_umax.{v u}] at this,
-  exact this
-end
+lift_mk_eq'.mpr ⟨(equiv.of_injective f hf).symm⟩
 
 lemma mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} (hf : injective f) :
   lift.{(max u w)} (# (range f)) = lift.{(max v w)} (# α) :=
@@ -1242,9 +1236,6 @@ lemma mk_bUnion_le {ι α : Type u} (A : ι → set α) (s : set ι) :
   #(⋃(x ∈ s), A x) ≤ #s * cardinal.sup.{u u} (λ x : s, #(A x.1)) :=
 by { rw [bUnion_eq_Union], apply mk_Union_le }
 
-@[simp] lemma finset_card {α : Type u} {s : finset α} : ↑(finset.card s) = #s :=
-by rw [fintype_card, nat_cast_inj, fintype.card_coe]
-
 lemma finset_card_lt_omega (s : finset α) : #(↑s : set α) < ω :=
 by { rw [lt_omega_iff_fintype], exact ⟨finset.subtype.fintype s⟩ }
 
@@ -1253,11 +1244,10 @@ theorem mk_eq_nat_iff_finset {α} {s : set α} {n : ℕ} :
 begin
   split,
   { intro h,
-    have : # s < omega, by { rw h, exact nat_lt_omega n },
-    refine ⟨(lt_omega_iff_finite.1 this).to_finset, finite.coe_to_finset _, nat_cast_inj.1 _⟩,
-    rwa [finset_card, finite.coe_sort_to_finset] },
+    lift s to finset α using lt_omega_iff_finite.1 (h.symm ▸ nat_lt_omega n),
+    simpa using h },
   { rintro ⟨t, rfl, rfl⟩,
-    exact finset_card.symm }
+    exact mk_finset }
 end
 
 theorem mk_union_add_mk_inter {α : Type u} {S T : set α} :
diff --git a/src/set_theory/cofinality.lean b/src/set_theory/cofinality.lean
index 5d98ad6ea9d49..42eff6b38f424 100644
--- a/src/set_theory/cofinality.lean
+++ b/src/set_theory/cofinality.lean
@@ -208,7 +208,7 @@ begin
     rw [← (_ : #_ = 1)], apply cof_type_le,
     { refine λ a, ⟨sum.inr punit.star, set.mem_singleton _, _⟩,
       rcases a with a|⟨⟨⟨⟩⟩⟩; simp [empty_relation] },
-    { rw [cardinal.fintype_card, set.card_singleton], simp } },
+    { rw [cardinal.mk_fintype, set.card_singleton], simp } },
   { rw [← cardinal.succ_zero, cardinal.succ_le],
     simpa [lt_iff_le_and_ne, cardinal.zero_le] using
       λ h, succ_ne_zero o (cof_eq_zero.1 (eq.symm h)) }
diff --git a/src/set_theory/ordinal_arithmetic.lean b/src/set_theory/ordinal_arithmetic.lean
index ab6ad7df3f5b4..433a5613d02dd 100644
--- a/src/set_theory/ordinal_arithmetic.lean
+++ b/src/set_theory/ordinal_arithmetic.lean
@@ -1376,8 +1376,8 @@ by induction n with n ih; [simp only [nat.cast_zero, lift_zero],
 theorem lift_type_fin (n : ℕ) : lift (@type (fin n) (<) _) = n :=
 by simp only [type_fin, lift_nat_cast]
 
-theorem fintype_card (r : α → α → Prop) [is_well_order α r] [fintype α] : type r = fintype.card α :=
-by rw [← card_eq_nat, card_type, fintype_card]
+theorem type_fintype (r : α → α → Prop) [is_well_order α r] [fintype α] : type r = fintype.card α :=
+by rw [← card_eq_nat, card_type, mk_fintype]
 
 end ordinal