𝒜 : Type u_1
inst✝² : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
this : Mono f
⊢ section h' ≫ retraction h = -section h ≫ retraction h'
𝒜 : Type u_1
inst✝² : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
⊢ section h' ≫ retraction h = -section h ≫ retraction h'
haveI := h.mono
𝒜 : Type u_1
inst✝² : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
this : Mono f
⊢ (section h' ≫ retraction h) ≫ f = (-section h ≫ retraction h') ≫ f
𝒜 : Type u_1
inst✝² : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
this : Mono f
⊢ section h' ≫ retraction h = -section h ≫ retraction h'
rw [← cancel_mono f]
no goals
𝒜 : Type u_1
inst✝² : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
this : Mono f
⊢ (section h' ≫ retraction h) ≫ f = (-section h ≫ retraction h') ≫ f
simp [retraction_ι_eq_id_sub]