From dc8955f7f6a1c6ca8cfa62bae4f836cacdc03e5a Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Mon, 3 Feb 2025 13:11:08 +0000 Subject: [PATCH] feat(Order/Nucleus): coe_mk simp lemma (#21346) Add `Nucleus.coe_mk`. Co-authored-by: Bergschaf <86738237+Bergschaf@users.noreply.github.com> --- Mathlib/Order/Nucleus.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Order/Nucleus.lean b/Mathlib/Order/Nucleus.lean index e867d9f21930b9..2a2c9d52506bda 100644 --- a/Mathlib/Order/Nucleus.lean +++ b/Mathlib/Order/Nucleus.lean @@ -55,6 +55,7 @@ instance : FunLike (Nucleus X) X X where lemma toFun_eq_coe (n : Nucleus X) : n.toFun = n := rfl @[simp] lemma coe_toInfHom (n : Nucleus X) : ⇑n.toInfHom = n := rfl +@[simp, norm_cast] lemma coe_mk (f : InfHom X X) (h1 h2) : ⇑(mk f h1 h2) = f := rfl instance : NucleusClass (Nucleus X) X where idempotent _ _ := idempotent' ..