refactor(set_theory/cardinal/basic): constrain universes

src/computability/encoding.lean

@@ -192,7 +192,7 @@ instance inhabited_encoding : inhabited (encoding bool) := ⟨fin_encoding_bool_
 
 lemma encoding.card_le_card_list {α : Type u} (e : encoding.{u v} α) :
   cardinal.lift.{v} (# α) ≤ cardinal.lift.{u} (# (list e.Γ)) :=
-(cardinal.lift_mk_le').2 ⟨⟨e.encode, e.encode_injective⟩⟩
+cardinal.lift_mk_le.2 ⟨⟨e.encode, e.encode_injective⟩⟩
 
 lemma encoding.card_le_aleph_0 {α : Type u} (e : encoding.{u v} α) [encodable e.Γ] : #α ≤ ℵ₀ :=
 begin

src/field_theory/finiteness.lean

@@ -27,7 +27,7 @@ its dimension (as a cardinal) is strictly less than the first infinite cardinal
 lemma iff_dim_lt_aleph_0 : is_noetherian K V ↔ module.rank K V < ℵ₀ :=
 begin
   let b := basis.of_vector_space K V,
-  rw [← b.mk_eq_dim'', lt_aleph_0_iff_finite],
+  rw [← b.mk_eq_dim', lt_aleph_0_iff_finite],
   split,
   { introI,
     exact finite_of_linear_independent (basis.of_vector_space_index.linear_independent K V) },

src/group_theory/solvable.lean

@@ -209,7 +209,7 @@ begin
   introI h,
   have key : nonempty (fin 5 ↪ X),
   { rwa [←cardinal.lift_mk_le, cardinal.mk_fin, cardinal.lift_nat_cast,
-    nat.cast_bit1, nat.cast_bit0, nat.cast_one, cardinal.lift_id] },
+      nat.cast_bit1, nat.cast_bit0, nat.cast_one, cardinal.lift_uzero] },
   exact equiv.perm.fin_5_not_solvable (solvable_of_solvable_injective
     (equiv.perm.via_embedding_hom_injective (nonempty.some key))),
 end

src/linear_algebra/dimension.lean

@@ -68,8 +68,11 @@ This reflects that `module.rank` was originally called `dim`, and only defined f
 
 Many theorems in this file are not universe-generic when they relate dimensions
 in different universes. They should be as general as they can be without
-inserting `lift`s. The types `V`, `V'`, ... all live in different universes,
+inserting `cardinal.lift`s. The types `V`, `V'`, ... all live in different universes,
 and `V₁`, `V₂`, ... all live in the same universe.
+
+For those lemmas that do employ `cardinal.lift`, take library
+note [cardinal comparison in different universes] in mind.
 -/
 
 noncomputable theory
@@ -123,7 +126,7 @@ begin
     cardinal.lift_supr (cardinal.bdd_above_range.{v v} _)],
   apply csupr_mono' (cardinal.bdd_above_range.{v' v} _),
   rintro ⟨s, li⟩,
