refactor(set_theory/cardinal): swap sides of simp lemmas (#10040)

## API changes

### Swap sides of simp lemmas

- `cardinal.add_def` is no loner a `simp` lemma, `cardinal.mk_sum` (renamed from `cardinal.add`) simplifies `#(α ⊕ β)` to `lift.{v u} (#α) + lift.{u v} (#β)`;
- `cardinal.mul_def` is no loner a `simp` lemma, `cardinal.mk_prod` (merged with `cardinal.mul`) simplifies `#(α × β)` to `lift.{v u} (#α) * lift.{u v} (#β)`;
- `cardinal.power_def` is no longer a `simp` lemma. New lemma `cardinal.mk_arrow` computes `#(α → β)`. It is not a `simp` lemma because it follows from other `simp` lemmas.
- replace `cardinal.sum_mk` with `cardinal.mk_sigma` and `cardinal.prod_mk` with `cardinal.mk_pi`;

### Other changes

- new lemmas `@[simp] cardinal.lift_uzero` and `cardinal.lift_umax'`;
- split `cardinal.linear_order` into `cardinal.preorder` (doesn't rely on `classical.choice`), `cardinal.partial_order` (needs `classical.choice`, computable), and `cardinal.linear_order` (noncomputable);
- add `cardinal.lift_order_embedding`;
- add `cardinal.mk_psum`;
- rename `cardinal.prop_eq_two` to `cardinal.mk_Prop`, drop the old `mk_Prop`;
- use local notation for natural power;
- rename old `sum_const` to `sum_const'`, the new `@[simp] lemma sum_const` is what used to be `sum_const_eq_lift_mul`;
- rename old `prod_const` to `prod_const'`, the new `@[simp] lemma prod_const` deals with types in different universes;
- add `@[simp]` to `cardinal.prod_eq_zero` and `cardinal.omega_le_mk`;
- add `@[simp]` lemmas `cardinal.mk_eq_one`, `cardinal.mk_vector`, `cardinal.omega_mul_eq`, and `cardinal.mul_omega_eq`;
- replace `mk_plift_of_true` and `mk_plift_of_false` with `mk_plift_true` and `mk_plift_false`;
- `mk_list_eq_mk` and `mk_finset_eq_mk` now assume `[infinite α]` instead of `ω ≤ #α`.

src/data/W/cardinal.lean

@@ -34,17 +34,16 @@ open cardinal
 
 lemma cardinal_mk_eq_sum : #(W_type β) = sum (λ a : α, #(W_type β) ^ #(β a)) :=
 begin
-  simp only [cardinal.power_def, cardinal.sum_mk],
-  exact cardinal.eq.2 ⟨equiv_sigma β⟩
+  simp only [cardinal.power_def, ← cardinal.mk_sigma],
+  exact mk_congr (equiv_sigma β)
 end
 
 /-- `#(W_type β)` is the least cardinal `κ` such that `sum (λ a : α, κ ^ #(β a)) ≤ κ` -/
 lemma cardinal_mk_le_of_le {κ : cardinal.{u}} (hκ : sum (λ a : α, κ ^ #(β a)) ≤ κ) :
   #(W_type β) ≤ κ :=
 begin
-  conv_rhs { rw ← cardinal.mk_out κ},
-  rw [← cardinal.mk_out κ] at hκ,
-  simp only [cardinal.power_def, cardinal.sum_mk, cardinal.le_def] at hκ,
+  induction κ using cardinal.induction_on with γ,
+  simp only [cardinal.power_def, ← cardinal.mk_sigma, cardinal.le_def] at hκ,
   cases hκ,
   exact cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)
 end

src/data/array/lemmas.lean

@@ -282,10 +282,6 @@ def d_array_equiv_fin {n : ℕ} (α : fin n → Type*) : d_array n α ≃ (Π i,
 def array_equiv_fin (n : ℕ) (α : Type*) : array n α ≃ (fin n → α) :=
 d_array_equiv_fin _
 
-/-- The natural equivalence between length-`n` vectors and functions from `fin n`. -/
-def vector_equiv_fin (α : Type*) (n : ℕ) : vector α n ≃ (fin n → α) :=
-⟨vector.nth, vector.of_fn, vector.of_fn_nth, λ f, funext $ vector.nth_of_fn f⟩
-
 /-- The natural equivalence between length-`n` vectors and length-`n` arrays. -/
 def vector_equiv_array (α : Type*) (n : ℕ) : vector α n ≃ array n α :=
 (vector_equiv_fin _ _).trans (array_equiv_fin _ _).symm

src/data/vector/basic.lean

@@ -88,6 +88,10 @@ begin
   simpa only [to_list_of_fn] using list.of_fn_nth_le _
 end
 
+/-- The natural equivalence between length-`n` vectors and functions from `fin n`. -/
+def _root_.equiv.vector_equiv_fin (α : Type*) (n : ℕ) : vector α n ≃ (fin n → α) :=
+⟨vector.nth, vector.of_fn, vector.of_fn_nth, λ f, funext $ vector.nth_of_fn f⟩
+
 theorem nth_tail (x : vector α n) (i) :
   x.tail.nth i = x.nth ⟨i.1 + 1, lt_tsub_iff_right.mp i.2⟩ :=
 by { rcases x with ⟨_|_, h⟩; refl, }

src/linear_algebra/dimension.lean

@@ -584,7 +584,10 @@ theorem basis.le_span {J : set M} (v : basis ι R M)
    (hJ : span R J = ⊤) : #(range v) ≤ #J :=
 begin
   haveI := nontrivial_of_invariant_basis_number R,
-  cases le_or_lt ω (#J) with oJ oJ,
+  casesI fintype_or_infinite J,
+  { rw [←cardinal.lift_le, cardinal.mk_range_eq_of_injective v.injective, cardinal.fintype_card J],
+    convert cardinal.lift_le.{w v}.2 (basis_le_span' v hJ),
+    simp, },
   { have := cardinal.mk_range_eq_of_injective v.injective,
     let S : J → set ι := λ j, ↑(v.repr j).support,
     let S' : J → set M := λ j, v '' S j,
@@ -607,11 +610,7 @@ begin
     refine lt_of_le_of_lt (le_trans cardinal.mk_Union_le_sum_mk
       (cardinal.sum_le_sum _ (λ _, cardinal.omega) _)) _,
     { exact λ j, le_of_lt (cardinal.lt_omega_iff_finite.2 $ (finset.finite_to_set _).image _) },
-    { rwa [cardinal.sum_const, cardinal.mul_eq_max oJ (le_refl _), max_eq_left oJ] } },
-  { haveI : fintype J := (cardinal.lt_omega_iff_fintype.mp oJ).some,
-    rw [←cardinal.lift_le, cardinal.mk_range_eq_of_injective v.injective, cardinal.fintype_card J],
-    convert cardinal.lift_le.{w v}.2 (basis_le_span' v hJ),
-    simp, },
+    { simpa } },
 end
 
 end rank_condition
@@ -721,13 +720,9 @@ lemma linear_independent_le_infinite_basis
   #κ ≤ #ι :=
 begin
   by_contradiction,
-  simp only [not_le] at h,
-  have w : #(finset ι) = #ι :=
-    cardinal.mk_finset_eq_mk (cardinal.infinite_iff.mp ‹infinite ι›),
-  rw ←w at h,
+  rw [not_le, ← cardinal.mk_finset_eq_mk ι] at h,
   let Φ := λ k : κ, (b.repr (v k)).support,
-  obtain ⟨s, w : infinite ↥(Φ ⁻¹' {s})⟩ := cardinal.exists_infinite_fiber Φ h
-    (by { rw [cardinal.infinite_iff, w], exact (cardinal.infinite_iff.mp ‹infinite ι›), }),
+  obtain ⟨s, w : infinite ↥(Φ ⁻¹' {s})⟩ := cardinal.exists_infinite_fiber Φ h (by apply_instance),
   let v' := λ k : Φ ⁻¹' {s}, v k,
   have i' : linear_independent R v' := i.comp _ subtype.val_injective,
   have w' : fintype (Φ ⁻¹' {s}),
@@ -1014,18 +1009,18 @@ lemma dim_pi : module.rank K (Πi, φ i) = cardinal.sum (λi, module.rank K (φ
 begin
   let b := assume i, basis.of_vector_space K (φ i),
   let this : basis (Σ j, _) K (Π j, φ j) := pi.basis b,
-  rw [←cardinal.lift_inj, ← this.mk_eq_dim],
-  simp [λ i, (b i).mk_range_eq_dim.symm, cardinal.sum_mk]
+  rw [← cardinal.lift_inj, ← this.mk_eq_dim],
+  simp [← (b _).mk_range_eq_dim]
 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.fintype_card]
 
 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_eq_lift_mul, cardinal.fintype_card, cardinal.lift_nat_cast]
+by rw [dim_pi, cardinal.sum_const, cardinal.fintype_card, 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/finsupp_vector_space.lean

@@ -129,10 +129,8 @@ 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 [← cardinal.lift_inj, cardinal.lift_mul, ← bs.mk_eq_dim,
-      ← (finsupp.basis (λa:ι, bs)).mk_eq_dim, ← cardinal.sum_mk,
-      ← cardinal.lift_mul, cardinal.lift_inj],
-  { simp only [cardinal.mk_image_eq (single_injective.{u u} _), cardinal.sum_const] }
+  rw [← bs.mk_eq_dim'', ← (finsupp.basis (λa:ι, bs)).mk_eq_dim'',
+    cardinal.mk_sigma, cardinal.sum_const']
 end
 
 end dim
@@ -149,7 +147,6 @@ variables [add_comm_group V'] [module K V']
 
 open module
 
-
 lemma equiv_of_dim_eq_lift_dim
   (h : cardinal.lift.{w} (module.rank K V) = cardinal.lift.{v} (module.rank K V')) :
   nonempty (V ≃ₗ[K] V') :=

src/linear_algebra/free_module/finite/rank.lean

@@ -60,15 +60,16 @@ by { rw [finrank, rank_finsupp, ← mk_to_nat_eq_card, to_nat_lift] }
 
 /-- The finrank of `(ι → R)` is `fintype.card ι`. -/
 lemma finrank_pi {ι : Type v} [fintype ι] : finrank R (ι → R) = card ι :=
-by { simp [finrank, sum_const_eq_lift_mul] }
+by simp [finrank]
 
 /-- The finrank of the direct sum is the sum of the finranks. -/
 @[simp] lemma finrank_direct_sum  {ι : Type v} [fintype ι] (M : ι → Type w)
   [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [Π (i : ι), module.free R (M i)]
   [Π (i : ι), module.finite R (M i)] : finrank R (⨁ i, M i) = ∑ i, finrank R (M i) :=
 begin
   letI := nontrivial_of_invariant_basis_number R,
-  simp [finrank, λ i, rank_eq_card_choose_basis_index R (M i)],
+  simp only [finrank, λ i, rank_eq_card_choose_basis_index R (M i), rank_direct_sum,
+    ← mk_sigma, mk_to_nat_eq_card, card_sigma],
 end
 
 /-- The finrank of `M × N` is `(finrank R M) + (finrank R N)`. -/
@@ -82,7 +83,8 @@ lemma finrank_pi_fintype {ι : Type v} [fintype ι] {M : ι → Type w}
   [Π (i : ι), module.finite R (M i)] : finrank R (Π i, M i) = ∑ i, finrank R (M i) :=
 begin
   letI := nontrivial_of_invariant_basis_number R,
-  simp [finrank, λ i, rank_eq_card_choose_basis_index R (M i)]
+  simp only [finrank, λ i, rank_eq_card_choose_basis_index R (M i), rank_pi_fintype,
+    ← mk_sigma, mk_to_nat_eq_card, card_sigma],
 end
 
 /-- If `n` and `m` are `fintype`, the finrank of `n × m` matrices is

src/linear_algebra/free_module/rank.lean

@@ -44,10 +44,10 @@ by simpa [lift_id', lift_umax] using
 lemma rank_finsupp' {ι : Type u} : module.rank R (ι →₀ R) = # ι := by simp
 
 /-- The rank of `M × N` is `(module.rank R M).lift + (module.rank R N).lift`. -/
-@[simp] lemma rank_prod : module.rank R (M × N) = lift.{w v} (module.rank R M) +
-  lift.{v w} (module.rank R N) :=
-by simpa [rank_eq_card_choose_basis_index R M, rank_eq_card_choose_basis_index R N, ← add]
-  using ((choose_basis R M).prod (choose_basis R N)).mk_eq_dim.symm
+@[simp] lemma rank_prod :
+  module.rank R (M × N) = lift.{w v} (module.rank R M) + lift.{v w} (module.rank R N) :=
+by simpa [rank_eq_card_choose_basis_index R M, rank_eq_card_choose_basis_index R N,
+  lift_umax, lift_umax'] using ((choose_basis R M).prod (choose_basis R N)).mk_eq_dim.symm
 
 /-- If `M` and `N` lie in the same universe, the rank of `M × N` is
   `(module.rank R M) + (module.rank R N)`. -/
@@ -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''.symm, ← cardinal.sum_mk, λ 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. -/
@@ -75,7 +75,7 @@ by { rw [← (direct_sum.linear_equiv_fun_on_fintype _ _ M).dim_eq, rank_direct_
   module.rank R (matrix n m R) = (lift.{(max v w u) v} (# n)) * (lift.{(max v w u) w} (# m)) :=
 begin
   have h := (matrix.std_basis R n m).mk_eq_dim,
-  rw [← lift_lift.{(max v w u) (max v w)}, lift_inj, mul] at h,
+  rw [← lift_lift.{(max v w u) (max v w)}, lift_inj] at h,
   simpa using h.symm,
 end
 
@@ -107,7 +107,7 @@ begin
 
   have h₁ := linear_equiv.lift_dim_eq (tensor_product.congr (repr R M) (repr R N)),
   let b : basis (ιM × ιN) R (_ →₀ R) := finsupp.basis_single_one,
-  rw [linear_equiv.dim_eq (finsupp_tensor_finsupp' R ιM ιN), ← b.mk_eq_dim, mul] at h₁,
+  rw [linear_equiv.dim_eq (finsupp_tensor_finsupp' R ιM ιN), ← b.mk_eq_dim, mk_prod] at h₁,
   rw [lift_inj.1 h₁, rank_eq_card_choose_basis_index R M, rank_eq_card_choose_basis_index R N],
 end