-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g_1 : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g_1 = 𝟙 B
Z : WalkingReflexivePair
g : one ⟶ Z
rightCompReflexion :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A :
        C)
      (match (motive := WalkingReflexivePair → C) zero with
        | zero => B
        | one => A :
        C))
    (match (motive :=
        (X Y : WalkingReflexivePair) →
          (X ⟶ Y) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingReflexivePair → C) X with
                | zero => B
                | one => A :
                C)
              (match (motive := WalkingReflexivePair → C) Y with
                | zero => B
                | one => A :
                C))
        one, zero, Hom.rightCompReflexion ≫ Hom.left with
      | x, .(x), Hom.id .(x) =>
        𝟙
          (match (motive := WalkingReflexivePair → C) x with
          | zero => B
          | one => A)
      | .(one), .(zero), Hom.left => f
      | .(one), .(zero), Hom.right => g_1
      | .(zero), .(one), Hom.reflexion => s
      | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
      | .(one), .(one), Hom.leftCompReflexion => f ≫ s :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) zero with
          | zero => B
          | one => A :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A)
        (match (motive :=
          (X Y : WalkingReflexivePair) →
            (X ⟶ Y) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingReflexivePair → C) X with
                  | zero => B
                  | one => A :
                  C)
                (match (motive := WalkingReflexivePair → C) Y with
                  | zero => B
                  | one => A :
                  C))
          one, one, Hom.rightCompReflexion with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match (motive := WalkingReflexivePair → C) x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g_1
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s)
        (match (motive :=
          (X Y : WalkingReflexivePair) →
            (X ⟶ Y) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingReflexivePair → C) X with
                  | zero => B
                  | one => A :
                  C)
                (match (motive := WalkingReflexivePair → C) Y with
                  | zero => B
                  | one => A :
                  C))
          one, zero, Hom.left with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match (motive := WalkingReflexivePair → C) x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g_1
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) zero with
          | zero => B
          | one => A :
          C))
rightCompReflexion₁ :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A :
        C)
      (match (motive := WalkingReflexivePair → C) zero with
        | zero => B
        | one => A :
        C))
    (match (motive :=
        (X Y : WalkingReflexivePair) →
          (X ⟶ Y) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingReflexivePair → C) X with
                | zero => B
                | one => A :
                C)
              (match (motive := WalkingReflexivePair → C) Y with
                | zero => B
                | one => A :
                C))
        one, zero, Hom.rightCompReflexion ≫ Hom.right with
      | x, .(x), Hom.id .(x) =>
        𝟙
          (match (motive := WalkingReflexivePair → C) x with
          | zero => B
          | one => A)
      | .(one), .(zero), Hom.left => f
      | .(one), .(zero), Hom.right => g_1
      | .(zero), .(one), Hom.reflexion => s
      | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
      | .(one), .(one), Hom.leftCompReflexion => f ≫ s :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) zero with
          | zero => B
          | one => A :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A)
        (match (motive :=
          (X Y : WalkingReflexivePair) →
            (X ⟶ Y) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingReflexivePair → C) X with
                  | zero => B
                  | one => A :
                  C)
                (match (motive := WalkingReflexivePair → C) Y with
                  | zero => B
                  | one => A :
                  C))
          one, one, Hom.rightCompReflexion with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match (motive := WalkingReflexivePair → C) x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g_1
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s)
        (match (motive :=
          (X Y : WalkingReflexivePair) →
            (X ⟶ Y) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingReflexivePair → C) X with
                  | zero => B
                  | one => A :
                  C)
                (match (motive := WalkingReflexivePair → C) Y with
                  | zero => B
                  | one => A :
                  C))
          one, zero, Hom.right with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match (motive := WalkingReflexivePair → C) x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g_1
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) zero with
          | zero => B
          | one => A :
          C))
