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

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