-  refine ⟨⟨f '' s, _⟩, cardinal.lift_mk_le'.mpr ⟨(equiv.set.image f s i).to_embedding⟩⟩,
+  refine ⟨⟨f '' s, _⟩, cardinal.lift_mk_le.mpr ⟨(equiv.set.image f s i).to_embedding⟩⟩,
   exact (li.map' _ $ linear_map.ker_eq_bot.mpr i).image,
 end
 
@@ -153,7 +156,7 @@ begin
   refine (le_csupr (cardinal.bdd_above_range.{v v} _) ⟨range_splitting f '' s, _⟩),
   { apply linear_independent.of_comp f.range_restrict,
     convert li.comp (equiv.set.range_splitting_image_equiv f s) (equiv.injective _) using 1, },
-  { exact (cardinal.lift_mk_eq'.mpr ⟨equiv.set.range_splitting_image_equiv f s⟩).ge, },
+  { exact (cardinal.lift_mk_eq.mpr ⟨equiv.set.range_splitting_image_equiv f s⟩).ge, },
 end
 
 lemma dim_range_le (f : M →ₗ[R] M₁) : module.rank R f.range ≤ module.rank R M :=
@@ -231,9 +234,9 @@ theorem dim_quotient_le (p : submodule R M) :
 
 variables [nontrivial R]
 
-lemma {m} cardinal_lift_le_dim_of_linear_independent
+lemma cardinal_lift_le_dim_of_linear_independent
   {ι : Type w} {v : ι → M} (hv : linear_independent R v) :
-  cardinal.lift.{max v m} (#ι) ≤ cardinal.lift.{max w m} (module.rank R M) :=
+  cardinal.lift.{v} (#ι) ≤ cardinal.lift.{w} (module.rank R M) :=
 begin
   apply le_trans,
   { exact cardinal.lift_mk_le.mpr
@@ -248,7 +251,7 @@ end
 lemma cardinal_lift_le_dim_of_linear_independent'
   {ι : Type w} {v : ι → M} (hv : linear_independent R v) :
   cardinal.lift.{v} (#ι) ≤ cardinal.lift.{w} (module.rank R M) :=
-cardinal_lift_le_dim_of_linear_independent.{u v w 0} hv
+cardinal_lift_le_dim_of_linear_independent hv
 
 lemma cardinal_le_dim_of_linear_independent
   {ι : Type v} {v : ι → M} (hv : linear_independent R v) :
@@ -505,7 +508,7 @@ begin
     -- we see they have the same cardinality.
     have w₁ :=
       infinite_basis_le_maximal_linear_independent' v _ v'.linear_independent v'.maximal,
-    rcases cardinal.lift_mk_le'.mp w₁ with ⟨f⟩,
+    rcases cardinal.lift_mk_le.mp w₁ with ⟨f⟩,
     haveI : infinite ι' := infinite.of_injective f f.2,
     have w₂ :=
       infinite_basis_le_maximal_linear_independent' v' _ v.linear_independent v.maximal,
@@ -515,7 +518,7 @@ end
 /-- Given two bases indexed by `ι` and `ι'` of an `R`-module, where `R` satisfies the invariant
 basis number property, an equiv `ι ≃ ι' `. -/
 def basis.index_equiv (v : basis ι R M) (v' : basis ι' R M) : ι ≃ ι' :=
-nonempty.some (cardinal.lift_mk_eq.1 (cardinal.lift_umax_eq.2 (mk_eq_mk_of_basis v v')))
+(cardinal.lift_mk_eq.1 $ mk_eq_mk_of_basis v v').some
 
 theorem mk_eq_mk_of_basis' {ι' : Type w} (v : basis ι R M) (v' : basis ι' R M) :
   #ι = #ι' :=
@@ -773,8 +776,7 @@ begin
     exact infinite_basis_le_maximal_linear_independent b v i m, }
 end
 
-theorem basis.mk_eq_dim'' {ι : Type v} (v : basis ι R M) :
-  #ι = module.rank R M :=
+theorem basis.mk_eq_dim' {ι : Type v} (v : basis ι R M) : #ι = module.rank R M :=
 begin
   haveI := nontrivial_of_invariant_basis_number R,
   apply le_antisymm,
@@ -794,7 +796,7 @@ attribute [irreducible] module.rank
 
 theorem basis.mk_range_eq_dim (v : basis ι R M) :
   #(range v) = module.rank R M :=
-v.reindex_range.mk_eq_dim''
+v.reindex_range.mk_eq_dim'
 
 /-- If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the
 cardinality of the basis. -/
@@ -829,10 +831,6 @@ begin
   rw [←v.mk_range_eq_dim, cardinal.mk_range_eq_of_injective v.injective]
 end
 
-theorem {m} basis.mk_eq_dim' (v : basis ι R M) :
-  cardinal.lift.{max v m} (#ι) = cardinal.lift.{max w m} (module.rank R M) :=
-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_aleph_0 {ι : Type*}
   (b : basis ι R M) (h : module.rank R M < ℵ₀) :
@@ -924,8 +922,8 @@ begin
   let B := basis.of_vector_space K V,
   let B' := basis.of_vector_space K V',
   have : cardinal.lift.{v' v} (#_) = cardinal.lift.{v v'} (#_),
-    by rw [B.mk_eq_dim'', cond, B'.mk_eq_dim''],
-  exact (cardinal.lift_mk_eq.{v v' 0}.1 this).map (B.equiv B')
+    by rw [B.mk_eq_dim', cond, B'.mk_eq_dim'],
+  exact (cardinal.lift_mk_eq.1 this).map (B.equiv B')
 end
 
 /-- Two vector spaces are isomorphic if they have the same dimension. -/
@@ -1193,7 +1191,7 @@ begin
   split,
   { intro h,
     let t := basis.of_vector_space K V,
-    rw [← t.mk_eq_dim'', cardinal.le_mk_iff_exists_subset] at h,
+    rw [← t.mk_eq_dim', cardinal.le_mk_iff_exists_subset] at h,
     rcases h with ⟨s, hst, hsc⟩,
     exact ⟨s, hsc, (of_vector_space_index.linear_independent K V).mono hst⟩ },
   { rintro ⟨s, rfl, si⟩,
@@ -1219,7 +1217,7 @@ begin
   let b := basis.of_vector_space K V,
   split,
   { intro hd,
-    rw [← b.mk_eq_dim'', cardinal.le_one_iff_subsingleton, subsingleton_coe] at hd,
+    rw [← b.mk_eq_dim', cardinal.le_one_iff_subsingleton, subsingleton_coe] at hd,
     rcases eq_empty_or_nonempty (of_vector_space_index K V) with hb | ⟨⟨v₀, hv₀⟩⟩,
     { use 0,
       have h' : ∀ v : V, v = 0, { simpa [hb, submodule.eq_bot_iff] using b.span_eq.symm },

src/linear_algebra/finite_dimensional.lean

@@ -285,9 +285,8 @@ lemma cardinal_mk_le_finrank_of_linear_independent
   [finite_dimensional K V] {ι : Type w} {b : ι → V} (h : linear_independent K b) :
   #ι ≤ finrank K V :=
 begin
-  rw ← lift_le.{_ (max v w)},
-  simpa [← finrank_eq_dim K V] using
-    cardinal_lift_le_dim_of_linear_independent.{_ _ _ (max v w)} h
+  rw ← lift_le,
+  simpa [← finrank_eq_dim K V] using cardinal_lift_le_dim_of_linear_independent h
 end
 
 lemma fintype_card_le_finrank_of_linear_independent

src/linear_algebra/finsupp_vector_space.lean

@@ -125,7 +125,7 @@ variables [field K] [add_comm_group V] [module K V]
 lemma dim_eq : module.rank K (ι →₀ V) = #ι * module.rank K V :=
 begin
   let bs := basis.of_vector_space K V,
-  rw [← bs.mk_eq_dim'', ← (finsupp.basis (λa:ι, bs)).mk_eq_dim'',
+  rw [← bs.mk_eq_dim', ← (finsupp.basis (λa:ι, bs)).mk_eq_dim',
     cardinal.mk_sigma, cardinal.sum_const']
 end
 

src/linear_algebra/free_module/finite/rank.lean

@@ -38,7 +38,7 @@ variables [add_comm_group N] [module R N] [module.free R N] [module.finite R N]
 lemma rank_lt_aleph_0 : module.rank R M < ℵ₀ :=
 begin
   letI := nontrivial_of_invariant_basis_number R,
-  rw [← (choose_basis R M).mk_eq_dim'', lt_aleph_0_iff_fintype],
+  rw [← (choose_basis R M).mk_eq_dim', lt_aleph_0_iff_fintype],
   exact nonempty.intro infer_instance
 end
 

src/linear_algebra/free_module/rank.lean

@@ -33,7 +33,7 @@ variables [add_comm_group N] [module R N] [module.free R N]
 
 /-- The rank of a free module `M` over `R` is the cardinality of `choose_basis_index R M`. -/
 lemma rank_eq_card_choose_basis_index : module.rank R M = #(choose_basis_index R M) :=
-(choose_basis R M).mk_eq_dim''.symm
+(choose_basis R M).mk_eq_dim'.symm
 
 /-- The rank of `(ι →₀ R)` is `(# ι).lift`. -/
 @[simp] lemma rank_finsupp {ι : Type v} : module.rank R (ι →₀ R) = (# ι).lift :=
@@ -61,7 +61,7 @@ lemma rank_prod' (N : Type v) [add_comm_group N] [module R N] [module.free R N]
 begin
   let B := λ i, choose_basis R (M i),
   let b : basis _ R (⨁ i, M i) := dfinsupp.basis (λ i, B i),
-  simp [← b.mk_eq_dim'', λ i, (B i).mk_eq_dim''],
+  simp [← b.mk_eq_dim', λ i, (B i).mk_eq_dim'],
 end
 
 /-- The rank of a finite product is the sum of the ranks. -/

src/model_theory/basic.lean

@@ -698,12 +698,12 @@ variables [language.empty.Structure M] [language.empty.Structure N]
 @[simp] lemma empty.nonempty_embedding_iff :
   nonempty (M ↪[language.empty] N) ↔ cardinal.lift.{w'} (# M) ≤ cardinal.lift.{w} (# N) :=
 trans ⟨nonempty.map (λ f, f.to_embedding), nonempty.map (λ f, {to_embedding := f})⟩
-  cardinal.lift_mk_le'.symm
+  cardinal.lift_mk_le.symm
 
 @[simp] lemma empty.nonempty_equiv_iff :
   nonempty (M ≃[language.empty] N) ↔ cardinal.lift.{w'} (# M) = cardinal.lift.{w} (# N) :=
 trans ⟨nonempty.map (λ f, f.to_equiv), nonempty.map (λ f, {to_equiv := f})⟩
-  cardinal.lift_mk_eq'.symm
+  cardinal.lift_mk_eq.symm
 
 end
 

src/model_theory/satisfiability.lean

@@ -113,7 +113,7 @@ theorem is_satisfiable_union_distinct_constants_theory_of_card_le (T : L.Theory)
   ((L.Lhom_with_constants α).on_Theory T ∪ L.distinct_constants_theory s).is_satisfiable :=
 begin
   haveI : inhabited M := classical.inhabited_of_nonempty infer_instance,
-  rw [cardinal.lift_mk_le'] at h,
+  rw [cardinal.lift_mk_le] at h,
   letI : (constants_on α).Structure M :=
     constants_on.Structure (function.extend coe h.some default),
   haveI : M ⊨ (L.Lhom_with_constants α).on_Theory T ∪ L.distinct_constants_theory s,

src/model_theory/semantics.lean

@@ -884,7 +884,7 @@ end
 lemma card_le_of_model_distinct_constants_theory (s : set α) (M : Type w) [L[[α]].Structure M]
   [h : M ⊨ L.distinct_constants_theory s] :
   cardinal.lift.{w} (# s) ≤ cardinal.lift.{u'} (# M) :=
-lift_mk_le'.2 ⟨⟨_, set.inj_on_iff_injective.1 ((L.model_distinct_constants_theory s).1 h)⟩⟩
+lift_mk_le.2 ⟨⟨_, set.inj_on_iff_injective.1 ((L.model_distinct_constants_theory s).1 h)⟩⟩
 
 end cardinality