awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
f : Opposite.op one ⟶ Opposite.op zero
g : unop (Opposite.op zero) ⟶ unop (Opposite.op one) := f.unop
this : f = g.op
op :
  Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op zero))
    (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op left))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op zero))))
    (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op one)))
      (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op left)))
op₁ :
  Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op zero))
    (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op right))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op zero))))
    (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op one)))
      (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op right)))
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op zero))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op zero)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op one)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
f : Opposite.op one ⟶ Opposite.op one
g : unop (Opposite.op one) ⟶ unop (Opposite.op one) := f.unop
this : f = g.op
op :
  Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one))
    (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (Opposite.op one)))))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op one))))
    (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op one)))
      (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op (WalkingParallelPairHom.id (unop (Opposite.op one))))))
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op one)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op one)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero))
    (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero)))))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op zero))))
    (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op zero)))
      (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero))))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero))
    (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op left))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op zero))))
    (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op one)))
      (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op left)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero))
    (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op right))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op zero))))
    (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op one)))
      (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op right)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
f : op one ⟶ op one
g : unop (op one) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one))
    (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
        (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one)))))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op one))))
    (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op one)))
      (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one))))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
j : WalkingParallelPair
zero :
  walkingParallelPairOp.map
        ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app
          WalkingParallelPair.zero) ≫
      NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso ⋯) ⋯))
        (walkingParallelPairOp.obj WalkingParallelPair.zero) =
    𝟙 (walkingParallelPairOp.obj WalkingParallelPair.zero)
one :
  walkingParallelPairOp.map
        ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app
          WalkingParallelPair.one) ≫
      NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso ⋯) ⋯))
        (walkingParallelPairOp.obj WalkingParallelPair.one) =
    𝟙 (walkingParallelPairOp.obj WalkingParallelPair.one)
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app
          j) ≫
      NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso ⋯) ⋯))
        (walkingParallelPairOp.obj j) =
    𝟙 (walkingParallelPairOp.obj j)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app
          zero) ≫
      NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso ⋯) ⋯))
        (walkingParallelPairOp.obj zero) =
    𝟙 (walkingParallelPairOp.obj zero)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app
          one) ≫
      NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso ⋯) ⋯))
        (walkingParallelPairOp.obj one) =
    𝟙 (walkingParallelPairOp.obj one)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.unitIso.app zero = Iso.refl zero

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.unitIso.app one = Iso.refl one

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ Eq (α :=
    (walkingParallelPairOpEquiv.inverse ⋙ walkingParallelPairOpEquiv.functor).obj (op zero) ≅
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero))
    (walkingParallelPairOpEquiv.counitIso.app (op zero)) (Iso.refl (op zero))

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ Eq (α :=
    (walkingParallelPairOpEquiv.inverse ⋙ walkingParallelPairOpEquiv.functor).obj (op one) ≅
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one))
    (walkingParallelPairOpEquiv.counitIso.app (op one)) (Iso.refl (op one))

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.unitIso.hom.app zero = 𝟙 zero

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.unitIso.hom.app one = 𝟙 one

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.unitIso.inv.app zero = 𝟙 zero

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.unitIso.inv.app one = 𝟙 one

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.counitIso.hom.app (op zero) = 𝟙 (op zero)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.counitIso.hom.app (op one) = 𝟙 (op one)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.counitIso.inv.app (op zero) = 𝟙 (op zero)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOpEquiv.counitIso.inv.app (op one) = 𝟙 (op one)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f g).obj zero = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f g).obj one = Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f g).map left = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ (parallelPair f g).map right = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
j : WalkingParallelPair
zero : (parallelPair (F.map left) (F.map right)).obj WalkingParallelPair.zero = F.obj WalkingParallelPair.zero
one : (parallelPair (F.map left) (F.map right)).obj WalkingParallelPair.one = F.obj WalkingParallelPair.one
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ (parallelPair (F.map left) (F.map right)).obj zero = F.obj zero

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ (parallelPair (F.map left) (F.map right)).obj one = F.obj one

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F : Functor.{0, v, 0, u} WalkingParallelPair C
j : WalkingParallelPair
zero : F.obj WalkingParallelPair.zero = (parallelPair (F.map left) (F.map right)).obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one = (parallelPair (F.map left) (F.map right)).obj WalkingParallelPair.one
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ F.obj zero = (parallelPair (F.map left) (F.map right)).obj zero

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ F.obj one = (parallelPair (F.map left) (F.map right)).obj one

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ F.map left ≫
      Iso.hom
        ((fun (j : WalkingParallelPair) ↦ (eqToIso ⋯ : F.obj j ≅ (parallelPair (F.map left) (F.map right)).obj j))
          one) =
    Iso.hom
        ((fun (j : WalkingParallelPair) ↦ (eqToIso ⋯ : F.obj j ≅ (parallelPair (F.map left) (F.map right)).obj j))
          zero) ≫
      (parallelPair (F.map left) (F.map right)).map left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ F.map right ≫
      Iso.hom
        ((fun (j : WalkingParallelPair) ↦ (eqToIso ⋯ : F.obj j ≅ (parallelPair (F.map left) (F.map right)).obj j))
          one) =
    Iso.hom
        ((fun (j : WalkingParallelPair) ↦ (eqToIso ⋯ : F.obj j ≅ (parallelPair (F.map left) (F.map right)).obj j))
          zero) ≫
      (parallelPair (F.map left) (F.map right)).map right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F : Functor.{0, v, 0, u} WalkingParallelPair C
