feat: isomorphic monoid objects have isomorphic hom monoids (#29830)

From Toric

Author: YaelDillies

Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

@@ -355,3 +355,13 @@ lemma MonObj.mul_eq_mul : μ = fst M M * snd _ _ :=
   show _ = _ ≫ _ by rw [lift_fst_snd, Category.id_comp]
 
 @[deprecated (since := "2025-09-09")] alias Mon_Class.mul_eq_mul := MonObj.mul_eq_mul
+
+namespace Hom
+
+/-- If `M` and `N` are isomorphic as monoid objects, then `X ⟶ M` and `X ⟶ N` are isomorphic
+monoids. -/
+@[simps!]
+def mulEquivCongrRight (e : M ≅ N) [IsMonHom e.hom] (X : C) : (X ⟶ M) ≃* (X ⟶ N) :=
+  ((yonedaMon.mapIso <| Mon.mkIso' e).app <| .op X).monCatIsoToMulEquiv
+
+end Hom