chore(logic/equiv/basic): Generalize Type to Sort (#18543)

eric-wieser · eric-wieser · commit d2d8742b0c21 · 2023-03-03T19:01:42.000Z
This backports a change that was already made in mathlib4. Indeed, mathport complains that the change was made, see the comments in https://github.com/leanprover-community/mathlib3port/blob/e3a205b1f51e409563e9e4294f41dd4df61f578a/Mathbin/Logic/Equiv/Basic.lean#L1729-L1735 By backporting this, we can deal with the fallout up-front rather than during porting.
diff --git a/src/combinatorics/configuration.lean b/src/combinatorics/configuration.lean
@@ -437,7 +437,7 @@ begin
     convert (fintype.card_subtype_compl _).trans (congr_arg _ (fintype.card_subtype_eq p)) },
   have h2 : ∀ l : {l : L // p ∈ l}, fintype.card {q // q ∈ l.1 ∧ q ≠ p} = order P L,
   { intro l,
-    rw [←fintype.card_congr (equiv.subtype_subtype_equiv_subtype_inter _ _),
+    rw [←fintype.card_congr (equiv.subtype_subtype_equiv_subtype_inter (∈ l.val) (≠ p)),
       fintype.card_subtype_compl (λ (x : subtype (∈ l.val)), x.val = p), ←nat.card_eq_fintype_card],
     refine tsub_eq_of_eq_add ((point_count_eq P l.1).trans _),
     rw ← fintype.card_subtype_eq (⟨p, l.2⟩ : {q : P // q ∈ l.1}),
diff --git a/src/data/list/defs.lean b/src/data/list/defs.lean
@@ -246,23 +246,23 @@ mall id
 end
 
 /-- Auxiliary definition for `foldl_with_index`. -/
-def foldl_with_index_aux (f : ℕ → α → β → α) : ℕ → α → list β → α
+def foldl_with_index_aux {α : Sort*} {β : Type*} (f : ℕ → α → β → α) : ℕ → α → list β → α
 | _ a [] := a
 | i a (b :: l) := foldl_with_index_aux (i + 1) (f i a b) l
 
 /-- Fold a list from left to right as with `foldl`, but the combining function
 also receives each element's index. -/
-def foldl_with_index (f : ℕ → α → β → α) (a : α) (l : list β) : α :=
+def foldl_with_index {α : Sort*} {β : Type*} (f : ℕ → α → β → α) (a : α) (l : list β) : α :=
 foldl_with_index_aux f 0 a l
 
 /-- Auxiliary definition for `foldr_with_index`. -/
-def foldr_with_index_aux (f : ℕ → α → β → β) : ℕ → β → list α → β
+def foldr_with_index_aux {α : Type*} {β : Sort*} (f : ℕ → α → β → β) : ℕ → β → list α → β
 | _ b [] := b
 | i b (a :: l) := f i a (foldr_with_index_aux (i + 1) b l)
 
 /-- Fold a list from right to left as with `foldr`, but the combining function
 also receives each element's index. -/
-def foldr_with_index (f : ℕ → α → β → β) (b : β) (l : list α) : β :=
+def foldr_with_index {α : Type*} {β : Sort*} (f : ℕ → α → β → β) (b : β) (l : list α) : β :=
 foldr_with_index_aux f 0 b l
 
 /-- `find_indexes p l` is the list of indexes of elements of `l` that satisfy `p`. -/
diff --git a/src/logic/basic.lean b/src/logic/basic.lean
@@ -177,11 +177,11 @@ attribute [symm] ne.symm
 
 lemma ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨ne.symm, ne.symm⟩
 
-@[simp] lemma eq_iff_eq_cancel_left {b c : α} :
+@[simp] lemma eq_iff_eq_cancel_left {α : Sort*} {b c : α} :
   (∀ {a}, a = b ↔ a = c) ↔ (b = c) :=
 ⟨λ h, by rw [← h], λ h a, by rw h⟩
 
-@[simp] lemma eq_iff_eq_cancel_right {a b : α} :
+@[simp] lemma eq_iff_eq_cancel_right {α : Sort*} {a b : α} :
   (∀ {c}, a = c ↔ b = c) ↔ (a = b) :=
 ⟨λ h, by rw h, λ h a, by rw h⟩
 
diff --git a/src/logic/equiv/basic.lean b/src/logic/equiv/basic.lean
@@ -811,20 +811,20 @@ def subtype_equiv_of_subtype' {p : α → Prop} (e : α ≃ β) :
 e.symm.subtype_equiv_of_subtype.symm
 
 /-- If two predicates are equal, then the corresponding subtypes are equivalent. -/
-def subtype_equiv_prop {α : Type*} {p q : α → Prop} (h : p = q) : subtype p ≃ subtype q :=
+def subtype_equiv_prop {α : Sort*} {p q : α → Prop} (h : p = q) : subtype p ≃ subtype q :=
 subtype_equiv (equiv.refl α) (assume a, h ▸ iff.rfl)
 
 /-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This
 version allows the “inner” predicate to depend on `h : p a`. -/
 @[simps]
-def subtype_subtype_equiv_subtype_exists {α : Type u} (p : α → Prop) (q : subtype p → Prop) :
+def subtype_subtype_equiv_subtype_exists {α : Sort u} (p : α → Prop) (q : subtype p → Prop) :
   subtype q ≃ {a : α // ∃h:p a, q ⟨a, h⟩ } :=
 ⟨λ a, ⟨a, a.1.2, by { rcases a with ⟨⟨a, hap⟩, haq⟩, exact haq }⟩,
   λ a, ⟨⟨a, a.2.fst⟩, a.2.snd⟩,
   assume ⟨⟨a, ha⟩, h⟩, rfl, assume ⟨a, h₁, h₂⟩, rfl⟩
 
 /-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. -/
-@[simps] def subtype_subtype_equiv_subtype_inter {α : Type u} (p q : α → Prop) :
+@[simps] def subtype_subtype_equiv_subtype_inter {α : Sort u} (p q : α → Prop) :
   {x : subtype p // q x.1} ≃ subtype (λ x, p x ∧ q x) :=
 (subtype_subtype_equiv_subtype_exists p _).trans $
 subtype_equiv_right $ λ x, exists_prop
@@ -1249,7 +1249,7 @@ end function.involutive
 lemma plift.eq_up_iff_down_eq {x : plift α} {y : α} : x = plift.up y ↔ x.down = y :=
 equiv.plift.eq_symm_apply
 
-lemma function.injective.map_swap {α β : Type*} [decidable_eq α] [decidable_eq β]
+lemma function.injective.map_swap {α β : Sort*} [decidable_eq α] [decidable_eq β]
   {f : α → β} (hf : function.injective f) (x y z : α) :
   f (equiv.swap x y z) = equiv.swap (f x) (f y) (f z) :=
 begin
diff --git a/src/logic/nonempty.lean b/src/logic/nonempty.lean
@@ -121,6 +121,7 @@ lemma classical.nonempty_pi {ι} {α : ι → Sort*} : nonempty (Π i, α i) ↔
 lemma subsingleton_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : subsingleton α :=
 ⟨λ x, false.elim $ not_nonempty_iff_imp_false.mp h x⟩
 
-lemma function.surjective.nonempty [h : nonempty β] {f : α → β} (hf : function.surjective f) :
+lemma function.surjective.nonempty {α β : Sort*} [h : nonempty β] {f : α → β}
+  (hf : function.surjective f) :
   nonempty α :=
 let ⟨y⟩ := h, ⟨x, hx⟩ := hf y in ⟨x⟩
