awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
rw : F.map (reflexion ≫ left) = 𝟙 (F.obj zero)
rw₁ : F.map (𝟙 zero) = 𝟙 (F.obj zero)
rw₂ rw₃ : Eq.{v + 1} (α := F.obj zero ⟶ F.obj zero) (𝟙 (F.obj zero)) (𝟙 (F.obj zero))
⊢ F.map reflexion ≫ F.map left = 𝟙 (F.obj zero)

Tactic:
rw [← F.map_comp, reflexion_comp_left, F.map_id]

Premises used: CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_left, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
rw : F.map (reflexion ≫ right) = 𝟙 (F.obj zero)
rw₁ : F.map (𝟙 zero) = 𝟙 (F.obj zero)
rw₂ rw₃ : Eq.{v + 1} (α := F.obj zero ⟶ F.obj zero) (𝟙 (F.obj zero)) (𝟙 (F.obj zero))
⊢ F.map reflexion ≫ F.map right = 𝟙 (F.obj zero)

Tactic:
rw [← F.map_comp, reflexion_comp_right, F.map_id]

Premises used: CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_right, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Nonempty (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)

Tactic:
⟨StructuredArrow.mk (Y := one) (𝟙 _)⟩

Premises used: CategoryTheory.CategoryStruct.id, Nonempty.intro, CategoryTheory.StructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Nonempty (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)

Tactic:
exact ⟨StructuredArrow.mk (Y := one) (𝟙 _)⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Nonempty (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)

Tactic:
⟨StructuredArrow.mk (Y := zero) (𝟙 _)⟩

Premises used: CategoryTheory.CategoryStruct.id, Nonempty.intro, CategoryTheory.StructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Nonempty (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)

Tactic:
exact ⟨StructuredArrow.mk (Y := zero) (𝟙 _)⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
X : WalkingReflexivePair
zero : Nonempty (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
one : Nonempty (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
⊢ Nonempty (StructuredArrow X inclusionWalkingReflexivePair)

Tactic:
cases X with
  | zero => exact ⟨StructuredArrow.mk (Y := one) (𝟙 _)⟩
  | one => exact ⟨StructuredArrow.mk (Y := zero) (𝟙 _)⟩

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsConnected (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)

Tactic:
IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_

Premises used: CategoryTheory.IsConnected.of_induct
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
zero :
  ∀ (p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)),
    StructuredArrow.mk (Y := one) (𝟙 WalkingReflexivePair.zero) ∈ p →
      (∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂),
          j₁ ∈ p ↔ j₂ ∈ p) →
        ∀ (j : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair), j ∈ p
⊢ IsConnected (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)

Tactic:
refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_

Premises used: CategoryTheory.IsConnected.of_induct
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := one) (𝟙 WalkingReflexivePair.zero) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := reflexion } ∈ p

Tactic:
(h₂ (StructuredArrow.homMk .left)).2 h₁

Premises used: CategoryTheory.StructuredArrow.homMk, Iff.mpr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := one) (𝟙 WalkingReflexivePair.zero) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := reflexion } ∈ p

Tactic:
exact (h₂ (StructuredArrow.homMk .left)).2 h₁

Premises used: CategoryTheory.StructuredArrow.homMk, Iff.mpr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := one) (𝟙 WalkingReflexivePair.zero) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ { left := { as := PUnit.unit }, right := one,
      hom :=
        Hom.id (Functor.obj (Functor.fromPUnit WalkingReflexivePair.zero) { as := PUnit.unit : Discrete PUnit.{1} }) } ∈
    p

Tactic:
h₁

Premises used: Set.Mem, CategoryTheory.StructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := one) (𝟙 WalkingReflexivePair.zero) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ { left := { as := PUnit.unit }, right := one,
      hom :=
        Hom.id (Functor.obj (Functor.fromPUnit WalkingReflexivePair.zero) { as := PUnit.unit : Discrete PUnit.{1} }) } ∈
    p

Tactic:
exact h₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsConnected (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)

Tactic:
IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := zero) (𝟙 _))
        (fun p h₁ h₂ ↦ ?_)

Premises used: CategoryTheory.IsConnected.of_induct
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
one :
  ∀ (p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair))
    (h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p)
    (h₂ :
      ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p)
    (j : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair), j ∈ p
⊢ IsConnected (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)

Tactic:
refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := zero) (𝟙 _))
        (fun p h₁ h₂ ↦ ?_)

