feat: change Type to Sort in Algebra/Classes, fix some priorities (#…

…10354)

Mathlib/Data/Nat/Cast/Defs.lean

@@ -58,7 +58,7 @@ instance is what makes things like `37 : R` type check.  Note that `0` and `1` a
 because they are recognized as terms of `R` (at least when `R` is an `AddMonoidWithOne`) through
 `Zero` and `One`, respectively. -/
 @[nolint unusedArguments]
-instance instOfNatAtLeastTwo [NatCast R] [Nat.AtLeastTwo n] : OfNat R n where
+instance (priority := 100) instOfNatAtLeastTwo [NatCast R] [Nat.AtLeastTwo n] : OfNat R n where
   ofNat := n.cast
 
 library_note "no_index around OfNat.ofNat"

Mathlib/Init/Algebra/Classes.lean

@@ -67,219 +67,219 @@ set_option autoImplicit true
 universe u v
 
 -- porting note: removed `outParam`
-class IsSymmOp (α : Type u) (β : Type v) (op : α → α → β) : Prop where
+class IsSymmOp (α : Sort u) (β : Sort v) (op : α → α → β) : Prop where
   symm_op : ∀ a b, op a b = op b a
 #align is_symm_op IsSymmOp
 
 /-- A commutative binary operation. -/
 @[deprecated IsCommutative]
-abbrev IsCommutative (α : Type u) (op : α → α → α) := Std.Commutative op
+abbrev IsCommutative (α : Sort u) (op : α → α → α) := Std.Commutative op
 #align is_commutative IsCommutative
 
-instance (priority := 100) isSymmOp_of_isCommutative (α : Type u) (op : α → α → α)
+instance (priority := 100) isSymmOp_of_isCommutative (α : Sort u) (op : α → α → α)
     [Std.Commutative op] : IsSymmOp α α op where symm_op := Std.Commutative.comm
 #align is_symm_op_of_is_commutative isSymmOp_of_isCommutative
 
 /-- An associative binary operation. -/
 @[deprecated IsAssociative]
-abbrev IsAssociative (α : Type u) (op : α → α → α) := Std.Associative op
+abbrev IsAssociative (α : Sort u) (op : α → α → α) := Std.Associative op
 
 /-- A binary operation with a left identity. -/
 @[deprecated IsLeftId]
-abbrev IsLeftId (α : Type u) (op : α → α → α) (o : outParam α) := Std.LawfulLeftIdentity op o
+abbrev IsLeftId (α : Sort u) (op : α → α → α) (o : outParam α) := Std.LawfulLeftIdentity op o
 #align is_left_id Std.LawfulLeftIdentity
 
 /-- A binary operation with a right identity. -/
 @[deprecated IsRightId]
-abbrev IsRightId (α : Type u) (op : α → α → α) (o : outParam α) := Std.LawfulRightIdentity op o
+abbrev IsRightId (α : Sort u) (op : α → α → α) (o : outParam α) := Std.LawfulRightIdentity op o
 #align is_right_id Std.LawfulRightIdentity
 
--- class IsLeftNull (α : Type u) (op : α → α → α) (o : outParam α) : Prop where
+-- class IsLeftNull (α : Sort u) (op : α → α → α) (o : outParam α) : Prop where
 --   left_null : ∀ a, op o a = o
 #noalign is_left_null -- IsLeftNull
 
--- class IsRightNull (α : Type u) (op : α → α → α) (o : outParam α) : Prop where
+-- class IsRightNull (α : Sort u) (op : α → α → α) (o : outParam α) : Prop where
 --   right_null : ∀ a, op a o = o
 #noalign is_right_null -- IsRightNull
 
-class IsLeftCancel (α : Type u) (op : α → α → α) : Prop where
+class IsLeftCancel (α : Sort u) (op : α → α → α) : Prop where
   left_cancel : ∀ a b c, op a b = op a c → b = c
 #align is_left_cancel IsLeftCancel
 
-class IsRightCancel (α : Type u) (op : α → α → α) : Prop where
+class IsRightCancel (α : Sort u) (op : α → α → α) : Prop where
   right_cancel : ∀ a b c, op a b = op c b → a = c
 #align is_right_cancel IsRightCancel
 
 @[deprecated IsIdempotent]
