awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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.leftCompReflexion ≫ 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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 ≫ 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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 ≫ 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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 ≫ Hom.id one 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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.id one 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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.id one ≫ 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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.id one ≫ 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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))
      zero, one, Hom.id zero ≫ Hom.reflexion 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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.id 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    f ≫ s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (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.id 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
    | .(zero), .(one), Hom.reflexion => s
    | .(one), .(one), Hom.rightCompReflexion => g ≫ s
    | .(one), .(one), Hom.leftCompReflexion => f ≫ s) =
    g ≫ s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
X : WalkingReflexivePair
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingReflexivePair → C) X with
        | zero => B
        | one => A :
        C)
      (match (motive := WalkingReflexivePair → C) X 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))
        X, X, Hom.id X ≫ Hom.id X 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
      | .(zero), .(one), Hom.reflexion => s
      | .(one), .(one), Hom.rightCompReflexion => g ≫ s
      | .(one), .(one), Hom.leftCompReflexion => f ≫ s :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) X with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) X with
          | zero => B
          | one => A :
          C))
    (𝟙
        (match (motive := WalkingReflexivePair → C) X with
        | zero => B
        | one => A) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) X with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) X with
          | zero => B
          | one => A :
          C))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (reflexivePair f g s sl sr).obj zero = B

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (reflexivePair f g s sl sr).obj one = A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (reflexivePair f g s sl sr).map Hom.left = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (reflexivePair f g s sl sr).map Hom.right = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
⊢ (reflexivePair f g s sl sr).map Hom.reflexion = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsReflexivePair f g
⊢ (ofIsReflexivePair f g).map Hom.left = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsReflexivePair f g
⊢ (ofIsReflexivePair f g).map Hom.right = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map Hom.left ≫ e₀ = e₁ ≫ G.map Hom.left
h₂ : F.map Hom.right ≫ e₀ = e₁ ≫ G.map Hom.right
h₃ : F.map Hom.reflexion ≫ e₁ = e₀ ≫ G.map Hom.reflexion
x x_1 : WalkingReflexivePair
f : x ⟶ x_1
left :
  Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.left ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.left)
right :
  Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.right ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.right)
reflexion :
  Eq (α := F.obj zero ⟶ G.obj one)
    (F.map Hom.reflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.reflexion)
leftCompReflexion :
  Eq (α := F.obj one ⟶ G.obj one)
    (F.map Hom.leftCompReflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.leftCompReflexion)
rightCompReflexion :
  Eq (α := F.obj one ⟶ G.obj one)
    (F.map Hom.rightCompReflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.rightCompReflexion)
id :
  Eq (α := F.obj x ⟶ G.obj x)
    (F.map (Hom.id x) ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
      | zero => e₀
      | one => e₁) ≫
      G.map (Hom.id x))
⊢ Eq (α := F.obj x ⟶ G.obj x_1)
    (F.map f ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x_1 with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
      | zero => e₀
      | one => e₁) ≫
      G.map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map Hom.left ≫ e₀ = e₁ ≫ G.map Hom.left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
left : F.map Hom.left ≫ e₀ = e₁ ≫ G.map Hom.left
⊢ Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.left ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.left)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ F.map left ≫ e₀ = e₁ ≫ G.map left

Tactic:
simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map Hom.right ≫ e₀ = e₁ ≫ G.map Hom.right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
right : F.map Hom.right ≫ e₀ = e₁ ≫ G.map Hom.right
⊢ Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.right ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.right)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ F.map right ≫ e₀ = e₁ ≫ G.map right

Tactic:
simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ reflexion : F.map Hom.reflexion ≫ e₁ = e₀ ≫ G.map Hom.reflexion
⊢ Eq (α := F.obj zero ⟶ G.obj one)
    (F.map Hom.reflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.reflexion)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion

Tactic:
simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp