no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
e : C ≌ D
X Y : D
f f' : X ⟶ Y
⊢ f ≫ (counitInv e).app Y = f' ≫ (counitInv e).app Y ↔ f = f'
simp only [cancel_mono]