-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst_2 : HasPullback f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Opposite.op X) (Y :=
      pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) (pushout.inl f.op f.op)
      (pushout.inr f.op f.op))
    (Fork.ofι f.op ⋯)
⊢ Iso.inv (Iso.refl (Opposite.unop (Opposite.op X))) ≫
      CategoryStruct.comp (Y :=
        Cocone.pt (F :=
          parallelPair (X :=
            Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op))
            (Y := Opposite.unop (Opposite.op X)) (Quiver.Hom.unop (pushout.inl f.op f.op))
            (Quiver.Hom.unop (pushout.inr f.op f.op)))
          (ofπ f.op.unop ⋯ :
            Cofork.{v₁, u₁} (C := C) (X :=
              Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op))
              (Y := Opposite.unop (Opposite.op X)) (Quiver.Hom.unop (pushout.inl f.op f.op))
              (Quiver.Hom.unop (pushout.inr f.op f.op))))
        (π (ofπ f.op.unop ⋯) :
          Opposite.unop (Opposite.op X) ⟶
            Cocone.pt (F :=
              parallelPair (X :=
                Opposite.unop
                  (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op))
                (Y := Opposite.unop (Opposite.op X)) (Quiver.Hom.unop (pushout.inl f.op f.op))
                (Quiver.Hom.unop (pushout.inr f.op f.op)))
              (ofπ f.op.unop ⋯ :
                Cofork.{v₁, u₁} (C := C) (X :=
                  Opposite.unop
                    (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op))
                  (Y := Opposite.unop (Opposite.op X)) (Quiver.Hom.unop (pushout.inl f.op f.op))
                  (Quiver.Hom.unop (pushout.inr f.op f.op))))
        (Iso.hom
            (Iso.refl
              (Cocone.pt (F :=
                parallelPair (X :=
                  Opposite.unop
                    (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op))
                  (Y := Opposite.unop (Opposite.op X)) (Quiver.Hom.unop (pushout.inl f.op f.op))
                  (Quiver.Hom.unop (pushout.inr f.op f.op)))
                (ofπ f.op.unop ⋯ :
                  Cofork.{v₁, u₁} (C := C) (X :=
                    Opposite.unop
                      (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op))
                    (Y := Opposite.unop (Opposite.op X)) (Quiver.Hom.unop (pushout.inl f.op f.op))
                    (Quiver.Hom.unop (pushout.inr f.op f.op))))) :
          Cocone.pt (F :=
              parallelPair (X :=
                Opposite.unop
                  (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op))
                (Y := Opposite.unop (Opposite.op X)) (Quiver.Hom.unop (pushout.inl f.op f.op))
                (Quiver.Hom.unop (pushout.inr f.op f.op)))
              (ofπ f.op.unop ⋯ :
                Cofork.{v₁, u₁} (C := C) (X :=
                  Opposite.unop
                    (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op))
                  (Y := Opposite.unop (Opposite.op X)) (Quiver.Hom.unop (pushout.inl f.op f.op))
                  (Quiver.Hom.unop (pushout.inr f.op f.op))) ⟶
            Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (ofπ f ⋯)) =
    π (ofπ f ⋯)

Tactic:
simp