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