bump to nightly-2023-03-05-03

mathlib commit leanprover-community/mathlib@641b6a8

Mathbin/Combinatorics/Configuration.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 
 ! This file was ported from Lean 3 source module combinatorics.configuration
-! leanprover-community/mathlib commit 26c71658340519485e2356d20cdca619e1cd4e19
+! leanprover-community/mathlib commit d2d8742b0c21426362a9dacebc6005db895ca963
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -513,7 +513,7 @@ theorem card_points [Fintype P] [Finite L] : Fintype.card P = order P L ^ 2 + or
     have h2 : ∀ l : { l : L // p ∈ l }, Fintype.card { q // q ∈ l.1 ∧ q ≠ p } = order P L :=
       by
       intro l
-      rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter _ _),
+      rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
         Fintype.card_subtype_compl fun 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 _)

Mathbin/Data/List/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.list.defs
-! leanprover-community/mathlib commit 1447cae870f372074e480de1acbeb51de0077698
+! leanprover-community/mathlib commit d2d8742b0c21426362a9dacebc6005db895ca963
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -395,39 +395,45 @@ def andM : List (m Bool) → m Bool :=
 
 end
 
+/- warning: list.foldl_with_index_aux -> List.foldlWithIndexAux is a dubious translation:
+lean 3 declaration is
+  forall {α : Sort.{u1}} {β : Type.{u2}}, (Nat -> α -> β -> α) -> Nat -> α -> (List.{u2} β) -> α
+but is expected to have type
+  forall {α : Sort.{u2}} {β : Type.{u1}}, (Nat -> α -> β -> α) -> Nat -> α -> (List.{u1} β) -> α
+Case conversion may be inaccurate. Consider using '#align list.foldl_with_index_aux List.foldlWithIndexAuxₓ'. -/
 /-- Auxiliary definition for `foldl_with_index`. -/
-def foldlWithIndexAux (f : ℕ → α → β → α) : ℕ → α → List β → α
+def foldlWithIndexAux {α : Sort _} {β : Type _} (f : ℕ → α → β → α) : ℕ → α → List β → α
   | _, a, [] => a
   | i, a, b :: l => foldl_with_index_aux (i + 1) (f i a b) l
 #align list.foldl_with_index_aux List.foldlWithIndexAux
 
 /- warning: list.foldl_with_index -> List.foldlIdx is a dubious translation:
 lean 3 declaration is
