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 : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone c)).ι.app
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone 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 : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone c)).ι.app
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone 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 : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone c)).ι.app
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone 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 : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone c)).ι.app
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone c)).pt).hom =
    (c.map G).ι.app WalkingParallelPair.one