rightCompReflexion₂ :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A :
        C)
      (match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A :
        C))
    (match (motive :=
        (X Y : WalkingReflexivePair) →
          (X ⟶ Y) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingReflexivePair → C) X with
                | zero => B
                | one => A :
                C)
              (match (motive := WalkingReflexivePair → C) Y with
                | zero => B
                | one => A :
                C))
        one, one, Hom.rightCompReflexion ≫ Hom.leftCompReflexion with
      | x, .(x), Hom.id .(x) =>
        𝟙
          (match (motive := WalkingReflexivePair → C) x with
          | zero => B
          | one => A)
      | .(one), .(zero), Hom.left => f
      | .(one), .(zero), Hom.right => g_1
      | .(zero), .(one), Hom.reflexion => s
      | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
      | .(one), .(one), Hom.leftCompReflexion => f ≫ s :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A)
        (match (motive :=
          (X Y : WalkingReflexivePair) →
            (X ⟶ Y) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingReflexivePair → C) X with
                  | zero => B
                  | one => A :
                  C)
                (match (motive := WalkingReflexivePair → C) Y with
                  | zero => B
                  | one => A :
                  C))
          one, one, Hom.rightCompReflexion with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match (motive := WalkingReflexivePair → C) x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g_1
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s)
        (match (motive :=
          (X Y : WalkingReflexivePair) →
            (X ⟶ Y) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingReflexivePair → C) X with
                  | zero => B
                  | one => A :
                  C)
                (match (motive := WalkingReflexivePair → C) Y with
                  | zero => B
                  | one => A :
                  C))
          one, one, Hom.leftCompReflexion with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match (motive := WalkingReflexivePair → C) x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g_1
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A :
        C)
      (match (motive := WalkingReflexivePair → C) Z with
        | zero => B
        | one => A :
        C))
    (match (motive :=
        (X Y : WalkingReflexivePair) →
          (X ⟶ Y) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingReflexivePair → C) X with
                | zero => B
                | one => A :
                C)
              (match (motive := WalkingReflexivePair → C) Y with
                | zero => B
                | one => A :
                C))
        one, Z, Hom.rightCompReflexion ≫ g with
      | x, .(x), Hom.id .(x) =>
        𝟙
          (match (motive := WalkingReflexivePair → C) x with
          | zero => B
          | one => A)
      | .(one), .(zero), Hom.left => f
      | .(one), .(zero), Hom.right => g_1
      | .(zero), .(one), Hom.reflexion => s
      | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
      | .(one), .(one), Hom.leftCompReflexion => f ≫ s :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) Z with
          | zero => B
          | one => A :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A)
        (match (motive :=
          (X Y : WalkingReflexivePair) →
            (X ⟶ Y) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingReflexivePair → C) X with
                  | zero => B
                  | one => A :
                  C)
                (match (motive := WalkingReflexivePair → C) Y with
                  | zero => B
                  | one => A :
                  C))
          one, one, Hom.rightCompReflexion with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match (motive := WalkingReflexivePair → C) x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g_1
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s)
        (match (motive :=
          (X Y : WalkingReflexivePair) →
            (X ⟶ Y) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingReflexivePair → C) X with
                  | zero => B
                  | one => A :
                  C)
                (match (motive := WalkingReflexivePair → C) Y with
                  | zero => B
                  | one => A :
                  C))
          one, Z, g with
        | x, .(x), Hom.id .(x) =>
          𝟙
            (match (motive := WalkingReflexivePair → C) x with
            | zero => B
            | one => A)
        | .(one), .(zero), Hom.left => f
        | .(one), .(zero), Hom.right => g_1
        | .(zero), .(one), Hom.reflexion => s
        | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
        | .(one), .(one), Hom.leftCompReflexion => f ≫ s) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) one with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) Z with
          | zero => B
          | one => A :
          C))
have rightCompReflexion₃ : Eq.{v + 1} (α :=
  Quiver.Hom.{v, u} (V := C)
    (match (motive := WalkingReflexivePair → C) one with
      | zero => B
      | one => A :
      C)
    (match (motive := WalkingReflexivePair → C) one with
      | zero => B
      | one => A :
      C))
  (match (motive :=
      (X Y : WalkingReflexivePair) →
        (X ⟶ Y) →
          Quiver.Hom.{v, u} (V := C)
            (match (motive := WalkingReflexivePair → C) X with
              | zero => B
              | one => A :
              C)
            (match (motive := WalkingReflexivePair → C) Y with
              | zero => B
              | one => A :
              C))
      one, one, Hom.rightCompReflexion ≫ Hom.rightCompReflexion with
    | x, .(x), Hom.id .(x) =>
      𝟙
        (match (motive := WalkingReflexivePair → C) x with
        | zero => B
        | one => A)
    | .(one), .(zero), Hom.left => f
    | .(one), .(zero), Hom.right => g_1
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s :
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A :
        C)
      (match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A :
        C))
  (CategoryStruct.comp (Y :=
      match (motive := WalkingReflexivePair → C) one with
      | zero => B
      | one => A)
      (match (motive :=
        (X Y : WalkingReflexivePair) →
          (X ⟶ Y) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingReflexivePair → C) X with
                | zero => B
                | one => A :
                C)
              (match (motive := WalkingReflexivePair → C) Y with
                | zero => B
                | one => A :
                C))
        one, one, Hom.rightCompReflexion with
      | x, .(x), Hom.id .(x) =>
        𝟙
          (match (motive := WalkingReflexivePair → C) x with
          | zero => B
          | one => A)
      | .(one), .(zero), Hom.left => f
      | .(one), .(zero), Hom.right => g_1
      | .(zero), .(one), Hom.reflexion => s
      | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
      | .(one), .(one), Hom.leftCompReflexion => f ≫ s)
      (match (motive :=
        (X Y : WalkingReflexivePair) →
          (X ⟶ Y) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingReflexivePair → C) X with
                | zero => B
                | one => A :
                C)
              (match (motive := WalkingReflexivePair → C) Y with
                | zero => B
                | one => A :
                C))
        one, one, Hom.rightCompReflexion with
      | x, .(x), Hom.id .(x) =>
        𝟙
          (match (motive := WalkingReflexivePair → C) x with
          | zero => B
          | one => A)
      | .(one), .(zero), Hom.left => f
      | .(one), .(zero), Hom.right => g_1
      | .(zero), .(one), Hom.reflexion => s
      | .(one), .(one), Hom.rightCompReflexion => g_1 ≫ s
      | .(one), .(one), Hom.leftCompReflexion => f ≫ s) :
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A :
        C)
      (match (motive := WalkingReflexivePair → C) one with
        | zero => B
        | one => A :
        C))
Tactic: cases g
Cleared hypotheses: Z, g