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

Goal state before:
pp: case zero.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.zero
⊢ (parallelPair f✝.op g.op).map f ≫
      (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 f

pp: case zero.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.one
⊢ (parallelPair f✝.op g.op).map f ≫
      (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 f

pp: case one.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.one ⟶ WalkingParallelPair.zero
⊢ (parallelPair f✝.op g.op).map f ≫
      (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.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 f

pp: case one.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.one ⟶ WalkingParallelPair.one
⊢ (parallelPair f✝.op g.op).map f ≫
      (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 f

Tactic:
<;>

Goal state after:
case zero.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.zero
⊢ (parallelPair f✝.op g.op).map f ≫
      (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 f

case zero.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.one
⊢ (parallelPair f✝.op g.op).map f ≫
      (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 f

case one.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.one ⟶ WalkingParallelPair.zero
⊢ (parallelPair f✝.op g.op).map f ≫
      (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.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 f

case one.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f✝ g : X ⟶ Y
f : WalkingParallelPair.one ⟶ WalkingParallelPair.one
⊢ (parallelPair f✝.op g.op).map f ≫
      (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 f