-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
some some₁ some₂ some₃ :
  Eq (α :=
    obj.{0, v₁, 0, u₁} (span f.op g.op) (Option.some WalkingPair.left) ⟶
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj (Option.some WalkingPair.left))
    (map (span f.op g.op) (WidePushoutShape.Hom.id (Option.some WalkingPair.left)) ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) none)
              | Option.some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) WalkingSpan.left)
              | Option.some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj x))
          (Option.some WalkingPair.left)))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) none)
              | Option.some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) WalkingSpan.left)
              | Option.some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj x))
          (Option.some WalkingPair.left)) ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id (Option.some WalkingPair.left)))
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (span f.op g.op) (Option.some WalkingPair.left) ⟶
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj (Option.some WalkingPair.left))
    (map (span f.op g.op) (WidePushoutShape.Hom.id (Option.some WalkingPair.left)) ≫
      Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) none)
              | Option.some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) WalkingSpan.left)
              | Option.some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj x))
          (Option.some WalkingPair.left)))
    (Iso.hom
        ((fun (x : WalkingSpan) ↦
            (match (motive :=
                (x : WalkingSpan) →
                  obj.{0, v₁, 0, u₁} (span f.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj x)
                x with
              | none => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) none)
              | Option.some WalkingPair.left => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) WalkingSpan.left)
              | Option.some WalkingPair.right => Iso.refl (obj.{0, v₁, 0, u₁} (span f.op g.op) WalkingSpan.right) :
              obj.{0, v₁, 0, u₁} (span f.op g.op) x ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj x))
          (Option.some WalkingPair.left)) ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id (Option.some WalkingPair.left)))

Tactic:
cat_disch