chore(set_theory/cardinal): more simp, fix LHS/RHS (#10212)

While `coe (fintype.card α)` is a larger expression than `#α`, it allows us to compute the cardinality of a finite type provided that we have a `simp` lemma for `fintype.card α`. It also plays well with lemmas about coercions from `nat` and `cardinal.lift`.

* rename `cardinal.fintype_card` to `cardinal.mk_fintype`, make it a `@[simp]` lemma;
* deduce other cases (`bool`, `Prop`, `unique`, `is_empty`) from it;
* rename `cardinal.finset_card` to `cardinal.mk_finset`, swap LHS/RHS;
* rename `ordinal.fintype_card` to `ordinal.type_fintype`.

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) :

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,

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

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

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}

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 $

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]

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
 

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

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