Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case id
X✝ Z✝ : WalkingParallelPair
g : X✝ ⟶ Z✝
⊢ (match Z✝, X✝, WalkingParallelPairHom.id X✝ ≫ g with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match X✝, X✝, WalkingParallelPairHom.id X✝ with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match Z✝, X✝, g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

Tactic:
cases g

Goal state after:
case id.left
⊢ (match one, zero, WalkingParallelPairHom.id zero ≫ WalkingParallelPairHom.left with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match zero, zero, WalkingParallelPairHom.id zero with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match one, zero, WalkingParallelPairHom.left with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

case id.right
⊢ (match one, zero, WalkingParallelPairHom.id zero ≫ WalkingParallelPairHom.right with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match zero, zero, WalkingParallelPairHom.id zero with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match one, zero, WalkingParallelPairHom.right with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

case id.id
X✝ : WalkingParallelPair
⊢ (match X✝, X✝, WalkingParallelPairHom.id X✝ ≫ WalkingParallelPairHom.id X✝ with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match X✝, X✝, WalkingParallelPairHom.id X✝ with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match X✝, X✝, WalkingParallelPairHom.id X✝ with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)