Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ ∀ {X_1 Y_1 : WalkingParallelPair} (f_1 : X_1 ⟶ Y_1),
    (parallelPair f.op g.op).map f_1 ≫
        (match Y_1 with
          | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
          | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
      (match X_1 with
          | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
          | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
        (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map f_1

Tactic:
rintro (_ | _ | _) (_ | _ | _) f <;> cases f

Goal state after:
case zero.zero.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map
        (WalkingParallelPairHom.id WalkingParallelPair.zero)

case zero.one.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map WalkingParallelPairHom.left ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map WalkingParallelPairHom.left

case zero.one.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map WalkingParallelPairHom.right ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.zero with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map WalkingParallelPairHom.right

case one.one.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f.op g.op).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
    (match WalkingParallelPair.one with
        | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
        | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map
        (WalkingParallelPairHom.id WalkingParallelPair.one)