C : Type u₁
inst✝ : Category C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : (g ≫ f) ≫ sm.retraction = (h ≫ f) ≫ sm.retraction
⊢ g = h
C : Type u₁
inst✝ : Category C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : g ≫ f = h ≫ f
⊢ g = h
replace w := w =≫ sm.retraction
no goals
C : Type u₁
inst✝ : Category C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : (g ≫ f) ≫ sm.retraction = (h ≫ f) ≫ sm.retraction
⊢ g = h
simpa using w