Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: case zero
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cone.postcompose
                (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
            (G.mapCone c)).π.app
      WalkingParallelPair.zero =
    (Iso.refl
          ((Cone.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCone c)).pt).hom ≫
      (c.map G).π.app WalkingParallelPair.zero

pp: case one
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cone.postcompose
                (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
            (G.mapCone c)).π.app
      WalkingParallelPair.one =
    (Iso.refl
          ((Cone.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCone c)).pt).hom ≫
      (c.map G).π.app WalkingParallelPair.one

Tactic:
<;>

Goal state after:
case zero
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cone.postcompose
                (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
            (G.mapCone c)).π.app
      WalkingParallelPair.zero =
    (Iso.refl
          ((Cone.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCone c)).pt).hom ≫
      (c.map G).π.app WalkingParallelPair.zero

case one
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cone.postcompose
                (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
            (G.mapCone c)).π.app
      WalkingParallelPair.one =
    (Iso.refl
          ((Cone.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCone c)).pt).hom ≫
      (c.map G).π.app WalkingParallelPair.one