English
For p: X ⟶ Y and q: Z = Y, the transported morphism satisfies (congrArg(λ W, X ⟶ W) q).mpr p = p ≫ eqToHom q.symm.
Русский
Для p: X ⟶ Y и q: Z = Y перенос по q даёт: (congrArg(λ W, X ⟶ W) q).mpr p = p ≫ eqToHom q.symm.
LaTeX
$$$ (\\mathrm{congrArg}(\\lambda W: X \\to W) q).mpr p = p \\circ eqToHom(q^{\\mathrm{symm}}) $$$
Lean4
/-- If we (perhaps unintentionally) perform equational rewriting on
the target 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_right {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) :
(congrArg (fun W : C => X ⟶ W) q).mpr p = p ≫ eqToHom q.symm :=
by
cases q
simp
