-- 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 ⟶ Y
g : X ⟶ Z
none none₁ none₂ none₃ :
  Eq (α :=
    (cospan f.unop g.unop).obj Option.none ⟶
      obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) Option.none)
    ((cospan f.unop g.unop).map (WidePullbackShape.Hom.id Option.none) ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) x)
                x with
              | Option.none => Iso.refl ((cospan f.unop g.unop).obj Option.none)
              | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right) :
              (cospan f.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) x))
          Option.none))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) x)
                x with
              | Option.none => Iso.refl ((cospan f.unop g.unop).obj Option.none)
              | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right) :
              (cospan f.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) x))
          Option.none) ≫
      map (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) (WidePullbackShape.Hom.id Option.none))
⊢ Eq (α :=
    (cospan f.unop g.unop).obj Option.none ⟶
      obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) Option.none)
    ((cospan f.unop g.unop).map (WidePullbackShape.Hom.id Option.none) ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) x)
                x with
              | Option.none => Iso.refl ((cospan f.unop g.unop).obj Option.none)
              | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right) :
              (cospan f.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) x))
          Option.none))
    (Iso.hom
        ((fun (x : WalkingCospan) ↦
            (match (motive :=
                (x : WalkingCospan) →
                  (cospan f.unop g.unop).obj x ≅
                    obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) x)
                x with
              | Option.none => Iso.refl ((cospan f.unop g.unop).obj Option.none)
              | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
              | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right) :
              (cospan f.unop g.unop).obj x ≅
                obj.{0, v₁, 0, u₁} (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) x))
          Option.none) ≫
      map (walkingSpanOpEquiv.inverse ⋙ Functor.leftOp (span f g)) (WidePullbackShape.Hom.id Option.none))

Tactic:
cat_disch