feat(Order/Nucleus): coe_mk simp lemma (#21346)

Add `Nucleus.coe_mk`. Co-authored-by: Bergschaf <[email protected]>
leanprover-community · Feb 3, 2025 · 0770956 · 0770956
1 parent e1f1958
commit 0770956
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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' ..