X_1 : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X_1) ≫
      Iso.hom
        ((fun (j : WalkingParallelPair) ↦ (eqToIso ⋯ : F.obj j ≅ (parallelPair (F.map left) (F.map right)).obj j))
          X_1) =
    Iso.hom
        ((fun (j : WalkingParallelPair) ↦ (eqToIso ⋯ : F.obj j ≅ (parallelPair (F.map left) (F.map right)).obj j))
          X_1) ≫
      (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X_1)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F G : Functor.{0, v, 0, u} WalkingParallelPair C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.obj zero ⟶ G.obj zero

Tactic:
exacts [p, q]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F G : Functor.{0, v, 0, u} WalkingParallelPair C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.obj zero ≅ G.obj zero

Tactic:
exacts [p, q]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y X' Y' : C
f g : X ⟶ Y
f' g' : X' ⟶ Y'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
⊢ (parallelPairHom f g f' g' p q wf wg).app zero = p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y X' Y' : C
f g : X ⟶ Y
f' g' : X' ⟶ Y'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
⊢ (parallelPairHom f g f' g' p q wf wg).app one = q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F G : Functor.{0, v, 0, u} WalkingParallelPair C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero

Tactic:
exacts [zero, one]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F G : Functor.{0, v, 0, u} WalkingParallelPair C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ Eq (α := F.obj WalkingParallelPair.zero ⟶ G.obj WalkingParallelPair.one)
    (F.map WalkingParallelPairHom.left ≫
      Iso.hom
        (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦ F.obj x ≅ G.obj x)
          WalkingParallelPair.one zero one))
    (Iso.hom
        (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦ F.obj x ≅ G.obj x)
          WalkingParallelPair.zero zero one) ≫
      G.map WalkingParallelPairHom.left)

Tactic:
simp [left, right]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F G : Functor.{0, v, 0, u} WalkingParallelPair C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ Eq (α := F.obj WalkingParallelPair.zero ⟶ G.obj WalkingParallelPair.one)
    (F.map WalkingParallelPairHom.right ≫
      Iso.hom
        (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦ F.obj x ≅ G.obj x)
          WalkingParallelPair.one zero one))
    (Iso.hom
        (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦ F.obj x ≅ G.obj x)
          WalkingParallelPair.zero zero one) ≫
      G.map WalkingParallelPairHom.right)

Tactic:
simp [left, right]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F G : Functor.{0, v, 0, u} WalkingParallelPair C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
X_1 : WalkingParallelPair
⊢ Eq (α := F.obj X_1 ⟶ G.obj X_1)
    (F.map (WalkingParallelPairHom.id X_1) ≫
      Iso.hom (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦ F.obj x ≅ G.obj x) X_1 zero one))
    (Iso.hom (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦ F.obj x ≅ G.obj x) X_1 zero one) ≫
      G.map (WalkingParallelPairHom.id X_1))

Tactic:
simp [left, right]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g f' g' : X ⟶ Y
hf : f = f'
hg : g = g'
⊢ (parallelPair f g).map left ≫ Iso.hom (Iso.refl ((parallelPair f g).obj one)) =
    Iso.hom (Iso.refl ((parallelPair f g).obj zero)) ≫ (parallelPair f' g').map left

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g f' g' : X ⟶ Y
hf : f = f'
hg : g = g'
⊢ (parallelPair f g).map right ≫ Iso.hom (Iso.refl ((parallelPair f g).obj one)) =
    Iso.hom (Iso.refl ((parallelPair f g).obj zero)) ≫ (parallelPair f' g').map right

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Fork f g
⊢ t.π.app zero = t.ι

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl