From 121c9a49ad79f4e3dd6dd80beba190e7896f612e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 26 Oct 2020 05:21:08 +0000
Subject: [PATCH] chore(algebra/group/hom): use `coe_comp` in `simp` lemmas
 (#4780)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This way Lean will simplify `⇑(f.comp g)` even if it is not applied to
an element.
---
 src/algebra/group/hom.lean  | 16 +++++++++++++---
 src/algebra/ring/basic.lean |  7 +++++--
 2 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/algebra/group/hom.lean b/src/algebra/group/hom.lean
index 2e0996adeb771..9083d84e326b5 100644
--- a/src/algebra/group/hom.lean
+++ b/src/algebra/group/hom.lean
@@ -279,13 +279,23 @@ add_decl_doc add_hom.comp
 /-- Composition of additive monoid morphisms as an additive monoid morphism. -/
 add_decl_doc add_monoid_hom.comp
 
-@[simp, to_additive] lemma one_hom.comp_apply [has_one M] [has_one N] [has_one P]
+@[simp, to_additive] lemma one_hom.coe_comp [has_one M] [has_one N] [has_one P]
+  (g : one_hom N P) (f : one_hom M N) :
+  ⇑(g.comp f) = g ∘ f := rfl
+@[simp, to_additive] lemma mul_hom.coe_comp [has_mul M] [has_mul N] [has_mul P]
+  (g : mul_hom N P) (f : mul_hom M N) :
+  ⇑(g.comp f) = g ∘ f := rfl
+@[simp, to_additive] lemma monoid_hom.coe_comp [monoid M] [monoid N] [monoid P]
+  (g : N →* P) (f : M →* N) :
+  ⇑(g.comp f) = g ∘ f := rfl
+
+@[to_additive] lemma one_hom.comp_apply [has_one M] [has_one N] [has_one P]
   (g : one_hom N P) (f : one_hom M N) (x : M) :
   g.comp f x = g (f x) := rfl
-@[simp, to_additive] lemma mul_hom.comp_apply [has_mul M] [has_mul N] [has_mul P]
+@[to_additive] lemma mul_hom.comp_apply [has_mul M] [has_mul N] [has_mul P]
   (g : mul_hom N P) (f : mul_hom M N) (x : M) :
   g.comp f x = g (f x) := rfl
-@[simp, to_additive] lemma monoid_hom.comp_apply [monoid M] [monoid N] [monoid P]
+@[to_additive] lemma monoid_hom.comp_apply [monoid M] [monoid N] [monoid P]
   (g : N →* P) (f : M →* N) (x : M) :
   g.comp f x = g (f x) := rfl
 
diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean
index 7d531e6a5b953..0f287f58e95fb 100644
--- a/src/algebra/ring/basic.lean
+++ b/src/algebra/ring/basic.lean
@@ -197,8 +197,11 @@ def mul_right {R : Type*} [semiring R] (r : R) : R →+ R :=
   map_zero' := zero_mul r,
   map_add' := λ _ _, add_mul _ _ r }
 
-@[simp] lemma mul_right_apply {R : Type*} [semiring R] (a r : R) :
-  (mul_right r : R → R) a = a * r := rfl
+@[simp] lemma coe_mul_right {R : Type*} [semiring R] (r : R) :
+  ⇑(mul_right r) = (* r) := rfl
+
+lemma mul_right_apply {R : Type*} [semiring R] (a r : R) :
+  mul_right r a = a * r := rfl
 
 end add_monoid_hom