From e0e004a2406351f254842985eb68b467c53c2cdf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 16 Oct 2024 11:05:19 +0000 Subject: [PATCH] chore(SetTheory/Ordinal/Arithmetic): fix `Ordinal.enum` type signature (#17601) For some reason, Lean was inferring [some nonsense](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/Basic.html#Ordinal.enum). Unfortunately, the explicit typing is required for `simp`; see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20and.20subrel). --- Mathlib/SetTheory/Ordinal/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index b0d0c08af9e087..2de607c6ac4062 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -449,7 +449,7 @@ the elements of `α`. -/ -- The explicit typing is required in order for `simp` to work properly. @[simps! symm_apply_coe] def enum (r : α → α → Prop) [IsWellOrder α r] : - @RelIso (Subtype fun o => o < type r) α (Subrel (· < · ) _) r := + @RelIso { o // o < type r } α (Subrel (· < ·) { o | o < type r }) r := (typein.principalSeg r).subrelIso @[simp]