-abbrev IsIdempotent (α : Type u) (op : α → α → α) := Std.IdempotentOp op
+abbrev IsIdempotent (α : Sort u) (op : α → α → α) := Std.IdempotentOp op
 #align is_idempotent Std.IdempotentOp
 
--- class IsLeftDistrib (α : Type u) (op₁ : α → α → α) (op₂ : outParam <| α → α → α) : Prop where
+-- class IsLeftDistrib (α : Sort u) (op₁ : α → α → α) (op₂ : outParam <| α → α → α) : Prop where
 --   left_distrib : ∀ a b c, op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c)
 #noalign is_left_distrib -- IsLeftDistrib
 
--- class IsRightDistrib (α : Type u) (op₁ : α → α → α) (op₂ : outParam <| α → α → α) : Prop where
+-- class IsRightDistrib (α : Sort u) (op₁ : α → α → α) (op₂ : outParam <| α → α → α) : Prop where
 --   right_distrib : ∀ a b c, op₁ (op₂ a b) c = op₂ (op₁ a c) (op₁ b c)
 #noalign is_right_distrib -- IsRightDistrib
 
--- class IsLeftInv (α : Type u) (op : α → α → α) (inv : outParam <| α → α) (o : outParam α) :
+-- class IsLeftInv (α : Sort u) (op : α → α → α) (inv : outParam <| α → α) (o : outParam α) :
 --     Prop where
 --   left_inv : ∀ a, op (inv a) a = o
 #noalign is_left_inv -- IsLeftInv
 
--- class IsRightInv (α : Type u) (op : α → α → α) (inv : outParam <| α → α) (o : outParam α) :
+-- class IsRightInv (α : Sort u) (op : α → α → α) (inv : outParam <| α → α) (o : outParam α) :
 --     Prop where
 --   right_inv : ∀ a, op a (inv a) = o
 #noalign is_right_inv -- IsRightInv
 
--- class IsCondLeftInv (α : Type u) (op : α → α → α) (inv : outParam <| α → α) (o : outParam α)
+-- class IsCondLeftInv (α : Sort u) (op : α → α → α) (inv : outParam <| α → α) (o : outParam α)
 --     (p : outParam <| α → Prop) : Prop where
 --   left_inv : ∀ a, p a → op (inv a) a = o
 #noalign is_cond_left_inv -- IsCondLeftInv
 
--- class IsCondRightInv (α : Type u) (op : α → α → α) (inv : outParam <| α → α) (o : outParam α)
+-- class IsCondRightInv (α : Sort u) (op : α → α → α) (inv : outParam <| α → α) (o : outParam α)
 --     (p : outParam <| α → Prop) : Prop where
 --   right_inv : ∀ a, p a → op a (inv a) = o
 #noalign is_cond_right_inv -- IsCondRightInv
 
--- class IsDistinct (α : Type u) (a : α) (b : α) : Prop where
+-- class IsDistinct (α : Sort u) (a : α) (b : α) : Prop where
 --   distinct : a ≠ b
 #noalign is_distinct -- IsDistinct
 
 /-
 -- The following type class doesn't seem very useful, a regular simp lemma should work for this.
-class is_inv (α : Type u) (β : Type v) (f : α → β) (g : out β → α) : Prop :=
+class is_inv (α : Sort u) (β : Sort v) (f : α → β) (g : out β → α) : Prop :=
 (inv : ∀ a, g (f a) = a)
 
 -- The following one can also be handled using a regular simp lemma
-class is_idempotent (α : Type u) (f : α → α) : Prop :=
+class is_idempotent (α : Sort u) (f : α → α) : Prop :=
 (idempotent : ∀ a, f (f a) = f a)
 -/
 
 /-- `IsIrrefl X r` means the binary relation `r` on `X` is irreflexive (that is, `r x x` never
 holds). -/
