From ed30a4bda6e145c9abeff276dba278f471f94ba8 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Thu, 8 Feb 2024 14:40:16 +0000 Subject: [PATCH] feat: change Type to Sort in `Algebra/Classes`, fix some priorities (#10354) --- Mathlib/Data/Nat/Cast/Defs.lean | 2 +- Mathlib/Init/Algebra/Classes.lean | 108 +++++++++++++++--------------- Mathlib/Init/ZeroOne.lean | 8 +-- Mathlib/Logic/Function/Basic.lean | 4 +- 4 files changed, 61 insertions(+), 61 deletions(-) diff --git a/Mathlib/Data/Nat/Cast/Defs.lean b/Mathlib/Data/Nat/Cast/Defs.lean index e2a184c21c213..1d6876a39c6b4 100644 --- a/Mathlib/Data/Nat/Cast/Defs.lean +++ b/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" diff --git a/Mathlib/Init/Algebra/Classes.lean b/Mathlib/Init/Algebra/Classes.lean index a3a8882bfac3e..b80ea46921f18 100644 --- a/Mathlib/Init/Algebra/Classes.lean +++ b/Mathlib/Init/Algebra/Classes.lean @@ -67,211 +67,211 @@ 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 @@ -279,7 +279,7 @@ instance eq_isEquiv (α : Type u) : IsEquiv α (· = ·) where 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,7 +456,7 @@ 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 @@ -464,21 +464,21 @@ theorem eq_of_incomp {α : Type u} {lt : α → α → Prop} [IsTrichotomous α | 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 diff --git a/Mathlib/Init/ZeroOne.lean b/Mathlib/Init/ZeroOne.lean index 4c279022a491a..0efd4fb2fb46b 100644 --- a/Mathlib/Init/ZeroOne.lean +++ b/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 diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean index 5b657e624a851..d39519d772d8a 100644 --- a/Mathlib/Logic/Function/Basic.lean +++ b/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