From 0770956a5269358923b1b0098d3827da9f19ad3b Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Mon, 3 Feb 2025 13:31:43 +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 e867d9f21930b..8f3b54ef36a4e 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] lemma coe_mk (f : InfHom X X) (h1 h2) : ⇑(mk f h1 h2) = f := rfl instance : NucleusClass (Nucleus X) X where idempotent _ _ := idempotent' ..