chore(data/equiv/mul_add): add monoid_hom.to_mul_equiv (#4628)

src/algebra/category/Group/basic.lean

@@ -203,25 +203,17 @@ namespace category_theory.iso
 @[to_additive AddGroup_iso_to_add_equiv "Build an `add_equiv` from an isomorphism in the category
 `AddGroup`."]
 def Group_iso_to_mul_equiv {X Y : Group} (i : X ≅ Y) : X ≃* Y :=
-{ to_fun    := i.hom,
-  inv_fun   := i.inv,
-  left_inv  := by tidy,
-  right_inv := by tidy,
-  map_mul'  := by tidy }.
+i.hom.to_mul_equiv i.inv i.hom_inv_id i.inv_hom_id
 
-attribute [simps] Group_iso_to_mul_equiv AddGroup_iso_to_add_equiv
+attribute [simps {rhs_md := semireducible}] Group_iso_to_mul_equiv AddGroup_iso_to_add_equiv
 
 /-- Build a `mul_equiv` from an isomorphism in the category `CommGroup`. -/
 @[to_additive AddCommGroup_iso_to_add_equiv "Build an `add_equiv` from an isomorphism
 in the category `AddCommGroup`."]
 def CommGroup_iso_to_mul_equiv {X Y : CommGroup} (i : X ≅ Y) : X ≃* Y :=
-{ to_fun    := i.hom,
-  inv_fun   := i.inv,
-  left_inv  := by tidy,
-  right_inv := by tidy,
-  map_mul'  := by tidy }.
+i.hom.to_mul_equiv i.inv i.hom_inv_id i.inv_hom_id
 
-attribute [simps] CommGroup_iso_to_mul_equiv AddCommGroup_iso_to_add_equiv
+attribute [simps {rhs_md := semireducible}] CommGroup_iso_to_mul_equiv AddCommGroup_iso_to_add_equiv
 
 end category_theory.iso
 

src/algebra/category/Mon/basic.lean

@@ -152,21 +152,13 @@ namespace category_theory.iso
 @[to_additive AddMon_iso_to_add_equiv "Build an `add_equiv` from an isomorphism in the category
 `AddMon`."]
 def Mon_iso_to_mul_equiv {X Y : Mon} (i : X ≅ Y) : X ≃* Y :=
-{ to_fun    := i.hom,
-  inv_fun   := i.inv,
-  left_inv  := by tidy,
-  right_inv := by tidy,
-  map_mul'  := by tidy }.
+i.hom.to_mul_equiv i.inv i.hom_inv_id i.inv_hom_id
 
 /-- Build a `mul_equiv` from an isomorphism in the category `CommMon`. -/
 @[to_additive "Build an `add_equiv` from an isomorphism in the category
 `AddCommMon`."]
 def CommMon_iso_to_mul_equiv {X Y : CommMon} (i : X ≅ Y) : X ≃* Y :=
-{ to_fun    := i.hom,
-  inv_fun   := i.inv,
-  left_inv  := by tidy,
-  right_inv := by tidy,
-  map_mul'  := by tidy }.
+i.hom.to_mul_equiv i.inv i.hom_inv_id i.inv_hom_id
 
 end category_theory.iso
 

src/data/equiv/mul_add.lean

@@ -189,6 +189,11 @@ def to_monoid_hom {M N} [monoid M] [monoid N] (h : M ≃* N) : (M →* N) :=
 { map_one' := h.map_one, .. h }
 
 @[simp, to_additive]
+lemma coe_to_monoid_hom {M N} [monoid M] [monoid N] (e : M ≃* N) :
+  ⇑e.to_monoid_hom = e :=
+rfl
+
+@[to_additive]
 lemma to_monoid_hom_apply {M N} [monoid M] [monoid N] (e : M ≃* N) (x : M) :
   e.to_monoid_hom x = e x :=
 rfl
@@ -230,6 +235,39 @@ attribute [ext] add_equiv.ext
 
 end mul_equiv
 
+-- We don't use `to_additive` to generate definition because it fails to tell Lean about
+-- equational lemmas
+
+/-- Given a pair of additive monoid homomorphisms `f`, `g` such that `g.comp f = id` and
+`f.comp g = id`, returns an additive equivalence with `to_fun = f` and `inv_fun = g`.  This
+constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
+monoid homomorphisms. -/
+def add_monoid_hom.to_add_equiv [add_monoid M] [add_monoid N] (f : M →+ N) (g : N →+ M)
+  (h₁ : g.comp f = add_monoid_hom.id _) (h₂ : f.comp g = add_monoid_hom.id _) :
+  M ≃+ N :=
+{ to_fun := f,
+  inv_fun := g,
+  left_inv := add_monoid_hom.congr_fun h₁,
+  right_inv := add_monoid_hom.congr_fun h₂,
+  map_add' := f.map_add }
+
+/-- Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`,
+returns an multiplicative equivalence with `to_fun = f` and `inv_fun = g`.  This constructor is
+useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms. -/
+@[to_additive]
+def monoid_hom.to_mul_equiv [monoid M] [monoid N] (f : M →* N) (g : N →* M)
+  (h₁ : g.comp f = monoid_hom.id _) (h₂ : f.comp g = monoid_hom.id _) :
+  M ≃* N :=
+{ to_fun := f,
+  inv_fun := g,
+  left_inv := monoid_hom.congr_fun h₁,
+  right_inv := monoid_hom.congr_fun h₂,
+  map_mul' := f.map_mul }
+
+@[simp, to_additive]
+lemma monoid_hom.coe_to_mul_equiv [monoid M] [monoid N] (f : M →* N) (g : N →* M) (h₁ h₂) :
+  ⇑(f.to_mul_equiv g h₁ h₂) = f := rfl
+
 /-- An additive equivalence of additive groups preserves subtraction. -/
 lemma add_equiv.map_sub [add_group A] [add_group B] (h : A ≃+ B) (x y : A) :
   h (x - y) = h x - h y :=