case h
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : ConcreteCategory C
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : (forget C).obj N),
    (forget C).map g ((forget C).map (cokernel.π f) n) = (forget C).map h ((forget C).map (cokernel.π f) n)
⊢ coequalizer.π f 0 ≫ g = coequalizer.π f 0 ≫ h
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : ConcreteCategory C
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : (forget C).obj N),
    (forget C).map g ((forget C).map (cokernel.π f) n) = (forget C).map h ((forget C).map (cokernel.π f) n)
⊢ g = h
apply coequalizer.hom_ext
case h
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : ConcreteCategory C
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : (forget C).obj N),
    (forget C).map g ((forget C).map (cokernel.π f) n) = (forget C).map h ((forget C).map (cokernel.π f) n)
⊢ ∀ (x : (forget C).obj N), (forget C).map (coequalizer.π f 0 ≫ g) x = (forget C).map (coequalizer.π f 0 ≫ h) x
case h
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : ConcreteCategory C
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : (forget C).obj N),
    (forget C).map g ((forget C).map (cokernel.π f) n) = (forget C).map h ((forget C).map (cokernel.π f) n)
⊢ coequalizer.π f 0 ≫ g = coequalizer.π f 0 ≫ h
apply ConcreteCategory.hom_ext _ _
no goals
case h
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : ConcreteCategory C
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : (forget C).obj N),
    (forget C).map g ((forget C).map (cokernel.π f) n) = (forget C).map h ((forget C).map (cokernel.π f) n)
⊢ ∀ (x : (forget C).obj N), (forget C).map (coequalizer.π f 0 ≫ g) x = (forget C).map (coequalizer.π f 0 ≫ h) x
simpa using w