Lean4
/-- If `F₁` and `F₂` are functors `J ⥤ C`, `G : K ⥤ J`, and
`F₁'` and `F₂'` are functors `K ⥤ C` that are respectively
isomorphic to `G ⋙ F₁` and `G ⋙ F₂`, then this is the
induced morphism `enrichedHom V F₁ F₂ ⟶ enrichedHom V F₁' F₂'` in `V`
when `C` is a category enriched in `V`. -/
noncomputable abbrev precompEnrichedHom' {F₁' F₂' : K ⥤ C} [HasEnrichedHom V F₁' F₂'] (e₁ : G ⋙ F₁ ≅ F₁')
(e₂ : G ⋙ F₂ ≅ F₂') : enrichedHom V F₁ F₂ ⟶ enrichedHom V F₁' F₂' :=
end_.lift
(fun x ↦
enrichedHomπ V F₁ F₂ (G.obj x) ≫ (eHomWhiskerRight _ (e₁.inv.app x) _ ≫ eHomWhiskerLeft _ _ (e₂.hom.app x)))
(fun i j f ↦ by
dsimp
rw [assoc, assoc, assoc, assoc, ← eHomWhiskerLeft_comp, ← eHom_whisker_exchange, ← e₂.hom.naturality f,
eHomWhiskerLeft_comp_assoc]
dsimp
rw [enrichedHom_condition_assoc, eHom_whisker_exchange, eHom_whisker_exchange, ← eHomWhiskerRight_comp_assoc, ←
eHomWhiskerRight_comp_assoc, NatTrans.naturality]
dsimp)
