no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
α : F ≅ G
X : D
Y : C
f f' : X ⟶ F.obj Y
⊢ f ≫ α.hom.app Y = f' ≫ α.hom.app Y ↔ f = f'
simp only [cancel_mono, refl]