awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
X : WalkingParallelPair
id :
  Quiver.Hom (V := WalkingParallelPair)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
        (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯ :
      WalkingParallelPair)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
        (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯ :
      WalkingParallelPair)
⊢ Quiver.Hom (V := WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
          (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
          (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)

Tactic:
apply Quiver.Hom.op

Premises used: Quiver.Hom.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ Quiver.Hom (V := WalkingParallelPair)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair) one
        (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) ⋯ :
      WalkingParallelPair)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair) zero
        (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) ⋯ :
      WalkingParallelPair)

Tactic:
exacts [left, right, WalkingParallelPairHom.id _]

Premises used: CategoryTheory.Limits.WalkingParallelPairHom.right, CategoryTheory.Limits.WalkingParallelPairHom.id, CategoryTheory.Limits.WalkingParallelPairHom.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOp.obj zero = op one

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOp.obj one = op zero

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOp.map left = Quiver.Hom.op left

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ walkingParallelPairOp.map right = Quiver.Hom.op right

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
j : WalkingParallelPair
zero :
  Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.zero =
    (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj WalkingParallelPair.zero
one :
  Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.one =
    (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj WalkingParallelPair.one
⊢ Functor.obj (𝟭 WalkingParallelPair) j = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ Functor.obj (𝟭 WalkingParallelPair) zero = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj zero

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ Functor.obj (𝟭 WalkingParallelPair) one = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj one

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ Eq (α := Functor.obj (𝟭 WalkingParallelPair) zero ⟶ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj one)
    (Functor.map (𝟭 WalkingParallelPair) left ≫
      Iso.hom
        ((fun (j : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj (𝟭 WalkingParallelPair) j ≅ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j))
          one))
    (Iso.hom
        ((fun (j : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj (𝟭 WalkingParallelPair) j ≅ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j))
          zero) ≫
      (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map left)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ Eq (α := Functor.obj (𝟭 WalkingParallelPair) zero ⟶ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj one)
    (Functor.map (𝟭 WalkingParallelPair) right ≫
      Iso.hom
        ((fun (j : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj (𝟭 WalkingParallelPair) j ≅ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j))
          one))
    (Iso.hom
        ((fun (j : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj (𝟭 WalkingParallelPair) j ≅ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j))
          zero) ≫
      (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
X : WalkingParallelPair
⊢ Eq (α := Functor.obj (𝟭 WalkingParallelPair) X ⟶ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj X)
    (Functor.map (𝟭 WalkingParallelPair) (WalkingParallelPairHom.id X) ≫
      Iso.hom
        ((fun (j : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj (𝟭 WalkingParallelPair) j ≅ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j))
          X))
    (Iso.hom
        ((fun (j : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj (𝟭 WalkingParallelPair) j ≅ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j))
          X) ≫
      (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map (WalkingParallelPairHom.id X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
j : WalkingParallelPairᵒᵖ
op :
  ∀ (X : WalkingParallelPair),
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op X) =
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op X)
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j = Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j

Tactic:
induction j with | _ X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
X : WalkingParallelPair
op :
  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) =
    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op zero)
op₁ :
  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) =
    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one)
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op X) =
    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op X)

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) = Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) = Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
i j : WalkingParallelPairᵒᵖ
f : i ⟶ j
op :
  ∀ (i : WalkingParallelPair) (f : Opposite.op i ⟶ j),
    Eq (α :=
      (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op i) ⟶
        Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j)
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
        Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso ⋯ :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            j))
      (Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso ⋯ :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (Opposite.op i)) ≫
        Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)
⊢ Eq (α := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj i ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j)
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          j))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          i) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)

Tactic:
induction i with | _ i
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
j : WalkingParallelPairᵒᵖ
i : WalkingParallelPair
f : Opposite.op i ⟶ j
op :
  ∀ (j : WalkingParallelPair) (f : Opposite.op i ⟶ Opposite.op j),
    Eq (α :=
      (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op i) ⟶
        Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
        Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso ⋯ :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (Opposite.op j)))
      (Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso ⋯ :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (Opposite.op i)) ≫
        Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op i) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j)
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          j))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)

Tactic:
induction j with | _ j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
⊢ f = g.op

Tactic:
have : f = g.op := rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
i j : WalkingParallelPair
f : Opposite.op i ⟶ Opposite.op j
g : unop (Opposite.op j) ⟶ unop (Opposite.op i) := f.unop
this : f = g.op
op :
  Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op i) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op i) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
i j : WalkingParallelPair
f : Opposite.op i ⟶ Opposite.op j
g : unop (Opposite.op j) ⟶ unop (Opposite.op i) := f.unop
this : f = g.op
op :
  ∀ (f : Opposite.op zero ⟶ Opposite.op j),
    let g := f.unop;
    ∀ (this : f = g.op),
      Eq (α :=
        (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) ⟶
          Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
        ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
          Iso.hom
            ((fun (j : WalkingParallelPairᵒᵖ) ↦
                (eqToIso ⋯ :
                  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅
                    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
              (Opposite.op j)))
        (Iso.hom
            ((fun (j : WalkingParallelPairᵒᵖ) ↦
                (eqToIso ⋯ :
                  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅
                    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
              (Opposite.op zero)) ≫
          Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
op₁ :
  ∀ (f : Opposite.op one ⟶ Opposite.op j),
    let g := f.unop;
    ∀ (this : f = g.op),
      Eq (α :=
        (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
          Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
        ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
          Iso.hom
            ((fun (j : WalkingParallelPairᵒᵖ) ↦
                (eqToIso ⋯ :
                  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅
                    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
              (Opposite.op j)))
        (Iso.hom
            ((fun (j : WalkingParallelPairᵒᵖ) ↦
                (eqToIso ⋯ :
                  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅
                    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
              (Opposite.op one)) ≫
          Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op i) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)

Tactic:
cases i
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
j : WalkingParallelPair
f : Opposite.op zero ⟶ Opposite.op j
g : unop (Opposite.op j) ⟶ unop (Opposite.op zero) := f.unop
this : f = g.op
op :
  ∀ (f : Opposite.op zero ⟶ Opposite.op zero),
    let g := f.unop;
    ∀ (this : f = g.op),
      Eq (α :=
        (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) ⟶
          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 zero)) ≫
          Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
op₁ :
  ∀ (f : Opposite.op zero ⟶ Opposite.op one),
    let g := f.unop;
    ∀ (this : f = g.op),
      Eq (α :=
        (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) ⟶
          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 zero)) ≫
          Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op zero)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)

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

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

Tactic:
cases g