chore: reorder universe variables in Cardinal.lift_le and `Cardinal…

….lift_mk_le` (#5325)

`Cardinal.lift_le` and `Cardinal.lift_mk_le` have their universes out of order, in the sense that persistently through the rest of the library we need to specify the 2nd universe (resp 3rd), while the others are solved by unification.

This PR reorders the universes so it's easier to specify the thing you need to specify!

(This PR doesn't get rid of all the occurrences of `\.\{_,` in the library, but I'd like to do that later.)

I do have a hidden agenda here, which is that I've been experimenting with solutions to the dreaded "Can't solve `max u v = max v ?u`" universe unification issue (which is making life hellish forward porting leanprover-community/mathlib#19153), and my favourite (but still hacky) solution doesn't like some of the occasions where we reference a lemma filling in some of its universe arguments with `_` but then fully specify a later one. (e.g. `rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{_, _, v}]` in `ModelTheory/Skolem.lean`). Hence the cleanup proposed in this PR makes my life easier working on these experiments. :-)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/LinearAlgebra/Dimension.lean

@@ -621,7 +621,7 @@ theorem Basis.le_span {J : Set M} (v : Basis ι R M) (hJ : span R J = ⊤) : (#r
   haveI := nontrivial_of_invariantBasisNumber R
   cases fintypeOrInfinite 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)
+    convert Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)
     simp
   · let S : J → Set ι := fun j => ↑(v.repr j).support
     let S' : J → Set M := fun j => v '' S j

Mathlib/LinearAlgebra/FiniteDimensional.lean