Premises used: CategoryTheory.IsConnected.of_induct
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ StructuredArrow.mk (Y := one) left ∈ p

Tactic:
have hₗ : StructuredArrow.mk left ∈ p := (h₂ (StructuredArrow.homMk .left)).1 h₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk (Y := one) left ∈ p
⊢ StructuredArrow.mk (Y := one) right ∈ p

Tactic:
have hᵣ : StructuredArrow.mk right ∈ p := (h₂ (StructuredArrow.homMk .right)).1 h₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk (Y := one) left ∈ p
hᵣ : StructuredArrow.mk (Y := one) right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := leftCompReflexion } ∈ p

Tactic:
(h₂ (StructuredArrow.homMk .left)).2 hₗ

Premises used: CategoryTheory.StructuredArrow.homMk, Iff.mpr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk (Y := one) left ∈ p
hᵣ : StructuredArrow.mk (Y := one) right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := leftCompReflexion } ∈ p

Tactic:
exact (h₂ (StructuredArrow.homMk .left)).2 hₗ

Premises used: CategoryTheory.StructuredArrow.homMk, Iff.mpr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk (Y := one) left ∈ p
hᵣ : StructuredArrow.mk (Y := one) right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := rightCompReflexion } ∈ p

Tactic:
(h₂ (StructuredArrow.homMk .right)).2 hᵣ

Premises used: CategoryTheory.StructuredArrow.homMk, Iff.mpr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk (Y := one) left ∈ p
hᵣ : StructuredArrow.mk (Y := one) right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := rightCompReflexion } ∈ p

Tactic:
exact (h₂ (StructuredArrow.homMk .right)).2 hᵣ

Premises used: CategoryTheory.StructuredArrow.homMk, Iff.mpr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk (Y := one) left ∈ p
hᵣ : StructuredArrow.mk (Y := one) right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero,
      hom :=
        Hom.id (Functor.obj (Functor.fromPUnit WalkingReflexivePair.one) { as := PUnit.unit : Discrete PUnit.{1} }) } ∈
    p

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk (Y := one) left ∈ p
hᵣ : StructuredArrow.mk (Y := one) right ∈ p
⊢ { left := { as := PUnit.unit }, right := one, hom := left } ∈ p

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (Y := zero) (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk (Y := one) left ∈ p
hᵣ : StructuredArrow.mk (Y := one) right ∈ p
⊢ { left := { as := PUnit.unit }, right := one, hom := right } ∈ p

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
X : WalkingReflexivePair
zero : IsConnected (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
one : IsConnected (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
⊢ IsConnected (StructuredArrow X inclusionWalkingReflexivePair)

Tactic:
cases X with
  | zero =>
      refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_
      rintro p h₁ h₂ ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 h₁
      · exact h₁
  | one =>
      refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := zero) (𝟙 _))
        (fun p h₁ h₂ ↦ ?_)
      have hₗ : StructuredArrow.mk left ∈ p := (h₂ (StructuredArrow.homMk .left)).1 h₁
      have hᵣ : StructuredArrow.mk right ∈ p := (h₂ (StructuredArrow.homMk .right)).1 h₁
      rintro ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 hₗ
      · exact (h₂ (StructuredArrow.homMk .right)).2 hᵣ
      all_goals assumption

Premises used: CategoryTheory.IsConnected.of_induct, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.WalkingParallelPair.zero
-- 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.left ≫ 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) =
    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.left ≫ Hom.id zero 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.right ≫ 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) =
    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.right ≫ Hom.id zero 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
⊢ Eq.{v + 1} (α := B ⟶ 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, zero, Hom.reflexion ≫ 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 :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) zero with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) zero with
          | zero => B
          | one => A :
          C))
    (𝟙 B : B ⟶ B)

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
⊢ Eq.{v + 1} (α := B ⟶ 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, zero, Hom.reflexion ≫ 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 :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingReflexivePair → C) zero with
          | zero => B
          | one => A :
          C)
        (match (motive := WalkingReflexivePair → C) zero with
          | zero => B
          | one => A :
          C))
    (𝟙 B : B ⟶ B)

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.reflexion ≫ 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) =
    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))
      zero, one, Hom.reflexion ≫ 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) =
    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))
      zero, one, Hom.reflexion ≫ 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) =
    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.leftCompReflexion ≫ 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