-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g))
      (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
        (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
      (Iso.inv (PreservesCokernel.iso G g)))
    (G.map (cokernel.map f g p q hpq))
rw₁ :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
        (Iso.inv (PreservesCokernel.iso G g))))
    (G.map (cokernel.map f g p q hpq))
rw₂ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesCokernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
      (G.map (cokernel.map f g p q hpq)))
rw₃ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (cokernelComparison g G))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
      (G.map (cokernel.map f g p q hpq)))
rw₄ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.map f g p q hpq)))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
      (G.map (cokernel.map f g p q hpq)))
hpq₁ : f ≫ q = p ≫ g
rw₅ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.map f g p q hpq)))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.map f g p q hpq)))
hpq₂ : f ≫ q = p ≫ g
rw₆ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.map f g p q hpq)))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.map f g p q hpq)))
hpq₃ : f ≫ q = p ≫ g
⊢ Eq (α := G.obj (cokernel f) ⟶ cokernel (G.map g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (cokernel g)) (G.map (cokernel.map f g p q hpq))
      (Iso.hom (PreservesCokernel.iso G g)))

Tactic:
rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
    cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.PreservesCokernel.iso_inv, CategoryTheory.Limits.cokernel_map_comp_cokernelComparison, CategoryTheory.Iso.eq_inv_comp