no goals
C : Type u
inst✝¹ : Category C
inst✝ : IsFilteredOrEmpty C
i j j' : C
f : i ⟶ j
f' : i ⟶ j'
K : C
G : j ⟶ K
G' : j' ⟶ K
h✝ : True
k : C
e : K ⟶ k
he : (f ≫ G) ≫ e = (f' ≫ G') ≫ e
⊢ f ≫ G ≫ e = f' ≫ G' ≫ e
simpa only [← Category.assoc]