Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left
Z✝ : WalkingParallelPair
g : one ⟶ Z✝
⊢ (match Z✝, zero, WalkingParallelPairHom.left ≫ 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 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)) ≫
      match Z✝, one, 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)

pp: case right
Z✝ : WalkingParallelPair
g : one ⟶ Z✝
⊢ (match Z✝, zero, WalkingParallelPairHom.right ≫ 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 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)) ≫
      match Z✝, one, 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)

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:
<;>

Goal state after:
case left
Z✝ : WalkingParallelPair
g : one ⟶ Z✝
⊢ (match Z✝, zero, WalkingParallelPairHom.left ≫ 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 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)) ≫
      match Z✝, one, 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)

case right
Z✝ : WalkingParallelPair
g : one ⟶ Z✝
⊢ (match Z✝, zero, WalkingParallelPairHom.right ≫ 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 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)) ≫
      match Z✝, one, 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)

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)