-- 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 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasKernel g
inst_9 : HasKernel (G.map g)
inst_10 : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel g))
      (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
      (Iso.hom (PreservesKernel.iso G g)))
rw₁ :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
      (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq))
        (Iso.hom (PreservesKernel.iso G g))))
rw₂ :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
      (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G)))
rw₃ :
  Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
    (CategoryStruct.comp (Y := kernel (G.map f)) (Iso.hom (PreservesKernel.iso G f))
      (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
rw₄ :
  Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
    (CategoryStruct.comp (Y := kernel (G.map f)) (kernelComparison f G)
      (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
rw₅ :
  Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
hpq₁ : f ≫ q = p ≫ g
rw₆ :
  Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
hpq₂ : f ≫ q = p ≫ g
⊢ Eq (α := kernel (G.map f) ⟶ G.obj (kernel g))
    (CategoryStruct.comp (Y := kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesKernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp,
    PreservesKernel.iso_hom, kernelComparison_comp_kernel_map]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.kernelComparison_comp_kernel_map, CategoryTheory.Limits.PreservesKernel.iso_hom, CategoryTheory.Iso.eq_inv_comp