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 Y' Z : D
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
f' : W ⟶ X'
g' : X' ⟶ Y'
h' : Y' ⟶ Z
⊢ f ≫ g ≫ h ≫ (counitInv e).app Z = f' ≫ g' ≫ h' ≫ (counitInv e).app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'
simp only [← Category.assoc, cancel_mono]