chore(set_theory/cardinal): fix name & reorder universes (#10236)

* add `cardinal.lift_injective`, `cardinal.lift_eq_zero`;
* reorder universe arguments in `cardinal.lift_nat_cast` to match
`cardinal.lift` and `ulift`;
* rename `cardinal.nat_eq_lift_eq_iff` to `cardinal.nat_eq_lift_iff`;
* add `@[simp]` to `cardinal.lift_eq_zero`,
`cardinal.lift_eq_nat_iff`, and `cardinal.nat_eq_lift_iff`.

src/linear_algebra/finite_dimensional.lean

@@ -411,11 +411,7 @@ end
 /-- Pushforwards of finite-dimensional submodules have a smaller finrank. -/
 lemma finrank_map_le (f : V →ₗ[K] V₂) (p : submodule K V) [finite_dimensional K p] :
   finrank K (p.map f) ≤ finrank K p :=
-begin
-  rw [← cardinal.nat_cast_le.{max v v'}, ← cardinal.lift_nat_cast.{v' v},
-    ← cardinal.lift_nat_cast.{v v'}, finrank_eq_dim K p, finrank_eq_dim K (p.map f)],
-  exact lift_dim_map_le f p
-end
+by simpa [← finrank_eq_dim] using lift_dim_map_le f p
 
 variable {K}
 

src/linear_algebra/matrix/to_lin.lean

@@ -234,13 +234,12 @@ linear_map.to_matrix_alg_equiv'_comp f g
 
 lemma matrix.rank_vec_mul_vec {K m n : Type u} [field K] [fintype n] [decidable_eq n]
   (w : m → K) (v : n → K) :
-rank (vec_mul_vec w v).to_lin' ≤ 1 :=
+  rank (vec_mul_vec w v).to_lin' ≤ 1 :=
 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.mk_fintype unit), cardinal.mk_unit],
-  exact le_of_eq (cardinal.lift_one)
+  refine (rank_le_domain _).trans_eq _,
+  rw [dim_fun', fintype.card_unit, nat.cast_one]
 end
 
 end to_matrix'

src/set_theory/cardinal.lean

@@ -228,8 +228,10 @@ induction_on₂ a b $ λ α β, by { rw ← lift_umax, exact lift_mk_le }
 @[simps { fully_applied := ff }] def lift_order_embedding : cardinal.{v} ↪o cardinal.{max v u} :=
 order_embedding.of_map_le_iff lift (λ _ _, lift_le)
 
+theorem lift_injective : injective lift.{u v} := lift_order_embedding.injective
+
 @[simp] theorem lift_inj {a b : cardinal} : lift a = lift b ↔ a = b :=
-lift_order_embedding.injective.eq_iff
+lift_injective.eq_iff
 
 @[simp] theorem lift_lt {a b : cardinal} : lift a < lift b ↔ a < b :=
 lift_order_embedding.lt_iff_lt
@@ -243,6 +245,9 @@ lemma mk_eq_zero (α : Type u) [is_empty α] : #α = 0 :=
 
 @[simp] theorem lift_zero : lift 0 = 0 := mk_congr (equiv.equiv_pempty _)
 
+@[simp] theorem lift_eq_zero {a : cardinal.{v}} : lift.{u} a = 0 ↔ a = 0 :=
+lift_injective.eq_iff' lift_zero
+
 lemma mk_eq_zero_iff {α : Type u} : #α = 0 ↔ is_empty α :=
 ⟨λ e, let ⟨h⟩ := quotient.exact e in h.is_empty, @mk_eq_zero α⟩
 
@@ -761,15 +766,15 @@ by rw [← lift_omega, lift_le]
 
 @[simp] theorem mk_fin (n : ℕ) : #(fin n) = n := by simp
 
-@[simp] theorem lift_nat_cast (n : ℕ) : lift n = n :=
+@[simp] theorem lift_nat_cast (n : ℕ) : lift.{u} (n : cardinal.{v}) = n :=
 by induction n; simp *
 
-lemma lift_eq_nat_iff {a : cardinal.{u}} {n : ℕ} : lift.{v} a = n ↔ a = n :=
-by rw [← lift_nat_cast.{u v} n, lift_inj]
+@[simp] lemma lift_eq_nat_iff {a : cardinal.{u}} {n : ℕ} : lift.{v} a = n ↔ a = n :=
+lift_injective.eq_iff' (lift_nat_cast n)
 
-lemma nat_eq_lift_eq_iff {n : ℕ} {a : cardinal.{u}} :
+@[simp] lemma nat_eq_lift_iff {n : ℕ} {a : cardinal.{u}} :
   (n : cardinal) = lift.{v} a ↔ (n : cardinal) = a :=
-by rw [← lift_nat_cast.{u v} n, lift_inj]
+by rw [← lift_nat_cast.{v} n, lift_inj]
 
 theorem lift_mk_fin (n : ℕ) : lift (#(fin n)) = n := by simp
 

src/set_theory/cardinal_ordinal.lean

@@ -614,7 +614,7 @@ begin
   { refine lt_of_le_of_lt (mk_subtype_le _) _,
     rw [← lift_lt, lift_omega, ← h1', ← lift_omega.{u (max v w)}, lift_lt], exact hα' },
   lift #(tᶜ : set β) to ℕ using this with k hk,
-  simp [nat_eq_lift_eq_iff] at h2, rw [nat_eq_lift_eq_iff.{v (max u w)}] at h2,
+  simp at h2, rw [nat_eq_lift_iff.{v (max u w)}] at h2,
   simp [h2.symm] at h1 ⊢, norm_cast at h1, simp at h1, exact h1
 end