@@ -276,7 +276,7 @@ theorem basisUnique.repr_eq_zero_iff {ι : Type _} [Unique ι] {h : finrank K V
 
 theorem cardinal_mk_le_finrank_of_linearIndependent [FiniteDimensional K V] {ι : Type w} {b : ι → V}
     (h : LinearIndependent K b) : (#ι) ≤ finrank K V := by
-  rw [← lift_le.{_, max v w}]
+  rw [← lift_le.{max v w}]
   simpa [← finrank_eq_rank', -finrank_eq_rank] using
     cardinal_lift_le_rank_of_linearIndependent h
 #align finite_dimensional.cardinal_mk_le_finrank_of_linear_independent FiniteDimensional.cardinal_mk_le_finrank_of_linearIndependent

Mathlib/ModelTheory/Satisfiability.lean

@@ -185,7 +185,7 @@ theorem exists_large_model_of_infinite_model (T : L.Theory) (κ : Cardinal.{w})
   refine' _root_.trans (lift_le.2 (le_of_eq (Cardinal.mk_out κ).symm)) _
   rw [← mk_univ]
   refine'
-    (card_le_of_model_distinctConstantsTheory L Set.univ N).trans (lift_le.{_, max u v w}.1 _)
+    (card_le_of_model_distinctConstantsTheory L Set.univ N).trans (lift_le.{max u v w}.1 _)
   rw [lift_lift]
 #align first_order.language.Theory.exists_large_model_of_infinite_model FirstOrder.Language.Theory.exists_large_model_of_infinite_model
 
@@ -238,14 +238,14 @@ theorem exists_elementaryEmbedding_card_eq_of_ge (M : Type w') [L.Structure M] [
     (h2 : Cardinal.lift.{w} (#M) ≤ Cardinal.lift.{w'} κ) :
     ∃ N : Bundled L.Structure, Nonempty (M ↪ₑ[L] N) ∧ (#N) = κ := by
   obtain ⟨N0, hN0⟩ := (L.elementaryDiagram M).exists_large_model_of_infinite_model κ M
-  rw [← lift_le.{max w w', max u v}, lift_lift, lift_lift] at h2
+  rw [← lift_le.{max u v}, lift_lift, lift_lift] at h2
   obtain ⟨N, ⟨NN0⟩, hN⟩ :=
     exists_elementaryEmbedding_card_eq_of_le (L[[M]]) N0 κ
       (aleph0_le_lift.1 ((aleph0_le_lift.2 (aleph0_le_mk M)).trans h2))
       (by
         simp only [card_withConstants, lift_add, lift_lift]
         rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]
-        rw [← lift_le.{_, w'}, lift_lift, lift_lift] at h1
+        rw [← lift_le.{w'}, lift_lift, lift_lift] at h1
         exact ⟨h2, h1⟩)
       (hN0.trans (by rw [← lift_umax', lift_id]))
   · letI := (lhomWithConstants L M).reduct N

Mathlib/ModelTheory/Semantics.lean

@@ -1037,7 +1037,7 @@ section Cardinality
 variable (L)
 @[simp]
 theorem Sentence.realize_cardGe (n) : M ⊨ Sentence.cardGe L n ↔ ↑n ≤ (#M) := by
-  rw [← lift_mk_fin, ← lift_le.{w, 0}, lift_lift, lift_mk_le, Sentence.cardGe, Sentence.Realize,
+  rw [← lift_mk_fin, ← lift_le.{0}, lift_lift, lift_mk_le, Sentence.cardGe, Sentence.Realize,
     BoundedFormula.realize_exs]
   simp_rw [BoundedFormula.realize_foldr_inf]
   simp only [Function.comp_apply, List.mem_map, Prod.exists, Ne.def, List.mem_product,

Mathlib/ModelTheory/Skolem.lean

@@ -56,7 +56,7 @@ theorem card_functions_sum_skolem₁ :
   conv_lhs => enter [2, 1, i]; rw [lift_id'.{u, v}]
   rw [add_comm, add_eq_max, max_eq_left]
   · refine' sum_le_sum _ _ fun n => _
-    rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{_, _, v}]
+    rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{v}]
     refine' ⟨⟨fun f => (func f default).bdEqual (func f default), fun f g h => _⟩⟩
     rcases h with ⟨rfl, ⟨rfl⟩⟩
     rfl
@@ -71,7 +71,7 @@ theorem card_functions_sum_skolem₁_le : (#Σn, (L.sum L.skolem₁).Functions n
   · exact
       ⟨⟨Sigma.map Nat.succ fun _ => id,
           Nat.succ_injective.sigma_map fun _ => Function.injective_id⟩⟩
-  · refine' _root_.trans BoundedFormula.card_le (lift_le.{_, max u v}.1 _)
+  · refine' _root_.trans BoundedFormula.card_le (lift_le.{max u v}.1 _)
     simp only [mk_empty, lift_zero, lift_uzero, zero_add]
     rfl
 #align first_order.language.card_functions_sum_skolem₁_le FirstOrder.Language.card_functions_sum_skolem₁_le
@@ -152,11 +152,11 @@ theorem exists_elementarySubstructure_card_eq (s : Set M) (κ : Cardinal.{w'}) (
   refine' ⟨h1, (mk_union_le _ _).trans _, (lift_le.2 card_functions_sum_skolem₁_le).trans _⟩
   · rw [← lift_le, lift_add, h, add_comm, add_eq_max h1]
     exact max_le le_rfl h2
-  · rw [lift_max, lift_aleph0, max_le_iff, aleph0_le_lift, and_comm, ← lift_le.{_, w'},
+  · rw [lift_max, lift_aleph0, max_le_iff, aleph0_le_lift, and_comm, ← lift_le.{w'},
       lift_lift, lift_lift, ← aleph0_le_lift, h]
     refine' ⟨_, h1⟩
     rw [← lift_lift.{w', w}]
-    refine' _root_.trans (lift_le.{_, w}.2 h3) _
+    refine' _root_.trans (lift_le.{w}.2 h3) _
     rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]
   · refine' _root_.trans _ (lift_le.2 (mk_le_mk_of_subset (Set.subset_union_right _ _)))
     rw [aleph0_le_lift, ← aleph0_le_lift, h]

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -300,8 +300,8 @@ theorem out_embedding {c c' : Cardinal} : c ≤ c' ↔ Nonempty (c.out ↪ c'.ou
   · rw [mk'_def, mk'_def, le_def]
 #align cardinal.out_embedding Cardinal.out_embedding
 
-theorem lift_mk_le {α : Type u} {β : Type v} :
-    lift.{max v w} (#α) ≤ lift.{max u w} (#β) ↔ Nonempty (α ↪ β) :=
+theorem lift_mk_le {α : Type v} {β : Type w} :
+    lift.{max u w} (#α) ≤ lift.{max u v} (#β) ↔ Nonempty (α ↪ β) :=
   ⟨fun ⟨f⟩ => ⟨Embedding.congr Equiv.ulift Equiv.ulift f⟩, fun ⟨f⟩ =>
     ⟨Embedding.congr Equiv.ulift.symm Equiv.ulift.symm f⟩⟩
 #align cardinal.lift_mk_le Cardinal.lift_mk_le
@@ -311,7 +311,7 @@ Because Lean often can not realize it should use this specialization itself,
 we provide this statement separately so you don't have to solve the specialization problem either.
 -/
 theorem lift_mk_le' {α : Type u} {β : Type v} : lift.{v} (#α) ≤ lift.{u} (#β) ↔ Nonempty (α ↪ β) :=
-  lift_mk_le.{u, v, 0}
+  lift_mk_le.{0}
 #align cardinal.lift_mk_le' Cardinal.lift_mk_le'
 
 theorem lift_mk_eq {α : Type u} {β : Type v} :
@@ -330,10 +330,10 @@ theorem lift_mk_eq' {α : Type u} {β : Type v} : lift.{v} (#α) = lift.{u} (#β
 #align cardinal.lift_mk_eq' Cardinal.lift_mk_eq'
 
 @[simp]
-theorem lift_le {a b : Cardinal.{u}} : lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b :=
+theorem lift_le {a b : Cardinal.{v}} : lift.{u, v} a ≤ lift.{u, v} b ↔ a ≤ b :=
   inductionOn₂ a b fun α β => by
     rw [← lift_umax]
-    exact lift_mk_le.{u, u, v}
+    exact lift_mk_le.{u}
 #align cardinal.lift_le Cardinal.lift_le
 
 -- Porting note: changed `simps` to `simps!` because the linter told to do so.
@@ -1111,7 +1111,7 @@ theorem lift_iInf {ι} (f : ι → Cardinal) : lift.{u,v} (iInf f) = ⨅ i, lift
 theorem lift_down {a : Cardinal.{u}} {b : Cardinal.{max u v}} :
     b ≤ lift.{v,u} a → ∃ a', lift.{v,u} a' = b :=
   inductionOn₂ a b fun α β => by
-    rw [← lift_id (#β), ← lift_umax, ← lift_umax.{u, v}, lift_mk_le.{_,_,v}]
+    rw [← lift_id (#β), ← lift_umax, ← lift_umax.{u, v}, lift_mk_le.{v}]
     exact fun ⟨f⟩ =>
       ⟨#Set.range f,
         Eq.symm <| lift_mk_eq.{_, _, v}.2
@@ -1406,7 +1406,7 @@ theorem one_le_iff_ne_zero {c : Cardinal} : 1 ≤ c ↔ c ≠ 0 := by
 theorem nat_lt_aleph0 (n : ℕ) : (n : Cardinal.{u}) < ℵ₀ :=
   succ_le_iff.1
     (by
-      rw [← nat_succ, ← lift_mk_fin, aleph0, lift_mk_le.{0, 0, u}]
+      rw [← nat_succ, ← lift_mk_fin, aleph0, lift_mk_le.{u}]
       exact ⟨⟨(↑), fun a b => Fin.ext⟩⟩)
 #align cardinal.nat_lt_aleph_0 Cardinal.nat_lt_aleph0
 
@@ -2001,7 +2001,7 @@ theorem mk_image_le {α β : Type u} {f : α → β} {s : Set α} : (#f '' s) 
 
 theorem mk_image_le_lift {α : Type u} {β : Type v} {f : α → β} {s : Set α} :
     lift.{u} (#f '' s) ≤ lift.{v} (#s) :=
-  lift_mk_le.{v, u, 0}.mpr ⟨Embedding.ofSurjective _ surjective_onto_image⟩
+  lift_mk_le.{0}.mpr ⟨Embedding.ofSurjective _ surjective_onto_image⟩
 #align cardinal.mk_image_le_lift Cardinal.mk_image_le_lift
 
 theorem mk_range_le {α β : Type u} {f : α → β} : (#range f) ≤ (#α) :=
@@ -2010,7 +2010,7 @@ theorem mk_range_le {α β : Type u} {f : α → β} : (#range f) ≤ (#α) :=
 
 theorem mk_range_le_lift {α : Type u} {β : Type v} {f : α → β} :
     lift.{u} (#range f) ≤ lift.{v} (#α) :=
-  lift_mk_le.{v, u, 0}.mpr ⟨Embedding.ofSurjective _ surjective_onto_range⟩
+  lift_mk_le.{0}.mpr ⟨Embedding.ofSurjective _ surjective_onto_range⟩
 #align cardinal.mk_range_le_lift Cardinal.mk_range_le_lift
 
 theorem mk_range_eq (f : α → β) (h : Injective f) : (#range f) = (#α) :=
@@ -2163,15 +2163,15 @@ theorem mk_sep (s : Set α) (t : α → Prop) : (#({ x ∈ s | t x } : Set α))
 
 theorem mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β)
     (h : Injective f) : lift.{v} (#f ⁻¹' s) ≤ lift.{u} (#s) := by
-  rw [lift_mk_le.{u, v, 0}]
+  rw [lift_mk_le.{0}]
   -- Porting note: Needed to insert `mem_preimage.mp` below
   use Subtype.coind (fun x => f x.1) fun x => mem_preimage.mp x.2
   apply Subtype.coind_injective; exact h.comp Subtype.val_injective
 #align cardinal.mk_preimage_of_injective_lift Cardinal.mk_preimage_of_injective_lift
 
 theorem mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β)
     (h : s ⊆ range f) : lift.{u} (#s) ≤ lift.{v} (#f ⁻¹' s) := by
-  rw [lift_mk_le.{v, u, 0}]
+  rw [lift_mk_le.{0}]
   refine' ⟨⟨_, _⟩⟩
   · rintro ⟨y, hy⟩
     rcases Classical.subtype_of_exists (h hy) with ⟨x, rfl⟩

Mathlib/SetTheory/Cardinal/Ordinal.lean

@@ -1041,9 +1041,9 @@ theorem mk_finsupp_lift_of_infinite (α : Type u) (β : Type v) [Infinite α] [Z
 
   · apply max_le <;> rw [← lift_id (#α →₀ β), ← lift_umax]
     · cases' exists_ne (0 : β) with b hb
-      exact lift_mk_le.{u, max u v, v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
+      exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
     · inhabit α
-      exact lift_mk_le.{v, max u v, u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩
+      exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩
 #align cardinal.mk_finsupp_lift_of_infinite Cardinal.mk_finsupp_lift_of_infinite
 
 theorem mk_finsupp_of_infinite (α β : Type u) [Infinite α] [Zero β] [Nontrivial β] :