no goals
C : Type u
inst✝¹ : Category C
D : Type u₁
inst✝ : Category D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ F.map (↑(Iso.homCongr α β) f) = ↑(Iso.homCongr (F.mapIso α) (F.mapIso β)) (F.map f)
simp