fix(Order/Hom): coercion lemmas for lattice and complete lattice (#7796)

These are a number of small fixes of coercions of lattices and complete lattices, made by Yaël Dillies in the context of a larger refactor of the branch `frametopadjunction`.

Co-authored by: Yaël Dillies

Mathlib/Order/Hom/CompleteLattice.lean

@@ -254,12 +254,11 @@ instance : sSupHomClass (sSupHom α β) α β
 -- instance : CoeFun (sSupHom α β) fun _ => α → β :=
 --   FunLike.hasCoeToFun
 
--- Porting note: times out
-@[simp]
-theorem toFun_eq_coe {f : sSupHom α β} : f.toFun = ⇑f :=
-  rfl
+@[simp] lemma toFun_eq_coe (f : sSupHom α β) : f.toFun = f := rfl
 #align Sup_hom.to_fun_eq_coe sSupHom.toFun_eq_coe
 
+@[simp, norm_cast] lemma coe_mk (f : α → β) (hf) : ⇑(mk f hf) = f := rfl
+
 @[ext]
 theorem ext {f g : sSupHom α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h
@@ -401,11 +400,11 @@ instance : sInfHomClass (sInfHom α β) α β
 -- instance : CoeFun (sInfHom α β) fun _ => α → β :=
 --   FunLike.hasCoeToFun
 
-@[simp]
-theorem toFun_eq_coe {f : sInfHom α β} : f.toFun = ⇑f :=
-  rfl
+@[simp] lemma toFun_eq_coe (f : sInfHom α β) : f.toFun = f := rfl
 #align Inf_hom.to_fun_eq_coe sInfHom.toFun_eq_coe
 
+@[simp] lemma coe_mk (f : α → β) (hf) : ⇑(mk f hf) = f := rfl
+
 @[ext]
 theorem ext {f g : sInfHom α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h
@@ -553,16 +552,12 @@ def toLatticeHom (f : FrameHom α β) : LatticeHom α β :=
   f
 #align frame_hom.to_lattice_hom FrameHom.toLatticeHom
 
-/- Porting note: SimpNF linter complains that lhs can be simplified,
-added _aux version with [simp] attribute -/
--- @[simp]
-theorem toFun_eq_coe {f : FrameHom α β} : f.toFun = ⇑f :=
-  rfl
+lemma toFun_eq_coe (f : FrameHom α β) : f.toFun = f := rfl
 #align frame_hom.to_fun_eq_coe FrameHom.toFun_eq_coe
 
-@[simp]
-theorem toFun_eq_coe_aux {f : FrameHom α β} : ↑f.toInfTopHom = ⇑f :=
-  rfl
+@[simp] lemma coe_toInfTopHom (f : FrameHom α β) : ⇑f.toInfTopHom = f := rfl
+@[simp] lemma coe_toLatticeHom (f : FrameHom α β) : ⇑f.toLatticeHom = f := rfl
+@[simp] lemma coe_mk (f : InfTopHom α β) (hf) : ⇑(mk f hf) = f := rfl
 
 @[ext]
 theorem ext {f g : FrameHom α β} (h : ∀ a, f a = g a) : f = g :=
@@ -685,16 +680,14 @@ def toBoundedLatticeHom (f : CompleteLatticeHom α β) : BoundedLatticeHom α β
 -- instance : CoeFun (CompleteLatticeHom α β) fun _ => α → β :=
 --   FunLike.hasCoeToFun
 
-/- Porting note: SimpNF linter complains that lhs can be simplified,
-added _aux version with [simp] attribute -/
--- @[simp]
-theorem toFun_eq_coe {f : CompleteLatticeHom α β} : f.toFun = ⇑f :=
-  rfl
+lemma toFun_eq_coe (f : CompleteLatticeHom α β) : f.toFun = f := rfl
 #align complete_lattice_hom.to_fun_eq_coe CompleteLatticeHom.toFun_eq_coe
 
-@[simp]
-theorem toFun_eq_coe_aux {f : CompleteLatticeHom α β} : ↑f.tosInfHom = ⇑f :=
-  rfl
+@[simp] lemma coe_tosInfHom (f : CompleteLatticeHom α β) : ⇑f.tosInfHom = f := rfl
+@[simp] lemma coe_tosSupHom (f : CompleteLatticeHom α β) : ⇑f.tosSupHom = f := rfl
+@[simp] lemma coe_toBoundedLatticeHom (f : CompleteLatticeHom α β) : ⇑f.toBoundedLatticeHom = f :=
+rfl
+@[simp] lemma coe_mk (f : sInfHom α β) (hf) : ⇑(mk f hf) = f := rfl
 
 @[ext]
 theorem ext {f g : CompleteLatticeHom α β} (h : ∀ a, f a = g a) : f = g :=

Mathlib/Order/Hom/Lattice.lean

@@ -345,11 +345,11 @@ directly. -/
 instance : FunLike (SupHom α β) α fun _ => β :=
   SupHomClass.toFunLike
 
-@[simp]
-theorem toFun_eq_coe {f : SupHom α β} : f.toFun = (f : α → β) :=
-  rfl
+@[simp] lemma toFun_eq_coe (f : SupHom α β) : f.toFun = f := rfl
 #align sup_hom.to_fun_eq_coe SupHom.toFun_eq_coe
 
+@[simp, norm_cast] lemma coe_mk (f : α → β) (hf) : ⇑(mk f hf) = f := rfl
+
 @[ext]
 theorem ext {f g : SupHom α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h
@@ -532,11 +532,11 @@ directly. -/
 instance : FunLike (InfHom α β) α fun _ => β :=
   InfHomClass.toFunLike
 
-@[simp]
-theorem toFun_eq_coe {f : InfHom α β} : f.toFun = (f : α → β) :=
-  rfl
+@[simp] lemma toFun_eq_coe (f : InfHom α β) : f.toFun = (f : α → β) := rfl
 #align inf_hom.to_fun_eq_coe InfHom.toFun_eq_coe
 
+@[simp, norm_cast] lemma coe_mk (f : α → β) (hf) : ⇑(mk f hf) = f := rfl
+
 @[ext]
 theorem ext {f g : InfHom α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h
@@ -728,20 +728,13 @@ instance : SupBotHomClass (SupBotHom α β) α β
 instance : FunLike (SupBotHom α β) α fun _ => β :=
   SupHomClass.toFunLike
 
--- porting note: this is the `simp`-normal version of `toFun_eq_coe`
-@[simp]
-theorem coe_toSupHom {f : SupBotHom α β} : (f.toSupHom : α → β) = (f : α → β) :=
-  rfl
-
--- porting note: adding this since we also added `coe_toSupHom`
-@[simp]
-theorem coe_toBotHom {f : SupBotHom α β} : (f.toBotHom : α → β) = (f : α → β) :=
-  rfl
-
-theorem toFun_eq_coe {f : SupBotHom α β} : f.toFun = (f : α → β) :=
-  rfl
+lemma toFun_eq_coe (f : SupBotHom α β) : f.toFun = f := rfl
 #align sup_bot_hom.to_fun_eq_coe SupBotHom.toFun_eq_coe
 
+@[simp] lemma coe_toSupHom (f : SupBotHom α β) : ⇑f.toSupHom = f := rfl
+@[simp] lemma coe_toBotHom (f : SupBotHom α β) : ⇑f.toBotHom = f := rfl
+@[simp] lemma coe_mk (f : SupHom α β) (hf) : ⇑(mk f hf) = f := rfl
+
 @[ext]
 theorem ext {f g : SupBotHom α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h
@@ -891,19 +884,13 @@ directly. -/
 instance : FunLike (InfTopHom α β) α fun _ => β :=
   InfHomClass.toFunLike
 
--- porting note: this is the `simp`-normal version of `toFun_eq_coe`
-@[simp]
-theorem coe_toInfHom {f : InfTopHom α β} : (f.toInfHom : α → β) = (f : α → β) :=
-  rfl
-
--- porting note: adding this since we also added `coe_toInfHom`
-@[simp]
-theorem coe_toTopHom {f : InfTopHom α β} : (f.toTopHom : α → β) = (f : α → β) :=
-  rfl
-
-theorem toFun_eq_coe {f : InfTopHom α β} : f.toFun = (f : α → β) := rfl
+theorem toFun_eq_coe (f : InfTopHom α β) : f.toFun = f := rfl
 #align inf_top_hom.to_fun_eq_coe InfTopHom.toFun_eq_coe
 
+@[simp] lemma coe_toInfHom (f : InfTopHom α β) : ⇑f.toInfHom = f := rfl
+@[simp] lemma coe_toTopHom (f : InfTopHom α β) : ⇑f.toTopHom = f := rfl
+@[simp] lemma coe_mk (f : InfHom α β) (hf) : ⇑(mk f hf) = f := rfl
+
 @[ext]
 theorem ext {f g : InfTopHom α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h
@@ -1046,19 +1033,13 @@ directly. -/
 instance : FunLike (LatticeHom α β) α fun _ => β :=
   SupHomClass.toFunLike
 
--- porting note: this is the `simp`-normal version of `toFun_eq_coe`
-@[simp]
-theorem coe_toSupHom {f : LatticeHom α β} : (f.toSupHom : α → β) = (f : α → β) :=
-  rfl
-
--- porting note: adding this since we also added `coe_toSupHom`
-@[simp]
-theorem coe_toInfHom {f : LatticeHom α β} : (f.toInfHom : α → β) = (f : α → β) :=
-  rfl
-
-theorem toFun_eq_coe {f : LatticeHom α β} : f.toFun = (f : α → β) := rfl
+lemma toFun_eq_coe (f : LatticeHom α β) : f.toFun = f := rfl
 #align lattice_hom.to_fun_eq_coe LatticeHom.toFun_eq_coe
 
+@[simp] lemma coe_toSupHom (f : LatticeHom α β) : ⇑f.toSupHom = f := rfl
+@[simp] lemma coe_toInfHom (f : LatticeHom α β) : ⇑f.toInfHom = f := rfl
+@[simp] lemma coe_mk (f : SupHom α β) (hf) : ⇑(mk f hf) = f := rfl
+
 @[ext]
 theorem ext {f g : LatticeHom α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h
@@ -1237,16 +1218,15 @@ instance instBoundedLatticeHomClass : BoundedLatticeHomClass (BoundedLatticeHom
   map_top f := f.map_top'
   map_bot f := f.map_bot'
 
--- porting note: this is the `simp`-normal version of `toFun_eq_coe`
-@[simp]
-theorem coe_toLatticeHom {f : BoundedLatticeHom α β} : (f.toLatticeHom : α → β) = (f : α → β) :=
-  rfl
-
-@[simp]
-theorem toFun_eq_coe {f : BoundedLatticeHom α β} : f.toFun = (f : α → β) :=
-  rfl
+@[simp] lemma toFun_eq_coe (f : BoundedLatticeHom α β) : f.toFun = f := rfl
 #align bounded_lattice_hom.to_fun_eq_coe BoundedLatticeHom.toFun_eq_coe
 
+@[simp] lemma coe_toLatticeHom (f : BoundedLatticeHom α β) : ⇑f.toLatticeHom = f := rfl
+@[simp] lemma coe_toSupBotHom (f : BoundedLatticeHom α β) : ⇑f.toSupBotHom = f := rfl
+@[simp] lemma coe_toInfTopHom (f : BoundedLatticeHom α β) : ⇑f.toInfTopHom = f := rfl
+@[simp] lemma coe_toBoundedOrderHom (f : BoundedLatticeHom α β) : ⇑f.toBoundedOrderHom = f := rfl
+@[simp] lemma coe_mk (f : LatticeHom α β) (hf hf') : ⇑(mk f hf hf') = f := rfl
+
 @[ext]
 theorem ext {f g : BoundedLatticeHom α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h