English
If X = Y and q: Y ⟶ Z, then transporting q along the equality X=Y yields a map from X to Z; applying mpr yields eqToHom p ≫ q.
Русский
Если X = Y и q: Y ⟶ Z, то перенос q по равенству X=Y дает отображение X ⟶ Z; применение mpr дает eqToHom p ≫ q.
LaTeX
$$$ (\\mathrm{congrArg}(\\lambda W: C \\to Z) p).mpr q = eqToHom(p) \\circ q $$$
Lean4
/-- If we (perhaps unintentionally) perform equational rewriting on
the source object of a morphism,
we can replace the resulting `_.mpr f` term by a composition with an `eqToHom`.
It may be advisable to introduce any necessary `eqToHom` morphisms manually,
rather than relying on this lemma firing.
-/
theorem congrArg_mpr_hom_left {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :
(congrArg (fun W : C => W ⟶ Z) p).mpr q = eqToHom p ≫ q :=
by
cases p
simp
