no goals
C : Type u
inst✝² : Category C
P Q : C
f : P ⟶ Q
inst✝¹ : Epi f
inst✝ : StrongMono f
⊢ 𝟙 P ≫ f = f ≫ 𝟙 Q
simp
no goals
C : Type u
inst✝² : Category C
P Q : C
f : P ⟶ Q
inst✝¹ : Epi f
inst✝ : StrongMono f
⊢ f ≫ CommSq.lift (_ : CommSq (𝟙 P) f f (𝟙 Q)) = 𝟙 P ∧ CommSq.lift (_ : CommSq (𝟙 P) f f (𝟙 Q)) ≫ f = 𝟙 Q
aesop_cat