∀ {M₁ : Type u_1} {M₂ : Type u_3} {N : Type u_2} [inst : MulOneClass M₁] [inst_1 : MulOneClass M₂] [inst_2 : Monoid N]
  (e : M₁ ≃* M₂) (f : M₁ →* N), (fun f => f.comp e.toMonoidHom) ((fun f => f.comp e.symm.toMonoidHom) f) = f