no goals
C : Type u
inst✝⁶ : Category C
X Y : C
D : Type u₂
inst✝⁵ : Category D
F : C ⥤ D
A A' B B' : C
inst✝⁴ : HasBinaryCoproduct A B
inst✝³ : HasBinaryCoproduct A' B'
inst✝² : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryCoproduct (F.obj A') (F.obj B')
inst✝ : IsIso (coprodComparison F A B)
⊢ F.map coprod.inr ≫ inv (coprodComparison F A B) = coprod.inr
simp [IsIso.inv_comp_eq]