From 265ba8e6e5a47b06f7cf08761518b97b2d7b9e3b Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 21 Jun 2023 05:36:50 +0000 Subject: [PATCH] chore: reorder universe variables in `Cardinal.lift_le` and `Cardinal.lift_mk_le` (#5325) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 https://github.com/leanprover-community/mathlib/pull/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 --- Mathlib/LinearAlgebra/Dimension.lean | 2 +- Mathlib/LinearAlgebra/FiniteDimensional.lean | 2 +- Mathlib/ModelTheory/Satisfiability.lean | 6 +++--- Mathlib/ModelTheory/Semantics.lean | 2 +- Mathlib/ModelTheory/Skolem.lean | 8 +++---- Mathlib/SetTheory/Cardinal/Basic.lean | 22 ++++++++++---------- Mathlib/SetTheory/Cardinal/Ordinal.lean | 4 ++-- 7 files changed, 23 insertions(+), 23 deletions(-) diff --git a/Mathlib/LinearAlgebra/Dimension.lean b/Mathlib/LinearAlgebra/Dimension.lean index 4bc9b33f12ff9..de76acf785551 100644 --- a/Mathlib/LinearAlgebra/Dimension.lean +++ b/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 diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean index 8f37213085982..ae0822321f430 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional.lean +++ b/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 diff --git a/Mathlib/ModelTheory/Satisfiability.lean b/Mathlib/ModelTheory/Satisfiability.lean index 1d8919977e619..4f0841d383509 100644 --- a/Mathlib/ModelTheory/Satisfiability.lean +++ b/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 diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean index 4563a1b2918e2..6f6eb540ab821 100644 --- a/Mathlib/ModelTheory/Semantics.lean +++ b/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, diff --git a/Mathlib/ModelTheory/Skolem.lean b/Mathlib/ModelTheory/Skolem.lean index f5f8b409b7f88..208cf82cc448c 100644 --- a/Mathlib/ModelTheory/Skolem.lean +++ b/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] diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 3f55e2fccfe86..65c2f42469980 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/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,7 +2163,7 @@ 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 @@ -2171,7 +2171,7 @@ theorem mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β 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⟩ diff --git a/Mathlib/SetTheory/Cardinal/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Ordinal.lean index 8b75c316a4035..c170d9e14cf2a 100644 --- a/Mathlib/SetTheory/Cardinal/Ordinal.lean +++ b/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 β] :