case h
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasCokernel f✝
X Y Z X' Y' Z' : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ coequalizer.π f 0 ≫ map f f' p q h₁ ≫ desc f' g' w' = coequalizer.π f 0 ≫ desc f g w ≫ r
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasCokernel f✝
X Y Z X' Y' Z' : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ map f f' p q h₁ ≫ desc f' g' w' = desc f g w ≫ r
apply coequalizer.hom_ext
no goals
case h
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasCokernel f✝
X Y Z X' Y' Z' : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ coequalizer.π f 0 ≫ map f f' p q h₁ ≫ desc f' g' w' = coequalizer.π f 0 ≫ desc f g w ≫ r
simp [h₂]