Horizontal maps in a pullback square have the same kernel

Consider a commutative square:

    t
 X₁ --> X₂
l|      |r
 v      v
 X₃ --> X₄
    b

• If this is a pullback square, then the induced map kernel t ⟶ kernel b is an isomorphism.
• If this is a pushout square, then the induced map cokernel t ⟶ cokernel b is an isomorphism.

(Similar results for the (co)kernels of the vertical maps can be obtained by applying these results to the flipped square.)

theorem CategoryTheory.Limits.isIso_kernel_map_of_isPullback {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} [HasKernel t] [HasKernel b] (sq : IsPullback t l r b) : IsIso (kernel.map t b l r ⋯)

theorem CategoryTheory.Limits.isIso_cokernel_map_of_isPushout {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} [HasCokernel t] [HasCokernel b] (sq : IsPushout t l r b) : IsIso (cokernel.map t b l r ⋯)