-  forall {α : Type.{u1}} {β : Type.{u2}}, (Nat -> α -> β -> α) -> α -> (List.{u2} β) -> α
+  forall {α : Sort.{u1}} {β : Type.{u2}}, (Nat -> α -> β -> α) -> α -> (List.{u2} β) -> α
 but is expected to have type
   forall {α : Sort.{u1}} {β : Type.{u2}}, (Nat -> α -> β -> α) -> α -> (List.{u2} β) -> (optParam.{1} Nat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> α
 Case conversion may be inaccurate. Consider using '#align list.foldl_with_index List.foldlIdxₓ'. -/
 /-- Fold a list from left to right as with `foldl`, but the combining function
 also receives each element's index. -/
-def foldlIdx (f : ℕ → α → β → α) (a : α) (l : List β) : α :=
+def foldlIdx {α : Sort _} {β : Type _} (f : ℕ → α → β → α) (a : α) (l : List β) : α :=
   foldlWithIndexAux f 0 a l
 #align list.foldl_with_index List.foldlIdx
 
 /-- Auxiliary definition for `foldr_with_index`. -/
-def foldrWithIndexAux (f : ℕ → α → β → β) : ℕ → β → List α → β
+def foldrWithIndexAux {α : Type _} {β : Sort _} (f : ℕ → α → β → β) : ℕ → β → List α → β
   | _, b, [] => b
   | i, b, a :: l => f i a (foldr_with_index_aux (i + 1) b l)
 #align list.foldr_with_index_aux List.foldrWithIndexAux
 
 /- warning: list.foldr_with_index -> List.foldrIdx is a dubious translation:
 lean 3 declaration is
-  forall {α : Type.{u1}} {β : Type.{u2}}, (Nat -> α -> β -> β) -> β -> (List.{u1} α) -> β
+  forall {α : Type.{u1}} {β : Sort.{u2}}, (Nat -> α -> β -> β) -> β -> (List.{u1} α) -> β
 but is expected to have type
   forall {α : Type.{u1}} {β : Sort.{u2}}, (Nat -> α -> β -> β) -> β -> (List.{u1} α) -> (optParam.{1} Nat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> β
 Case conversion may be inaccurate. Consider using '#align list.foldr_with_index List.foldrIdxₓ'. -/
 /-- Fold a list from right to left as with `foldr`, but the combining function
 also receives each element's index. -/
-def foldrIdx (f : ℕ → α → β → β) (b : β) (l : List α) : β :=
+def foldrIdx {α : Type _} {β : Sort _} (f : ℕ → α → β → β) (b : β) (l : List α) : β :=
   foldrWithIndexAux f 0 b l
 #align list.foldr_with_index List.foldrIdx
 

Mathbin/Data/List/Indexes.lean

@@ -162,7 +162,7 @@ theorem foldrIdx_eq_foldrIdxSpec (f : ℕ → α → β → β) (start b as) :
 
 /- warning: list.foldr_with_index_eq_foldr_enum -> List.foldrIdx_eq_foldr_enum is a dubious translation:
 lean 3 declaration is
-  forall {α : Type.{u1}} {β : Type.{u2}} (f : Nat -> α -> β -> β) (b : β) (as : List.{u1} α), Eq.{succ u2} β (List.foldrIdx.{u1, u2} α β f b as) (List.foldr.{u1, u2} (Prod.{0, u1} Nat α) β (Function.uncurry.{0, u1, u2} Nat α (β -> β) f) b (List.enum.{u1} α as))
+  forall {α : Type.{u1}} {β : Type.{u2}} (f : Nat -> α -> β -> β) (b : β) (as : List.{u1} α), Eq.{succ u2} β (List.foldrIdx.{u1, succ u2} α β f b as) (List.foldr.{u1, u2} (Prod.{0, u1} Nat α) β (Function.uncurry.{0, u1, u2} Nat α (β -> β) f) b (List.enum.{u1} α as))
 but is expected to have type
   forall {α : Type.{u1}} {β : Type.{u2}} (f : Nat -> α -> β -> β) (b : β) (as : List.{u1} α), Eq.{succ u2} β (List.foldrIdx.{u1, succ u2} α β f b as (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) (List.foldr.{u1, u2} (Prod.{0, u1} Nat α) β (Function.uncurry.{0, u1, u2} Nat α (β -> β) f) b (List.enum.{u1} α as))
 Case conversion may be inaccurate. Consider using '#align list.foldr_with_index_eq_foldr_enum List.foldrIdx_eq_foldr_enumₓ'. -/
@@ -211,7 +211,7 @@ theorem foldlIdx_eq_foldlIdxSpec (f : ℕ → α → β → α) (start a bs) :
 
 /- warning: list.foldl_with_index_eq_foldl_enum -> List.foldlIdx_eq_foldl_enum is a dubious translation:
 lean 3 declaration is
-  forall {α : Type.{u1}} {β : Type.{u2}} (f : Nat -> α -> β -> α) (a : α) (bs : List.{u2} β), Eq.{succ u1} α (List.foldlIdx.{u1, u2} α β f a bs) (List.foldl.{u1, u2} α (Prod.{0, u2} Nat β) (fun (a : α) (p : Prod.{0, u2} Nat β) => f (Prod.fst.{0, u2} Nat β p) a (Prod.snd.{0, u2} Nat β p)) a (List.enum.{u2} β bs))
+  forall {α : Type.{u1}} {β : Type.{u2}} (f : Nat -> α -> β -> α) (a : α) (bs : List.{u2} β), Eq.{succ u1} α (List.foldlIdx.{succ u1, u2} α β f a bs) (List.foldl.{u1, u2} α (Prod.{0, u2} Nat β) (fun (a : α) (p : Prod.{0, u2} Nat β) => f (Prod.fst.{0, u2} Nat β p) a (Prod.snd.{0, u2} Nat β p)) a (List.enum.{u2} β bs))
 but is expected to have type
   forall {α : Type.{u1}} {β : Type.{u2}} (f : Nat -> α -> β -> α) (a : α) (bs : List.{u2} β), Eq.{succ u1} α (List.foldlIdx.{succ u1, u2} α β f a bs (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) (List.foldl.{u1, u2} α (Prod.{0, u2} Nat β) (fun (a : α) (p : Prod.{0, u2} Nat β) => f (Prod.fst.{0, u2} Nat β p) a (Prod.snd.{0, u2} Nat β p)) a (List.enum.{u2} β bs))
 Case conversion may be inaccurate. Consider using '#align list.foldl_with_index_eq_foldl_enum List.foldlIdx_eq_foldl_enumₓ'. -/

Mathbin/Logic/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 
 ! This file was ported from Lean 3 source module logic.basic
-! leanprover-community/mathlib commit 13cd3e89b30352d5b1b7349f5537ea18ba878e40
+! leanprover-community/mathlib commit d2d8742b0c21426362a9dacebc6005db895ca963
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -287,27 +287,19 @@ theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a :=
 #align ne_comm ne_comm
 -/
 
-/- warning: eq_iff_eq_cancel_left -> eq_iff_eq_cancel_left is a dubious translation:
-lean 3 declaration is
-  forall {α : Type.{u1}} {b : α} {c : α}, Iff (forall {a : α}, Iff (Eq.{succ u1} α a b) (Eq.{succ u1} α a c)) (Eq.{succ u1} α b c)
-but is expected to have type
-  forall {α : Sort.{u1}} {b : α} {c : α}, Iff (forall {a : α}, Iff (Eq.{u1} α a b) (Eq.{u1} α a c)) (Eq.{u1} α b c)
-Case conversion may be inaccurate. Consider using '#align eq_iff_eq_cancel_left eq_iff_eq_cancel_leftₓ'. -/
+#print eq_iff_eq_cancel_left /-
 @[simp]
-theorem eq_iff_eq_cancel_left {b c : α} : (∀ {a}, a = b ↔ a = c) ↔ b = c :=
+theorem eq_iff_eq_cancel_left {α : Sort _} {b c : α} : (∀ {a}, a = b ↔ a = c) ↔ b = c :=
   ⟨fun h => by rw [← h], fun h a => by rw [h]⟩
 #align eq_iff_eq_cancel_left eq_iff_eq_cancel_left
+-/
 
-/- warning: eq_iff_eq_cancel_right -> eq_iff_eq_cancel_right is a dubious translation:
-lean 3 declaration is
-  forall {α : Type.{u1}} {a : α} {b : α}, Iff (forall {c : α}, Iff (Eq.{succ u1} α a c) (Eq.{succ u1} α b c)) (Eq.{succ u1} α a b)
-but is expected to have type
-  forall {α : Sort.{u1}} {a : α} {b : α}, Iff (forall {c : α}, Iff (Eq.{u1} α a c) (Eq.{u1} α b c)) (Eq.{u1} α a b)
-Case conversion may be inaccurate. Consider using '#align eq_iff_eq_cancel_right eq_iff_eq_cancel_rightₓ'. -/
+#print eq_iff_eq_cancel_right /-
 @[simp]
-theorem eq_iff_eq_cancel_right {a b : α} : (∀ {c}, a = c ↔ b = c) ↔ a = b :=
+theorem eq_iff_eq_cancel_right {α : Sort _} {a b : α} : (∀ {c}, a = c ↔ b = c) ↔ a = b :=
   ⟨fun h => by rw [h], fun h a => by rw [h]⟩
 #align eq_iff_eq_cancel_right eq_iff_eq_cancel_right
+-/
 
 #print Fact /-
 /- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`out] [] -/

Mathbin/Logic/Equiv/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 
 ! This file was ported from Lean 3 source module logic.equiv.basic
-! leanprover-community/mathlib commit 195fcd60ff2bfe392543bceb0ec2adcdb472db4c
+! leanprover-community/mathlib commit d2d8742b0c21426362a9dacebc6005db895ca963
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1697,47 +1697,35 @@ def subtypeEquivOfSubtype' {p : α → Prop} (e : α ≃ β) :
 #align equiv.subtype_equiv_of_subtype' Equiv.subtypeEquivOfSubtype'
 -/
 
-/- warning: equiv.subtype_equiv_prop -> Equiv.subtypeEquivProp is a dubious translation:
-lean 3 declaration is
-  forall {α : Type.{u1}} {p : α -> Prop} {q : α -> Prop}, (Eq.{succ u1} (α -> Prop) p q) -> (Equiv.{succ u1, succ u1} (Subtype.{succ u1} α p) (Subtype.{succ u1} α q))
-but is expected to have type
-  forall {α : Sort.{u1}} {p : α -> Prop} {q : α -> Prop}, (Eq.{max 1 u1} (α -> Prop) p q) -> (Equiv.{max 1 u1, max 1 u1} (Subtype.{u1} α p) (Subtype.{u1} α q))
-Case conversion may be inaccurate. Consider using '#align equiv.subtype_equiv_prop Equiv.subtypeEquivPropₓ'. -/
+#print Equiv.subtypeEquivProp /-
 /-- If two predicates are equal, then the corresponding subtypes are equivalent. -/
-def subtypeEquivProp {α : Type _} {p q : α → Prop} (h : p = q) : Subtype p ≃ Subtype q :=
+def subtypeEquivProp {α : Sort _} {p q : α → Prop} (h : p = q) : Subtype p ≃ Subtype q :=
   subtypeEquiv (Equiv.refl α) fun a => h ▸ Iff.rfl
 #align equiv.subtype_equiv_prop Equiv.subtypeEquivProp
+-/
 
-/- warning: equiv.subtype_subtype_equiv_subtype_exists -> Equiv.subtypeSubtypeEquivSubtypeExists is a dubious translation:
-lean 3 declaration is
-  forall {α : Type.{u1}} (p : α -> Prop) (q : (Subtype.{succ u1} α p) -> Prop), Equiv.{succ u1, succ u1} (Subtype.{succ u1} (Subtype.{succ u1} α p) q) (Subtype.{succ u1} α (fun (a : α) => Exists.{0} (p a) (fun (h : p a) => q (Subtype.mk.{succ u1} α p a h))))
-but is expected to have type
-  forall {α : Sort.{u1}} (p : α -> Prop) (q : (Subtype.{u1} α p) -> Prop), Equiv.{max 1 u1, max 1 u1} (Subtype.{max 1 u1} (Subtype.{u1} α p) q) (Subtype.{u1} α (fun (a : α) => Exists.{0} (p a) (fun (h : p a) => q (Subtype.mk.{u1} α p a h))))
-Case conversion may be inaccurate. Consider using '#align equiv.subtype_subtype_equiv_subtype_exists Equiv.subtypeSubtypeEquivSubtypeExistsₓ'. -/
+#print Equiv.subtypeSubtypeEquivSubtypeExists /-
 /-- 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 subtypeSubtypeEquivSubtypeExists {α : Type u} (p : α → Prop) (q : Subtype p → Prop) :
+def subtypeSubtypeEquivSubtypeExists {α : Sort u} (p : α → Prop) (q : Subtype p → Prop) :
     Subtype q ≃ { a : α // ∃ h : p a, q ⟨a, h⟩ } :=
   ⟨fun a =>
     ⟨a, a.1.2, by
       rcases a with ⟨⟨a, hap⟩, haq⟩
       exact haq⟩,
     fun a => ⟨⟨a, a.2.fst⟩, a.2.snd⟩, fun ⟨⟨a, ha⟩, h⟩ => rfl, fun ⟨a, h₁, h₂⟩ => rfl⟩
 #align equiv.subtype_subtype_equiv_subtype_exists Equiv.subtypeSubtypeEquivSubtypeExists
+-/
 
-/- warning: equiv.subtype_subtype_equiv_subtype_inter -> Equiv.subtypeSubtypeEquivSubtypeInter is a dubious translation:
-lean 3 declaration is
-  forall {α : Type.{u1}} (p : α -> Prop) (q : α -> Prop), Equiv.{succ u1, succ u1} (Subtype.{succ u1} (Subtype.{succ u1} α p) (fun (x : Subtype.{succ u1} α p) => q (Subtype.val.{succ u1} α p x))) (Subtype.{succ u1} α (fun (x : α) => And (p x) (q x)))
-but is expected to have type
-  forall {α : Sort.{u1}} (p : α -> Prop) (q : α -> Prop), Equiv.{max 1 u1, max 1 u1} (Subtype.{max 1 u1} (Subtype.{u1} α p) (fun (x : Subtype.{u1} α p) => q (Subtype.val.{u1} α p x))) (Subtype.{u1} α (fun (x : α) => And (p x) (q x)))
-Case conversion may be inaccurate. Consider using '#align equiv.subtype_subtype_equiv_subtype_inter Equiv.subtypeSubtypeEquivSubtypeInterₓ'. -/
+#print Equiv.subtypeSubtypeEquivSubtypeInter /-
 /-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. -/
 @[simps]
-def subtypeSubtypeEquivSubtypeInter {α : Type u} (p q : α → Prop) :
+def subtypeSubtypeEquivSubtypeInter {α : Sort u} (p q : α → Prop) :
     { x : Subtype p // q x.1 } ≃ Subtype fun x => p x ∧ q x :=
   (subtypeSubtypeEquivSubtypeExists p _).trans <| subtypeEquivRight fun x => exists_prop
 #align equiv.subtype_subtype_equiv_subtype_inter Equiv.subtypeSubtypeEquivSubtypeInter
+-/
 
 /- warning: equiv.subtype_subtype_equiv_subtype -> Equiv.subtypeSubtypeEquivSubtype is a dubious translation:
 lean 3 declaration is
@@ -2504,11 +2492,11 @@ theorem PLift.eq_up_iff_down_eq {x : PLift α} {y : α} : x = PLift.up y ↔ x.d
 
 /- warning: function.injective.map_swap -> Function.Injective.map_swap is a dubious translation:
 lean 3 declaration is
-  forall {α : Type.{u1}} {β : Type.{u2}} [_inst_1 : DecidableEq.{succ u1} α] [_inst_2 : DecidableEq.{succ u2} β] {f : α -> β}, (Function.Injective.{succ u1, succ u2} α β f) -> (forall (x : α) (y : α) (z : α), Eq.{succ u2} β (f (coeFn.{succ u1, succ u1} (Equiv.Perm.{succ u1} α) (fun (_x : Equiv.{succ u1, succ u1} α α) => α -> α) (Equiv.hasCoeToFun.{succ u1, succ u1} α α) (Equiv.swap.{succ u1} α (fun (a : α) (b : α) => _inst_1 a b) x y) z)) (coeFn.{succ u2, succ u2} (Equiv.Perm.{succ u2} β) (fun (_x : Equiv.{succ u2, succ u2} β β) => β -> β) (Equiv.hasCoeToFun.{succ u2, succ u2} β β) (Equiv.swap.{succ u2} β (fun (a : β) (b : β) => _inst_2 a b) (f x) (f y)) (f z)))
+  forall {α : Sort.{u1}} {β : Sort.{u2}} [_inst_1 : DecidableEq.{u1} α] [_inst_2 : DecidableEq.{u2} β] {f : α -> β}, (Function.Injective.{u1, u2} α β f) -> (forall (x : α) (y : α) (z : α), Eq.{u2} β (f (coeFn.{max 1 u1, u1} (Equiv.Perm.{u1} α) (fun (_x : Equiv.{u1, u1} α α) => α -> α) (Equiv.hasCoeToFun.{u1, u1} α α) (Equiv.swap.{u1} α (fun (a : α) (b : α) => _inst_1 a b) x y) z)) (coeFn.{max 1 u2, u2} (Equiv.Perm.{u2} β) (fun (_x : Equiv.{u2, u2} β β) => β -> β) (Equiv.hasCoeToFun.{u2, u2} β β) (Equiv.swap.{u2} β (fun (a : β) (b : β) => _inst_2 a b) (f x) (f y)) (f z)))
 but is expected to have type
   forall {α : Sort.{u2}} {β : Sort.{u1}} [_inst_1 : DecidableEq.{u2} α] [_inst_2 : DecidableEq.{u1} β] {f : α -> β}, (Function.Injective.{u2, u1} α β f) -> (forall (x : α) (y : α) (z : α), Eq.{u1} β (f (FunLike.coe.{max 1 u2, u2, u2} (Equiv.Perm.{u2} α) α (fun (_x : α) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : α) => α) _x) (Equiv.instFunLikeEquiv.{u2, u2} α α) (Equiv.swap.{u2} α (fun (a : α) (b : α) => _inst_1 a b) x y) z)) (FunLike.coe.{max 1 u1, u1, u1} (Equiv.Perm.{u1} β) β (fun (_x : β) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : β) => β) _x) (Equiv.instFunLikeEquiv.{u1, u1} β β) (Equiv.swap.{u1} β (fun (a : β) (b : β) => _inst_2 a b) (f x) (f y)) (f z)))
 Case conversion may be inaccurate. Consider using '#align function.injective.map_swap Function.Injective.map_swapₓ'. -/
-theorem Function.Injective.map_swap {α β : Type _} [DecidableEq α] [DecidableEq β] {f : α → β}
+theorem Function.Injective.map_swap {α β : Sort _} [DecidableEq α] [DecidableEq β] {f : α → β}
     (hf : Function.Injective f) (x y z : α) : f (Equiv.swap x y z) = Equiv.swap (f x) (f y) (f z) :=
   by
   conv_rhs => rw [Equiv.swap_apply_def]

Mathbin/Logic/Nonempty.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module logic.nonempty
-! leanprover-community/mathlib commit 448144f7ae193a8990cb7473c9e9a01990f64ac7
+! leanprover-community/mathlib commit d2d8742b0c21426362a9dacebc6005db895ca963
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -262,16 +262,12 @@ theorem subsingleton_of_not_nonempty {α : Sort _} (h : ¬Nonempty α) : Subsing
 #align subsingleton_of_not_nonempty subsingleton_of_not_nonempty
 -/
 
-/- warning: function.surjective.nonempty -> Function.Surjective.nonempty is a dubious translation:
-lean 3 declaration is
-  forall {α : Type.{u1}} {β : Type.{u2}} [h : Nonempty.{succ u2} β] {f : α -> β}, (Function.Surjective.{succ u1, succ u2} α β f) -> (Nonempty.{succ u1} α)
-but is expected to have type
-  forall {α : Sort.{u1}} {β : Sort.{u2}} [h : Nonempty.{u2} β] {f : α -> β}, (Function.Surjective.{u1, u2} α β f) -> (Nonempty.{u1} α)
-Case conversion may be inaccurate. Consider using '#align function.surjective.nonempty Function.Surjective.nonemptyₓ'. -/
-theorem Function.Surjective.nonempty [h : Nonempty β] {f : α → β} (hf : Function.Surjective f) :
-    Nonempty α :=
+#print Function.Surjective.nonempty /-
+theorem Function.Surjective.nonempty {α β : Sort _} [h : Nonempty β] {f : α → β}
+    (hf : Function.Surjective f) : Nonempty α :=
   let ⟨y⟩ := h
   let ⟨x, hx⟩ := hf y
   ⟨x⟩
 #align function.surjective.nonempty Function.Surjective.nonempty
+-/