-class IsIrrefl (α : Type u) (r : α → α → Prop) : Prop where
+class IsIrrefl (α : Sort u) (r : α → α → Prop) : Prop where
   irrefl : ∀ a, ¬r a a
 #align is_irrefl IsIrrefl
 
 /-- `IsRefl X r` means the binary relation `r` on `X` is reflexive. -/
-class IsRefl (α : Type u) (r : α → α → Prop) : Prop where
+class IsRefl (α : Sort u) (r : α → α → Prop) : Prop where
   refl : ∀ a, r a a
 #align is_refl IsRefl
 
 /-- `IsSymm X r` means the binary relation `r` on `X` is symmetric. -/
-class IsSymm (α : Type u) (r : α → α → Prop) : Prop where
+class IsSymm (α : Sort u) (r : α → α → Prop) : Prop where
   symm : ∀ a b, r a b → r b a
 #align is_symm IsSymm
 
 /-- The opposite of a symmetric relation is symmetric. -/
-instance (priority := 100) isSymmOp_of_isSymm (α : Type u) (r : α → α → Prop) [IsSymm α r] :
+instance (priority := 100) isSymmOp_of_isSymm (α : Sort u) (r : α → α → Prop) [IsSymm α r] :
     IsSymmOp α Prop r where symm_op a b := propext <| Iff.intro (IsSymm.symm a b) (IsSymm.symm b a)
 #align is_symm_op_of_is_symm isSymmOp_of_isSymm
 
 /-- `IsAsymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
 `r a b → ¬ r b a`. -/
-class IsAsymm (α : Type u) (r : α → α → Prop) : Prop where
+class IsAsymm (α : Sort u) (r : α → α → Prop) : Prop where
   asymm : ∀ a b, r a b → ¬r b a
 #align is_asymm IsAsymm
 
 /-- `IsAntisymm X r` means the binary relation `r` on `X` is antisymmetric. -/
-class IsAntisymm (α : Type u) (r : α → α → Prop) : Prop where
+class IsAntisymm (α : Sort u) (r : α → α → Prop) : Prop where
   antisymm : ∀ a b, r a b → r b a → a = b
 #align is_antisymm IsAntisymm
 
 /-- `IsTrans X r` means the binary relation `r` on `X` is transitive. -/
-class IsTrans (α : Type u) (r : α → α → Prop) : Prop where
+class IsTrans (α : Sort u) (r : α → α → Prop) : Prop where
   trans : ∀ a b c, r a b → r b c → r a c
 #align is_trans IsTrans
 
-instance {α : Type u} {r : α → α → Prop} [IsTrans α r] : Trans r r r :=
+instance {α : Sort u} {r : α → α → Prop} [IsTrans α r] : Trans r r r :=
   ⟨IsTrans.trans _ _ _⟩
 
-instance {α : Type u} {r : α → α → Prop} [Trans r r r] : IsTrans α r :=
+instance (priority := 100) {α : Sort u} {r : α → α → Prop} [Trans r r r] : IsTrans α r :=
   ⟨fun _ _ _ => Trans.trans⟩
 
 /-- `IsTotal X r` means that the binary relation `r` on `X` is total, that is, that for any
 `x y : X` we have `r x y` or `r y x`.-/
-class IsTotal (α : Type u) (r : α → α → Prop) : Prop where
+class IsTotal (α : Sort u) (r : α → α → Prop) : Prop where
   total : ∀ a b, r a b ∨ r b a
 #align is_total IsTotal
 
 /-- `IsPreorder X r` means that the binary relation `r` on `X` is a pre-order, that is, reflexive
 and transitive. -/
-class IsPreorder (α : Type u) (r : α → α → Prop) extends IsRefl α r, IsTrans α r : Prop
+class IsPreorder (α : Sort u) (r : α → α → Prop) extends IsRefl α r, IsTrans α r : Prop
 #align is_preorder IsPreorder
 
 /-- `IsTotalPreorder X r` means that the binary relation `r` on `X` is total and a preorder. -/
-class IsTotalPreorder (α : Type u) (r : α → α → Prop) extends IsTrans α r, IsTotal α r : Prop
+class IsTotalPreorder (α : Sort u) (r : α → α → Prop) extends IsTrans α r, IsTotal α r : Prop
 #align is_total_preorder IsTotalPreorder
 
 /-- Every total pre-order is a pre-order. -/
-instance isTotalPreorder_isPreorder (α : Type u) (r : α → α → Prop) [s : IsTotalPreorder α r] :
-    IsPreorder α r where
+instance (priority := 100) isTotalPreorder_isPreorder (α : Sort u) (r : α → α → Prop)
+    [s : IsTotalPreorder α r] : IsPreorder α r where
   trans := s.trans
   refl a := Or.elim (@IsTotal.total _ r _ a a) id id
 #align is_total_preorder_is_preorder isTotalPreorder_isPreorder
 
 /-- `IsPartialOrder X r` means that the binary relation `r` on `X` is a partial order, that is,
 `IsPreorder X r` and `IsAntisymm X r`. -/
-class IsPartialOrder (α : Type u) (r : α → α → Prop) extends IsPreorder α r, IsAntisymm α r : Prop
+class IsPartialOrder (α : Sort u) (r : α → α → Prop) extends IsPreorder α r, IsAntisymm α r : Prop
 #align is_partial_order IsPartialOrder
 
 /-- `IsLinearOrder X r` means that the binary relation `r` on `X` is a linear order, that is,
 `IsPartialOrder X r` and `IsTotal X r`. -/
-class IsLinearOrder (α : Type u) (r : α → α → Prop) extends IsPartialOrder α r, IsTotal α r : Prop
+class IsLinearOrder (α : Sort u) (r : α → α → Prop) extends IsPartialOrder α r, IsTotal α r : Prop
 #align is_linear_order IsLinearOrder
 
 /-- `IsEquiv X r` means that the binary relation `r` on `X` is an equivalence relation, that
 is, `IsPreorder X r` and `IsSymm X r`. -/
-class IsEquiv (α : Type u) (r : α → α → Prop) extends IsPreorder α r, IsSymm α r : Prop
+class IsEquiv (α : Sort u) (r : α → α → Prop) extends IsPreorder α r, IsSymm α r : Prop
 #align is_equiv IsEquiv
 
 -- /-- `IsPer X r` means that the binary relation `r` on `X` is a partial equivalence relation, that
 -- is, `IsSymm X r` and `IsTrans X r`. -/
--- class IsPer (α : Type u) (r : α → α → Prop) extends IsSymm α r, IsTrans α r : Prop
+-- class IsPer (α : Sort u) (r : α → α → Prop) extends IsSymm α r, IsTrans α r : Prop
 #noalign is_per -- IsPer
 
 /-- `IsStrictOrder X r` means that the binary relation `r` on `X` is a strict order, that is,
 `IsIrrefl X r` and `IsTrans X r`. -/
-class IsStrictOrder (α : Type u) (r : α → α → Prop) extends IsIrrefl α r, IsTrans α r : Prop
+class IsStrictOrder (α : Sort u) (r : α → α → Prop) extends IsIrrefl α r, IsTrans α r : Prop
 #align is_strict_order IsStrictOrder
 
 /-- `IsIncompTrans X lt` means that for `lt` a binary relation on `X`, the incomparable relation
 `fun a b => ¬ lt a b ∧ ¬ lt b a` is transitive. -/
-class IsIncompTrans (α : Type u) (lt : α → α → Prop) : Prop where
+class IsIncompTrans (α : Sort u) (lt : α → α → Prop) : Prop where
   incomp_trans : ∀ a b c, ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a
 #align is_incomp_trans IsIncompTrans
 
 /-- `IsStrictWeakOrder X lt` means that the binary relation `lt` on `X` is a strict weak order,
 that is, `IsStrictOrder X lt` and `IsIncompTrans X lt`. -/
-class IsStrictWeakOrder (α : Type u) (lt : α → α → Prop) extends IsStrictOrder α lt,
+class IsStrictWeakOrder (α : Sort u) (lt : α → α → Prop) extends IsStrictOrder α lt,
     IsIncompTrans α lt : Prop
 #align is_strict_weak_order IsStrictWeakOrder
 
 /-- `IsTrichotomous X lt` means that the binary relation `lt` on `X` is trichotomous, that is,
 either `lt a b` or `a = b` or `lt b a` for any `a` and `b`. -/
-class IsTrichotomous (α : Type u) (lt : α → α → Prop) : Prop where
+class IsTrichotomous (α : Sort u) (lt : α → α → Prop) : Prop where
   trichotomous : ∀ a b, lt a b ∨ a = b ∨ lt b a
 #align is_trichotomous IsTrichotomous
 
 /-- `IsStrictTotalOrder X lt` means that the binary relation `lt` on `X` is a strict total order,
 that is, `IsTrichotomous X lt` and `IsStrictOrder X lt`. -/
-class IsStrictTotalOrder (α : Type u) (lt : α → α → Prop) extends IsTrichotomous α lt,
+class IsStrictTotalOrder (α : Sort u) (lt : α → α → Prop) extends IsTrichotomous α lt,
     IsStrictOrder α lt : Prop
 #align is_strict_total_order IsStrictTotalOrder
 
 /-- Equality is an equivalence relation. -/
-instance eq_isEquiv (α : Type u) : IsEquiv α (· = ·) where
+instance eq_isEquiv (α : Sort u) : IsEquiv α (· = ·) where
   symm := @Eq.symm _
   trans := @Eq.trans _
   refl := Eq.refl
 #align eq_is_equiv eq_isEquiv
 
 section
 
-variable {α : Type u} {r : α → α → Prop}
+variable {α : Sort u} {r : α → α → Prop}
 
 local infixl:50 " ≺ " => r
 
@@ -374,7 +374,7 @@ namespace StrictWeakOrder
 
 section
 
-variable {α : Type u} {r : α → α → Prop}
+variable {α : Sort u} {r : α → α → Prop}
 
 local infixl:50 " ≺ " => r
 
@@ -416,7 +416,7 @@ a " ≈[" lt "]" b:50 => @Equiv _ lt a b
 
 end StrictWeakOrder
 
-theorem isStrictWeakOrder_of_isTotalPreorder {α : Type u} {le : α → α → Prop} {lt : α → α → Prop}
+theorem isStrictWeakOrder_of_isTotalPreorder {α : Sort u} {le : α → α → Prop} {lt : α → α → Prop}
     [DecidableRel le] [IsTotalPreorder α le] (h : ∀ a b, lt a b ↔ ¬le b a) :
     IsStrictWeakOrder α lt :=
   { trans := fun a b c hab hbc =>
@@ -438,7 +438,7 @@ theorem isStrictWeakOrder_of_isTotalPreorder {α : Type u} {le : α → α → P
       And.intro (fun n => absurd hca (Iff.mp (h _ _) n)) fun n => absurd hac (Iff.mp (h _ _) n) }
 #align is_strict_weak_order_of_is_total_preorder isStrictWeakOrder_of_isTotalPreorder
 
-theorem lt_of_lt_of_incomp {α : Type u} {lt : α → α → Prop} [IsStrictWeakOrder α lt]
+theorem lt_of_lt_of_incomp {α : Sort u} {lt : α → α → Prop} [IsStrictWeakOrder α lt]
     [DecidableRel lt] : ∀ {a b c}, lt a b → ¬lt b c ∧ ¬lt c b → lt a c :=
   @fun a b c hab ⟨nbc, ncb⟩ =>
   have nca : ¬lt c a := fun hca => absurd (trans_of lt hca hab) ncb
@@ -447,7 +447,7 @@ theorem lt_of_lt_of_incomp {α : Type u} {lt : α → α → Prop} [IsStrictWeak
     absurd hab this.1
 #align lt_of_lt_of_incomp lt_of_lt_of_incomp
 
-theorem lt_of_incomp_of_lt {α : Type u} {lt : α → α → Prop} [IsStrictWeakOrder α lt]
+theorem lt_of_incomp_of_lt {α : Sort u} {lt : α → α → Prop} [IsStrictWeakOrder α lt]
     [DecidableRel lt] : ∀ {a b c}, ¬lt a b ∧ ¬lt b a → lt b c → lt a c :=
   @fun a b c ⟨nab, nba⟩ hbc =>
   have nca : ¬lt c a := fun hca => absurd (trans_of lt hbc hca) nba
@@ -456,29 +456,29 @@ theorem lt_of_incomp_of_lt {α : Type u} {lt : α → α → Prop} [IsStrictWeak
     absurd hbc this.1
 #align lt_of_incomp_of_lt lt_of_incomp_of_lt
 
-theorem eq_of_incomp {α : Type u} {lt : α → α → Prop} [IsTrichotomous α lt] {a b} :
+theorem eq_of_incomp {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a b} :
     ¬lt a b ∧ ¬lt b a → a = b := fun ⟨nab, nba⟩ =>
   match trichotomous_of lt a b with
   | Or.inl hab => absurd hab nab
   | Or.inr (Or.inl hab) => hab
   | Or.inr (Or.inr hba) => absurd hba nba
 #align eq_of_incomp eq_of_incomp
 
-theorem eq_of_eqv_lt {α : Type u} {lt : α → α → Prop} [IsTrichotomous α lt] {a b} :
+theorem eq_of_eqv_lt {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a b} :
     a ≈[lt]b → a = b :=
   eq_of_incomp
 #align eq_of_eqv_lt eq_of_eqv_lt
 
-theorem incomp_iff_eq {α : Type u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a b) :
+theorem incomp_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a b) :
     ¬lt a b ∧ ¬lt b a ↔ a = b :=
   Iff.intro eq_of_incomp fun hab => hab ▸ And.intro (irrefl_of lt a) (irrefl_of lt a)
 #align incomp_iff_eq incomp_iff_eq
 
-theorem eqv_lt_iff_eq {α : Type u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a b) :
+theorem eqv_lt_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a b) :
     a ≈[lt]b ↔ a = b :=
   incomp_iff_eq a b
 #align eqv_lt_iff_eq eqv_lt_iff_eq
 
-theorem not_lt_of_lt {α : Type u} {lt : α → α → Prop} [IsStrictOrder α lt] {a b} :
+theorem not_lt_of_lt {α : Sort u} {lt : α → α → Prop} [IsStrictOrder α lt] {a b} :
     lt a b → ¬lt b a := fun h₁ h₂ => absurd (trans_of lt h₁ h₂) (irrefl_of lt _)
 #align not_lt_of_lt not_lt_of_lt

Mathlib/Init/ZeroOne.lean

@@ -14,10 +14,10 @@ class Zero.{u} (α : Type u) where
   zero : α
 #align has_zero Zero
 
-instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
+instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
   ofNat := ‹Zero α›.1
 
-instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
+instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
   zero := 0
 
 
@@ -27,10 +27,10 @@ class One (α : Type u) where
 #align has_one One
 
 @[to_additive existing Zero.toOfNat0]
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
+instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
   ofNat := ‹One α›.1
 @[to_additive existing Zero.ofOfNat0, to_additive_change_numeral 2]
-instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
+instance (priority := 200) One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
   one := 1
 
 @[deprecated, match_pattern] def bit0 {α : Type u} [Add α] (a : α) : α := a + a

Mathlib/Logic/Function/Basic.lean

@@ -23,7 +23,7 @@ namespace Function
 
 section
 
-variable {α β γ : Sort _} {f : α → β}
+variable {α β γ : Sort*} {f : α → β}
 
 /-- Evaluate a function at an argument. Useful if you want to talk about the partially applied
   `Function.eval x : (∀ x, β x) → β x`. -/
@@ -87,7 +87,7 @@ theorem Injective.eq_iff (I : Injective f) {a b : α} : f a = f b ↔ a = b :=
   ⟨@I _ _, congr_arg f⟩
 #align function.injective.eq_iff Function.Injective.eq_iff
 
-theorem Injective.beq_eq [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β]
+theorem Injective.beq_eq {α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {f : α → β}
     (I : Injective f) {a b : α} : (f a == f b) = (a == b) := by
   by_cases h : a == b <;> simp [h] <;> simpa [I.eq_iff] using h