Best way to compose morphisms across an equality

Stream: mathlib4

[Chris Henson]

If I have morphisms a ⟶ b, c ⟶ d, and a proof that b = c, what is the best way to compose them? I tried writing something like the following

import Mathlib.CategoryTheory.Category.Basic
open CategoryTheory

def comp_eq
  {X : Type}
  [Category X]
  {a b c d : X}
  (m1 : a ⟶  b)
  (m2 : c ⟶  d)
  (h : b = c)
  : a ⟶  d :=
  by
  rw [h] at m1
  exact m1 ≫ m2

Is there a better way I should do this? This results in having cast in proofs that use it, which seems difficult to work with.

[Yaël Dillies]

There is indeed a better way, and it is docs#CategoryTheory.eqToHom

[Yaël Dillies]

The important thing is that we taught simp how to handle eqToHom